Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-cmtr GIF version

Definition df-cmtr 134
 Description: Define 'commutator'.
Assertion
Ref Expression
df-cmtr C (a, b) = (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab )))

Detailed syntax breakdown of Definition df-cmtr
StepHypRef Expression
1 wva . . 3 term  a
2 wvb . . 3 term  b
31, 2wcmtr 29 . 2 term  C (a, b)
41, 2wa 7 . . . 4 term  (ab)
52wn 4 . . . . 5 term  b
61, 5wa 7 . . . 4 term  (ab )
74, 6wo 6 . . 3 term  ((ab) ∪ (ab ))
81wn 4 . . . . 5 term  a
98, 2wa 7 . . . 4 term  (ab)
108, 5wa 7 . . . 4 term  (ab )
119, 10wo 6 . . 3 term  ((ab) ∪ (ab ))
127, 11wo 6 . 2 term  (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab )))
133, 12wb 1 1 wff  C (a, b) = (((ab) ∪ (ab )) ∪ ((ab) ∪ (ab )))
 Colors of variables: term This definition is referenced by:  cmtrcom  190  wdf-c1  383  wdf-c2  384  cmtr1com  493  comcmtr1  494  i0cmtrcom  495  3vded22  818  wdcom  1103  wdwom  1104
 Copyright terms: Public domain W3C validator