Theorem wcomlem 382

Description: Analogue of commutation is symmetric. Similar to Kalmbach 83 p. 22. (Contributed by NM, 27-Jan-2002.)

Hypothesis

Ref	Expression
wcomlem.1	(a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1

Assertion

Ref	Expression
wcomlem	(b ≡ ((b ∩ a) ∪ (b ∩ a⊥ ))) = 1

Proof of Theorem wcomlem

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . . . . . . . 10 (a⊥ ∪ b) = (b ∪ a⊥ )
2	1	bi1 118	. . . . . . . . 9 ((a⊥ ∪ b) ≡ (b ∪ a⊥ )) = 1
3	2	wran 369	. . . . . . . 8 (((a⊥ ∪ b) ∩ b) ≡ ((b ∪ a⊥ ) ∩ b)) = 1
4		ancom 74	. . . . . . . . 9 ((b ∪ a⊥ ) ∩ b) = (b ∩ (b ∪ a⊥ ))
5	4	bi1 118	. . . . . . . 8 (((b ∪ a⊥ ) ∩ b) ≡ (b ∩ (b ∪ a⊥ ))) = 1
6	3, 5	wr2 371	. . . . . . 7 (((a⊥ ∪ b) ∩ b) ≡ (b ∩ (b ∪ a⊥ ))) = 1
7		anabs 121	. . . . . . . 8 (b ∩ (b ∪ a⊥ )) = b
8	7	bi1 118	. . . . . . 7 ((b ∩ (b ∪ a⊥ )) ≡ b) = 1
9	6, 8	wr2 371	. . . . . 6 (((a⊥ ∪ b) ∩ b) ≡ b) = 1
10	9	wlan 370	. . . . 5 (((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b)) ≡ ((a⊥ ∪ b⊥ ) ∩ b)) = 1
11		wcomlem.1	. . . . . . . . . 10 (a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1
12		df-a 40	. . . . . . . . . . . 12 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
13	12	bi1 118	. . . . . . . . . . 11 ((a ∩ b) ≡ (a⊥ ∪ b⊥ )⊥ ) = 1
14		anor1 88	. . . . . . . . . . . 12 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
15	14	bi1 118	. . . . . . . . . . 11 ((a ∩ b⊥ ) ≡ (a⊥ ∪ b)⊥ ) = 1
16	13, 15	w2or 372	. . . . . . . . . 10 (((a ∩ b) ∪ (a ∩ b⊥ )) ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )) = 1
17	11, 16	wr2 371	. . . . . . . . 9 (a ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )) = 1
18	17	wr4 199	. . . . . . . 8 (a⊥ ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥ ) = 1
19		df-a 40	. . . . . . . . . 10 ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) = ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥
20	19	bi1 118	. . . . . . . . 9 (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥ ) = 1
21	20	wr1 197	. . . . . . . 8 (((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥ ≡ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))) = 1
22	18, 21	wr2 371	. . . . . . 7 (a⊥ ≡ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))) = 1
23	22	wran 369	. . . . . 6 ((a⊥ ∩ b) ≡ (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ b)) = 1
24		anass 76	. . . . . . 7 (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ b) = ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b))
25	24	bi1 118	. . . . . 6 ((((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ b) ≡ ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b))) = 1
26	23, 25	wr2 371	. . . . 5 ((a⊥ ∩ b) ≡ ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b))) = 1
27	13	wcon2 208	. . . . . 6 ((a ∩ b)⊥ ≡ (a⊥ ∪ b⊥ )) = 1
28	27	wran 369	. . . . 5 (((a ∩ b)⊥ ∩ b) ≡ ((a⊥ ∪ b⊥ ) ∩ b)) = 1
29	10, 26, 28	w3tr1 374	. . . 4 ((a⊥ ∩ b) ≡ ((a ∩ b)⊥ ∩ b)) = 1
30	29	wlor 368	. . 3 (((a ∩ b) ∪ (a⊥ ∩ b)) ≡ ((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b))) = 1
31	30	wr1 197	. 2 (((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b)) ≡ ((a ∩ b) ∪ (a⊥ ∩ b))) = 1
32		ax-a2 31	. . . . . 6 ((a ∩ b) ∪ b) = (b ∪ (a ∩ b))
33	32	bi1 118	. . . . 5 (((a ∩ b) ∪ b) ≡ (b ∪ (a ∩ b))) = 1
34		ancom 74	. . . . . . . 8 (a ∩ b) = (b ∩ a)
35	34	bi1 118	. . . . . . 7 ((a ∩ b) ≡ (b ∩ a)) = 1
36	35	wlor 368	. . . . . 6 ((b ∪ (a ∩ b)) ≡ (b ∪ (b ∩ a))) = 1
37		orabs 120	. . . . . . 7 (b ∪ (b ∩ a)) = b
38	37	bi1 118	. . . . . 6 ((b ∪ (b ∩ a)) ≡ b) = 1
39	36, 38	wr2 371	. . . . 5 ((b ∪ (a ∩ b)) ≡ b) = 1
40	33, 39	wr2 371	. . . 4 (((a ∩ b) ∪ b) ≡ b) = 1
41	40	wdf-le1 378	. . 3 ((a ∩ b) ≤2 b) = 1
42	41	wom4 380	. 2 (((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b)) ≡ b) = 1
43		ancom 74	. . . 4 (a⊥ ∩ b) = (b ∩ a⊥ )
44	43	bi1 118	. . 3 ((a⊥ ∩ b) ≡ (b ∩ a⊥ )) = 1
45	35, 44	w2or 372	. 2 (((a ∩ b) ∪ (a⊥ ∩ b)) ≡ ((b ∩ a) ∪ (b ∩ a⊥ ))) = 1
46	31, 42, 45	w3tr2 375	1 (b ≡ ((b ∩ a) ∪ (b ∩ a⊥ ))) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8

This theorem was proved from 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 theorem 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

This theorem is referenced by:  wdf-c1  383