QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-cmtr Unicode version
Definition df-cmtr 134
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
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 (a ^ b)
52wn 4 . . . . 5 term b'
61, 5wa 7 . . . 4 term (a ^ b')
74, 6wo 6 . . 3 term ((a ^ b) v (a ^ b'))
81wn 4 . . . . 5 term a'
98, 2wa 7 . . . 4 term (a' ^ b)
108, 5wa 7 . . . 4 term (a' ^ b')
119, 10wo 6 . . 3 term ((a' ^ b) v (a' ^ b'))
127, 11wo 6 . 2 term (((a ^ b) v (a ^ b')) v ((a' ^ b) v (a' ^ b')))
133, 12wb 1 1 wff C (a, b) = (((a ^ b) v (a ^ b')) v ((a' ^ b) v (a' ^ b')))
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