Definition df-cmtr 126

Description: Define 'commutator'.

Assertion

Ref	Expression
df-cmtr	C (a, b) = (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (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 28	. 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) v (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) v (a_|_ ^ b_|_))
12	7, 11	wo 6	. 2 term (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
13	3, 12	wb 1	1 wff C (a, b) = (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (a_|_ ^ b_|_)))

This definition is referenced by:  cmtrcom 182  wdf-c1 365  wdf-c2 366  cmtr1com 475  comcmtr1 476  i0cmtrcom 477  3vded22 800

metamath.org