Definition df-cmtr 134

Description: Define "commutator". (Contributed by NM, 24-Jan-1999.)

Assertion

Ref	Expression
df-cmtr	C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))

Detailed syntax breakdown of Definition df-cmtr

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2		wvb	. . 3 term  b
3	1, 2	wcmtr 29	. 2 term  C (a, b)
4	1, 2	wa 7	. . . 4 term  (a ∩ b)
5	2	wn 4	. . . . 5 term  b⊥
6	1, 5	wa 7	. . . 4 term  (a ∩ b⊥ )
7	4, 6	wo 6	. . 3 term  ((a ∩ b) ∪ (a ∩ b⊥ ))
8	1	wn 4	. . . . 5 term  a⊥
9	8, 2	wa 7	. . . 4 term  (a⊥ ∩ b)
10	8, 5	wa 7	. . . 4 term  (a⊥ ∩ b⊥ )
11	9, 10	wo 6	. . 3 term  ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ ))
12	7, 11	wo 6	. 2 term  (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
13	3, 12	wb 1	1 wff  C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))

This definition is used by:  cmtrcom  190  wdf-c1  383  wdf-c2  384  cmtr1com  493  comcmtr1  494  i0cmtrcom  495  3vded22  818  wdcom  1105  wdwom  1106