Theorem woml6 436

Description: Variant of weakly orthomodular law. (Contributed by NM, 14-Nov-1998.)

Assertion

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

Proof of Theorem woml6

Step	Hyp	Ref	Expression
1		df-i1 44	. . . . . 6 (a →1 b) = (a⊥ ∪ (a ∩ b))
2		df-a 40	. . . . . . 7 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
3	2	lor 70	. . . . . 6 (a⊥ ∪ (a ∩ b)) = (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )
4	1, 3	ax-r2 36	. . . . 5 (a →1 b) = (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )
5	4	ax-r4 37	. . . 4 (a →1 b)⊥ = (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )⊥
6		df-a 40	. . . . 5 (a ∩ (a⊥ ∪ b⊥ )) = (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )⊥
7	6	ax-r1 35	. . . 4 (a⊥ ∪ (a⊥ ∪ b⊥ )⊥ )⊥ = (a ∩ (a⊥ ∪ b⊥ ))
8	5, 7	ax-r2 36	. . 3 (a →1 b)⊥ = (a ∩ (a⊥ ∪ b⊥ ))
9		df-i2 45	. . 3 (a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
10	8, 9	2or 72	. 2 ((a →1 b)⊥ ∪ (a →2 b)) = ((a ∩ (a⊥ ∪ b⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))
11		ax-a2 31	. . . . 5 ((a ∩ (a⊥ ∪ b⊥ )) ∪ b) = (b ∪ (a ∩ (a⊥ ∪ b⊥ )))
12		ancom 74	. . . . . 6 (a ∩ (a⊥ ∪ b⊥ )) = ((a⊥ ∪ b⊥ ) ∩ a)
13	12	lor 70	. . . . 5 (b ∪ (a ∩ (a⊥ ∪ b⊥ ))) = (b ∪ ((a⊥ ∪ b⊥ ) ∩ a))
14	11, 13	ax-r2 36	. . . 4 ((a ∩ (a⊥ ∪ b⊥ )) ∪ b) = (b ∪ ((a⊥ ∪ b⊥ ) ∩ a))
15	14	ax-r5 38	. . 3 (((a ∩ (a⊥ ∪ b⊥ )) ∪ b) ∪ (a⊥ ∩ b⊥ )) = ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ ))
16		ax-a3 32	. . 3 (((a ∩ (a⊥ ∪ b⊥ )) ∪ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∩ (a⊥ ∪ b⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ )))
17		1b 117	. . . . 5 (1 ≡ ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ ))) = ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ ))
18	17	ax-r1 35	. . . 4 ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )) = (1 ≡ ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )))
19		wcomorr 412	. . . . . . . . . . . 12 C (b⊥ , (b⊥ ∪ a⊥ )) = 1
20		ax-a2 31	. . . . . . . . . . . . 13 (b⊥ ∪ a⊥ ) = (a⊥ ∪ b⊥ )
21	20	bi1 118	. . . . . . . . . . . 12 ((b⊥ ∪ a⊥ ) ≡ (a⊥ ∪ b⊥ )) = 1
22	19, 21	wcbtr 411	. . . . . . . . . . 11 C (b⊥ , (a⊥ ∪ b⊥ )) = 1
23	22	wcomcom 414	. . . . . . . . . 10 C ((a⊥ ∪ b⊥ ), b⊥ ) = 1
24	23	wcomcom3 416	. . . . . . . . 9 C ((a⊥ ∪ b⊥ )⊥ , b⊥ ) = 1
25	24	wcomcom5 420	. . . . . . . 8 C ((a⊥ ∪ b⊥ ), b) = 1
26		wcomorr 412	. . . . . . . . . . 11 C (a⊥ , (a⊥ ∪ b⊥ )) = 1
27	26	wcomcom 414	. . . . . . . . . 10 C ((a⊥ ∪ b⊥ ), a⊥ ) = 1
28	27	wcomcom3 416	. . . . . . . . 9 C ((a⊥ ∪ b⊥ )⊥ , a⊥ ) = 1
29	28	wcomcom5 420	. . . . . . . 8 C ((a⊥ ∪ b⊥ ), a) = 1
30	25, 29	wfh4 426	. . . . . . 7 ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ≡ ((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a))) = 1
31	30	wr5-2v 366	. . . . . 6 (((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )) ≡ (((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) ∪ (a⊥ ∩ b⊥ ))) = 1
32		or12 80	. . . . . . . . . . . . 13 (b ∪ (a⊥ ∪ b⊥ )) = (a⊥ ∪ (b ∪ b⊥ ))
33		df-t 41	. . . . . . . . . . . . . . 15 1 = (b ∪ b⊥ )
34	33	lor 70	. . . . . . . . . . . . . 14 (a⊥ ∪ 1) = (a⊥ ∪ (b ∪ b⊥ ))
35	34	ax-r1 35	. . . . . . . . . . . . 13 (a⊥ ∪ (b ∪ b⊥ )) = (a⊥ ∪ 1)
36		or1 104	. . . . . . . . . . . . 13 (a⊥ ∪ 1) = 1
37	32, 35, 36	3tr 65	. . . . . . . . . . . 12 (b ∪ (a⊥ ∪ b⊥ )) = 1
38	37	ran 78	. . . . . . . . . . 11 ((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) = (1 ∩ (b ∪ a))
39		ancom 74	. . . . . . . . . . 11 (1 ∩ (b ∪ a)) = ((b ∪ a) ∩ 1)
40	38, 39	ax-r2 36	. . . . . . . . . 10 ((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) = ((b ∪ a) ∩ 1)
41		an1 106	. . . . . . . . . 10 ((b ∪ a) ∩ 1) = (b ∪ a)
42		ax-a2 31	. . . . . . . . . 10 (b ∪ a) = (a ∪ b)
43	40, 41, 42	3tr 65	. . . . . . . . 9 ((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) = (a ∪ b)
44		anor3 90	. . . . . . . . 9 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
45	43, 44	2or 72	. . . . . . . 8 (((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b) ∪ (a ∪ b)⊥ )
46		df-t 41	. . . . . . . . 9 1 = ((a ∪ b) ∪ (a ∪ b)⊥ )
47	46	ax-r1 35	. . . . . . . 8 ((a ∪ b) ∪ (a ∪ b)⊥ ) = 1
48	45, 47	ax-r2 36	. . . . . . 7 (((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) ∪ (a⊥ ∩ b⊥ )) = 1
49	48	bi1 118	. . . . . 6 ((((b ∪ (a⊥ ∪ b⊥ )) ∩ (b ∪ a)) ∪ (a⊥ ∩ b⊥ )) ≡ 1) = 1
50	31, 49	wr2 371	. . . . 5 (((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )) ≡ 1) = 1
51	50	wr1 197	. . . 4 (1 ≡ ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ ))) = 1
52	18, 51	ax-r2 36	. . 3 ((b ∪ ((a⊥ ∪ b⊥ ) ∩ a)) ∪ (a⊥ ∩ b⊥ )) = 1
53	15, 16, 52	3tr2 64	. 2 ((a ∩ (a⊥ ∪ b⊥ )) ∪ (b ∪ (a⊥ ∩ b⊥ ))) = 1
54	10, 53	ax-r2 36	1 ((a →1 b)⊥ ∪ (a →2 b)) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12   →₂ wi2 13

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wom 361

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134

This theorem is used by:  lem3.4.1  1075