Theorem wcom3ii 419

Description: Lemma 3(ii) of Kalmbach 83 p. 23. (Contributed by NM, 13-Oct-1997.)

Hypothesis

Ref	Expression
wcomcom.1	C (a, b) = 1

Assertion

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

Proof of Theorem wcom3ii

Step	Hyp	Ref	Expression
1		wcomcom.1	. . . . . 6 C (a, b) = 1
2	1	wcomcom 414	. . . . 5 C (b, a) = 1
3	2	wcomd 418	. . . 4 (b ≡ ((b ∪ a) ∩ (b ∪ a⊥ ))) = 1
4	3	wlan 370	. . 3 ((a ∩ b) ≡ (a ∩ ((b ∪ a) ∩ (b ∪ a⊥ )))) = 1
5		anass 76	. . . . . 6 ((a ∩ (b ∪ a)) ∩ (b ∪ a⊥ )) = (a ∩ ((b ∪ a) ∩ (b ∪ a⊥ )))
6	5	bi1 118	. . . . 5 (((a ∩ (b ∪ a)) ∩ (b ∪ a⊥ )) ≡ (a ∩ ((b ∪ a) ∩ (b ∪ a⊥ )))) = 1
7	6	wr1 197	. . . 4 ((a ∩ ((b ∪ a) ∩ (b ∪ a⊥ ))) ≡ ((a ∩ (b ∪ a)) ∩ (b ∪ a⊥ ))) = 1
8		ax-a2 31	. . . . . . . 8 (b ∪ a) = (a ∪ b)
9	8	bi1 118	. . . . . . 7 ((b ∪ a) ≡ (a ∪ b)) = 1
10	9	wlan 370	. . . . . 6 ((a ∩ (b ∪ a)) ≡ (a ∩ (a ∪ b))) = 1
11		anabs 121	. . . . . . 7 (a ∩ (a ∪ b)) = a
12	11	bi1 118	. . . . . 6 ((a ∩ (a ∪ b)) ≡ a) = 1
13	10, 12	wr2 371	. . . . 5 ((a ∩ (b ∪ a)) ≡ a) = 1
14		ax-a2 31	. . . . . 6 (b ∪ a⊥ ) = (a⊥ ∪ b)
15	14	bi1 118	. . . . 5 ((b ∪ a⊥ ) ≡ (a⊥ ∪ b)) = 1
16	13, 15	w2an 373	. . . 4 (((a ∩ (b ∪ a)) ∩ (b ∪ a⊥ )) ≡ (a ∩ (a⊥ ∪ b))) = 1
17	7, 16	wr2 371	. . 3 ((a ∩ ((b ∪ a) ∩ (b ∪ a⊥ ))) ≡ (a ∩ (a⊥ ∪ b))) = 1
18	4, 17	wr2 371	. 2 ((a ∩ b) ≡ (a ∩ (a⊥ ∪ b))) = 1
19	18	wr1 197	1 ((a ∩ (a⊥ ∪ b)) ≡ (a ∩ b)) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8   C wcmtr 29

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:  wfh1  423  wfh2  424