Theorem wcomlem 364

Description: Analogue of commutation is symmetric. Similar to Kalmbach 83 p. 22.

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 30	. . . . . . . . . 10 (a⊥ ∪ b) = (b ∪ a⊥ )
2	1	bi1 110	. . . . . . . . 9 ((a⊥ ∪ b) ≡ (b ∪ a⊥ )) = 1
3	2	wran 351	. . . . . . . 8 (((a⊥ ∪ b) ∩ b) ≡ ((b ∪ a⊥ ) ∩ b)) = 1
4		ancom 68	. . . . . . . . 9 ((b ∪ a⊥ ) ∩ b) = (b ∩ (b ∪ a⊥ ))
5	4	bi1 110	. . . . . . . 8 (((b ∪ a⊥ ) ∩ b) ≡ (b ∩ (b ∪ a⊥ ))) = 1
6	3, 5	wr2 353	. . . . . . 7 (((a⊥ ∪ b) ∩ b) ≡ (b ∩ (b ∪ a⊥ ))) = 1
7		a5c 113	. . . . . . . 8 (b ∩ (b ∪ a⊥ )) = b
8	7	bi1 110	. . . . . . 7 ((b ∩ (b ∪ a⊥ )) ≡ b) = 1
9	6, 8	wr2 353	. . . . . 6 (((a⊥ ∪ b) ∩ b) ≡ b) = 1
10	9	wlan 352	. . . . 5 (((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b)) ≡ ((a⊥ ∪ b⊥ ) ∩ b)) = 1
11		wcomlem.1	. . . . . . . . . 10 (a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1
12		df-a 39	. . . . . . . . . . . 12 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
13	12	bi1 110	. . . . . . . . . . 11 ((a ∩ b) ≡ (a⊥ ∪ b⊥ )⊥ ) = 1
14		anor1 80	. . . . . . . . . . . 12 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
15	14	bi1 110	. . . . . . . . . . 11 ((a ∩ b⊥ ) ≡ (a⊥ ∪ b)⊥ ) = 1
16	13, 15	w2or 354	. . . . . . . . . 10 (((a ∩ b) ∪ (a ∩ b⊥ )) ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )) = 1
17	11, 16	wr2 353	. . . . . . . . 9 (a ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )) = 1
18	17	wr4 191	. . . . . . . 8 (a⊥ ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥ ) = 1
19		df-a 39	. . . . . . . . . 10 ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) = ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥
20	19	bi1 110	. . . . . . . . 9 (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ≡ ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥ ) = 1
21	20	wr1 189	. . . . . . . 8 (((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥ ≡ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))) = 1
22	18, 21	wr2 353	. . . . . . 7 (a⊥ ≡ ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))) = 1
23	22	wran 351	. . . . . 6 ((a⊥ ∩ b) ≡ (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ b)) = 1
24		anass 69	. . . . . . 7 (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ b) = ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b))
25	24	bi1 110	. . . . . 6 ((((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ b) ≡ ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b))) = 1
26	23, 25	wr2 353	. . . . 5 ((a⊥ ∩ b) ≡ ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b))) = 1
27	13	wcon2 200	. . . . . 6 ((a ∩ b)⊥ ≡ (a⊥ ∪ b⊥ )) = 1
28	27	wran 351	. . . . 5 (((a ∩ b)⊥ ∩ b) ≡ ((a⊥ ∪ b⊥ ) ∩ b)) = 1
29	10, 26, 28	w3tr1 356	. . . 4 ((a⊥ ∩ b) ≡ ((a ∩ b)⊥ ∩ b)) = 1
30	29	wlor 350	. . 3 (((a ∩ b) ∪ (a⊥ ∩ b)) ≡ ((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b))) = 1
31	30	wr1 189	. 2 (((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b)) ≡ ((a ∩ b) ∪ (a⊥ ∩ b))) = 1
32		ax-a2 30	. . . . . 6 ((a ∩ b) ∪ b) = (b ∪ (a ∩ b))
33	32	bi1 110	. . . . 5 (((a ∩ b) ∪ b) ≡ (b ∪ (a ∩ b))) = 1
34		ancom 68	. . . . . . . 8 (a ∩ b) = (b ∩ a)
35	34	bi1 110	. . . . . . 7 ((a ∩ b) ≡ (b ∩ a)) = 1
36	35	wlor 350	. . . . . 6 ((b ∪ (a ∩ b)) ≡ (b ∪ (b ∩ a))) = 1
37		a5b 112	. . . . . . 7 (b ∪ (b ∩ a)) = b
38	37	bi1 110	. . . . . 6 ((b ∪ (b ∩ a)) ≡ b) = 1
39	36, 38	wr2 353	. . . . 5 ((b ∪ (a ∩ b)) ≡ b) = 1
40	33, 39	wr2 353	. . . 4 (((a ∩ b) ∪ b) ≡ b) = 1
41	40	wdf-le1 360	. . 3 ((a ∩ b) ≤2 b) = 1
42	41	wom4 362	. 2 (((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b)) ≡ b) = 1
43		ancom 68	. . . 4 (a⊥ ∩ b) = (b ∩ a⊥ )
44	43	bi1 110	. . 3 ((a⊥ ∩ b) ≡ (b ∩ a⊥ )) = 1
45	35, 44	w2or 354	. 2 (((a ∩ b) ∪ (a⊥ ∩ b)) ≡ ((b ∩ a) ∪ (b ∩ a⊥ ))) = 1
46	31, 42, 45	w3tr2 357	1 (b ≡ ((b ∩ a) ∪ (b ∩ a⊥ ))) = 1

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

This theorem is referenced by:  wdf-c1 365

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

metamath.org