Theorem wcomlem 364

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

Hypothesis

Ref	Expression
wcomlem.1	(a == ((a ^ b) v (a ^ b_|_))) = 1

Assertion

Ref	Expression
wcomlem	(b == ((b ^ a) v (b ^ a_|_))) = 1

Proof of Theorem wcomlem

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

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v 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