Theorem cmtrcom 182

Description: Commutative law for commutator.

Assertion

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

Proof of Theorem cmtrcom

Step	Hyp	Ref	Expression
1		ancom 68	. . . . 5 (a ∩ b) = (b ∩ a)
2		ancom 68	. . . . 5 (a ∩ b⊥ ) = (b⊥ ∩ a)
3	1, 2	2or 67	. . . 4 ((a ∩ b) ∪ (a ∩ b⊥ )) = ((b ∩ a) ∪ (b⊥ ∩ a))
4		ancom 68	. . . . 5 (a⊥ ∩ b) = (b ∩ a⊥ )
5		ancom 68	. . . . 5 (a⊥ ∩ b⊥ ) = (b⊥ ∩ a⊥ )
6	4, 5	2or 67	. . . 4 ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) = ((b ∩ a⊥ ) ∪ (b⊥ ∩ a⊥ ))
7	3, 6	2or 67	. . 3 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b ∩ a⊥ ) ∪ (b⊥ ∩ a⊥ )))
8		or4 77	. . 3 (((b ∩ a) ∪ (b⊥ ∩ a)) ∪ ((b ∩ a⊥ ) ∪ (b⊥ ∩ a⊥ ))) = (((b ∩ a) ∪ (b ∩ a⊥ )) ∪ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )))
9	7, 8	ax-r2 35	. 2 (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))) = (((b ∩ a) ∪ (b ∩ a⊥ )) ∪ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )))
10		df-cmtr 126	. 2 C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
11		df-cmtr 126	. 2 C (b, a) = (((b ∩ a) ∪ (b ∩ a⊥ )) ∪ ((b⊥ ∩ a) ∪ (b⊥ ∩ a⊥ )))
12	9, 10, 11	3tr1 60	1 C (a, b) = C (b, a)

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7   C wcmtr 28

This theorem is referenced by:  wdf-c1 365  wcomcom 396  3vded3 801

This theorem was proved from axioms:  ax-a2 30  ax-a3 31  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-cmtr 126

metamath.org