Theorem wwcomd 214

Description: Commutation dual (weak). Kalmbach 83 p. 23. (Contributed by NM, 2-Sep-1997.)

Hypothesis

Ref	Expression
wwcomd.1	a⊥ C b

Assertion

Ref	Expression
wwcomd	a = ((a ∪ b) ∩ (a ∪ b⊥ ))

Proof of Theorem wwcomd

Step	Hyp	Ref	Expression
1		wwcomd.1	. . . 4 a⊥ C b
2	1	df-c2 133	. . 3 a⊥ = ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
3		oran 87	. . . 4 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) = ((a⊥ ∩ b⊥ )⊥ ∩ (a⊥ ∩ b)⊥ )⊥
4		ax-a2 31	. . . 4 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
5		oran 87	. . . . . 6 (a ∪ b) = (a⊥ ∩ b⊥ )⊥
6		anor2 89	. . . . . . . 8 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
7	6	ax-r1 35	. . . . . . 7 (a ∪ b⊥ )⊥ = (a⊥ ∩ b)
8	7	con3 68	. . . . . 6 (a ∪ b⊥ ) = (a⊥ ∩ b)⊥
9	5, 8	2an 79	. . . . 5 ((a ∪ b) ∩ (a ∪ b⊥ )) = ((a⊥ ∩ b⊥ )⊥ ∩ (a⊥ ∩ b)⊥ )
10	9	ax-r4 37	. . . 4 ((a ∪ b) ∩ (a ∪ b⊥ ))⊥ = ((a⊥ ∩ b⊥ )⊥ ∩ (a⊥ ∩ b)⊥ )⊥
11	3, 4, 10	3tr1 63	. . 3 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b) ∩ (a ∪ b⊥ ))⊥
12	2, 11	ax-r2 36	. 2 a⊥ = ((a ∪ b) ∩ (a ∪ b⊥ ))⊥
13	12	con1 66	1 a = ((a ∪ b) ∩ (a ∪ b⊥ ))

This proof depends on syntax axioms:   = wb 1   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-a 40  df-c2 133

This theorem is used by:  wwcom3ii  215