Theorem woml6 418

Description: Variant of weakly orthomodular law.

Assertion

Ref	Expression
woml6	((a →1 b)⊥ ∪ (a →2 b)) = 1

Proof of Theorem woml6

Step	Hyp	Ref	Expression
1		df-i1 43	. . . . . 6 (a →1 b) = (a⊥ ∪ (a ∩ b))
2		df-a 39	. . . . . . 7 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
3	2	lor 66	. . . . . 6 (a⊥ ∪ (a ∩ b)) = (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )
4	1, 3	ax-r2 35	. . . . 5 (a →1 b) = (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )
5	4	ax-r4 36	. . . 4 (a →1 b)⊥ = (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )⊥
6		df-a 39	. . . . 5 (a ∩ (a⊥ ∪ b⊥ )) = (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )⊥
7	6	ax-r1 34	. . . 4 (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )⊥ = (a ∩ (a⊥ ∪ b⊥ ))
8	5, 7	ax-r2 35	. . 3 (a →1 b)⊥ = (a ∩ (a⊥ ∪ b⊥ ))
9		df-i2 44	. . 3 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
10	8, 9	2or 67	. 2 ((a →1 b)⊥ ∪ (a →2 b)) = ((a ∩ (a⊥ ∪ b⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))
11		ax-a2 30	. . . . 5 ((a ∩ (a⊥ ∪ b⊥ )) ∪ b) = (b ∪ (a ∩ (a⊥ ∪ b⊥ )))
12		ancom 68	. . . . . 6 (a ∩ (a⊥ ∪ b⊥ )) = ((a⊥ ∪ b⊥ ) ∩ a)
13	12	lor 66	. . . . 5 (b ∪ (a ∩ (a⊥ ∪ b⊥ ))) = (b ∪ ((a⊥ ∪ b⊥ ) ∩ a))
14	11, 13	ax-r2 35	. . . 4 ((a ∩ (a⊥ ∪ b⊥ )) ∪ b) = (b ∪ ((a⊥ ∪ b⊥ ) ∩ a))
15	14	ax-r5 37	. . 3 (((a ∩ (a⊥ ∪ b⊥ )) ∪ b) ∪ (a⊥ ∩ b⊥ )) = ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ ))
16		ax-a3 31	. . 3 (((a ∩ (a⊥ ∪ b⊥ )) ∪ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∩ (a⊥ ∪ b⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))
17		1b 109	. . . . 5 (1 ≡ ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ ))) = ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ ))
18	17	ax-r1 34	. . . 4 ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )) = (1 ≡ ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )))
19		wcomorr 394	. . . . . . . . . . . 12 C (b⊥ , (b⊥ ∪ a⊥ )) = 1
20		ax-a2 30	. . . . . . . . . . . . 13 (b⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
21	20	bi1 110	. . . . . . . . . . . 12 ((b⊥ ∪ a⊥ ) ≡ (a⊥ ∪ b⊥ )) = 1
22	19, 21	wcbtr 393	. . . . . . . . . . 11 C (b⊥ , (a⊥ ∪ b⊥ )) = 1
23	22	wcomcom 396	. . . . . . . . . 10 C ((a⊥ ∪ b⊥ ), b⊥ ) = 1
24	23	wcomcom3 398	. . . . . . . . 9 C ((a⊥ ∪ b⊥ )⊥ , b⊥ ) = 1
25	24	wcomcom5 402	. . . . . . . 8 C ((a⊥ ∪ b⊥ ), b) = 1
26		wcomorr 394	. . . . . . . . . . 11 C (a⊥ , (a⊥ ∪ b⊥ )) = 1
27	26	wcomcom 396	. . . . . . . . . 10 C ((a⊥ ∪ b⊥ ), a⊥ ) = 1
28	27	wcomcom3 398	. . . . . . . . 9 C ((a⊥ ∪ b⊥ )⊥ , a⊥ ) = 1
29	28	wcomcom5 402	. . . . . . . 8 C ((a⊥ ∪ b⊥ ), a) = 1
30	25, 29	wfh4 408	. . . . . . 7 ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ≡ ((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a))) = 1
31	30	wr5-2v 348	. . . . . 6 (((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )) ≡ (((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) ∪ (a⊥ ∩ b⊥ ))) = 1
32		or12 73	. . . . . . . . . . . . 13 (b ∪ (a⊥ ∪ b⊥ )) = (a⊥ ∪ (b ∪ b⊥ ))
33		df-t 40	. . . . . . . . . . . . . . 15 1 = (b ∪ b⊥ )
34	33	lor 66	. . . . . . . . . . . . . 14 (a⊥ ∪ 1) = (a⊥ ∪ (b ∪ b⊥ ))
35	34	ax-r1 34	. . . . . . . . . . . . 13 (a⊥ ∪ (b ∪ b⊥ )) = (a⊥ ∪ 1)
36		or1 96	. . . . . . . . . . . . 13 (a⊥ ∪ 1) = 1
37	32, 35, 36	3tr 62	. . . . . . . . . . . 12 (b ∪ (a⊥ ∪ b⊥ )) = 1
38	37	ran 71	. . . . . . . . . . 11 ((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) = (1 ∩ (b ∪ a))
39		ancom 68	. . . . . . . . . . 11 (1 ∩ (b ∪ a)) = ((b ∪ a) ∩ 1)
40	38, 39	ax-r2 35	. . . . . . . . . 10 ((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) = ((b ∪ a) ∩ 1)
41		an1 98	. . . . . . . . . 10 ((b ∪ a) ∩ 1) = (b ∪ a)
42		ax-a2 30	. . . . . . . . . 10 (b ∪ a) = (a ∪ b)
43	40, 41, 42	3tr 62	. . . . . . . . 9 ((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) = (a ∪ b)
44		anor3 82	. . . . . . . . 9 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
45	43, 44	2or 67	. . . . . . . 8 (((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b) ∪ (a ∪ b)⊥ )
46		df-t 40	. . . . . . . . 9 1 = ((a ∪ b) ∪ (a ∪ b)⊥ )
47	46	ax-r1 34	. . . . . . . 8 ((a ∪ b) ∪ (a ∪ b)⊥ ) = 1
48	45, 47	ax-r2 35	. . . . . . 7 (((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) ∪ (a⊥ ∩ b⊥ )) = 1
49	48	bi1 110	. . . . . 6 ((((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) ∪ (a⊥ ∩ b⊥ )) ≡ 1) = 1
50	31, 49	wr2 353	. . . . 5 (((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )) ≡ 1) = 1
51	50	wr1 189	. . . 4 (1 ≡ ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ ))) = 1
52	18, 51	ax-r2 35	. . 3 ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )) = 1
53	15, 16, 52	3tr2 61	. 2 ((a ∩ (a⊥ ∪ b⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ ))) = 1
54	10, 53	ax-r2 35	1 ((a →1 b)⊥ ∪ (a →2 b)) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 9   →₁ wi1 13   →₂ wi2 14

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-wom 343

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le 121  df-le1 122  df-le2 123  df-cmtr 126

metamath.org