Theorem cmtrcom 190

Description: Commutative law for commutator. (Contributed by NM, 24-Jan-1999.)

Assertion

Ref	Expression
cmtrcom	C (a, b) = C (b, a)

Proof of Theorem cmtrcom

Step	Hyp	Ref	Expression
1		ancom 74	. . . . 5 (a ∩ b) = (b ∩ a)
2		ancom 74	. . . . 5 (a ∩ b⊥ ) = (b⊥ ∩ a)
3	1, 2	2or 72	. . . 4 ((a ∩ b) ∪ (a ∩ b⊥ )) = ((b ∩ a) ∪ (b⊥ ∩ a))
4		ancom 74	. . . . 5 (a⊥ ∩ b) = (b ∩ a⊥ )
5		ancom 74	. . . . 5 (a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ )
6	4, 5	2or 72	. . . 4 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((b ∩ a⊥ ) ∪ (b⊥ ∩ a⊥ ))
7	3, 6	2or 72	. . 3 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b ∩ a⊥ ) ∪ (b⊥ ∩ a⊥ )))
8		or4 84	. . 3 (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b ∩ a⊥ ) ∪ (b⊥ ∩ a⊥ ))) = (((b ∩ a) ∪ (b ∩ a⊥ )) ∪ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )))
9	7, 8	ax-r2 36	. 2 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((b ∩ a) ∪ (b ∩ a⊥ )) ∪ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )))
10		df-cmtr 134	. 2 C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
11		df-cmtr 134	. 2 C (b, a) = (((b ∩ a) ∪ (b ∩ a⊥ )) ∪ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )))
12	9, 10, 11	3tr1 63	1 C (a, b) = C (b, a)

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

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

This proof depends on definitions:  df-a 40  df-cmtr 134

This theorem is used by:  wdf-c1  383  wcomcom  414  3vded3  819