QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wcomlem Unicode version
Theorem wcomlem 382
Description: Analogue of commutation is symmetric. Similar to Kalmbach 83 p. 22.
Hypothesis
Ref Expression
wcomlem.1 (a == ((a ^ b) v (a ^ b'))) = 1
Assertion
Ref Expression
wcomlem (b == ((b ^ a) v (b ^ a'))) = 1
Proof of Theorem wcomlem
StepHypRef Expression
1 ax-a2 31 . . . . . . . . . 10 (a' v b) = (b v a')
21bi1 118 . . . . . . . . 9 ((a' v b) == (b v a')) = 1
32wran 369 . . . . . . . 8 (((a' v b) ^ b) == ((b v a') ^ b)) = 1
4 ancom 74 . . . . . . . . 9 ((b v a') ^ b) = (b ^ (b v a'))
54bi1 118 . . . . . . . 8 (((b v a') ^ b) == (b ^ (b v a'))) = 1
63, 5wr2 371 . . . . . . 7 (((a' v b) ^ b) == (b ^ (b v a'))) = 1
7 anabs 121 . . . . . . . 8 (b ^ (b v a')) = b
87bi1 118 . . . . . . 7 ((b ^ (b v a')) == b) = 1
96, 8wr2 371 . . . . . 6 (((a' v b) ^ b) == b) = 1
109wlan 370 . . . . 5 (((a' v b') ^ ((a' v b) ^ b)) == ((a' v b') ^ b)) = 1
11 wcomlem.1 . . . . . . . . . 10 (a == ((a ^ b) v (a ^ b'))) = 1
12 df-a 40 . . . . . . . . . . . 12 (a ^ b) = (a' v b')'
1312bi1 118 . . . . . . . . . . 11 ((a ^ b) == (a' v b')') = 1
14 anor1 88 . . . . . . . . . . . 12 (a ^ b') = (a' v b)'
1514bi1 118 . . . . . . . . . . 11 ((a ^ b') == (a' v b)') = 1
1613, 15w2or 372 . . . . . . . . . 10 (((a ^ b) v (a ^ b')) == ((a' v b')' v (a' v b)')) = 1
1711, 16wr2 371 . . . . . . . . 9 (a == ((a' v b')' v (a' v b)')) = 1
1817wr4 199 . . . . . . . 8 (a' == ((a' v b')' v (a' v b)')') = 1
19 df-a 40 . . . . . . . . . 10 ((a' v b') ^ (a' v b)) = ((a' v b')' v (a' v b)')'
2019bi1 118 . . . . . . . . 9 (((a' v b') ^ (a' v b)) == ((a' v b')' v (a' v b)')') = 1
2120wr1 197 . . . . . . . 8 (((a' v b')' v (a' v b)')' == ((a' v b') ^ (a' v b))) = 1
2218, 21wr2 371 . . . . . . 7 (a' == ((a' v b') ^ (a' v b))) = 1
2322wran 369 . . . . . 6 ((a' ^ b) == (((a' v b') ^ (a' v b)) ^ b)) = 1
24 anass 76 . . . . . . 7 (((a' v b') ^ (a' v b)) ^ b) = ((a' v b') ^ ((a' v b) ^ b))
2524bi1 118 . . . . . 6 ((((a' v b') ^ (a' v b)) ^ b) == ((a' v b') ^ ((a' v b) ^ b))) = 1
2623, 25wr2 371 . . . . 5 ((a' ^ b) == ((a' v b') ^ ((a' v b) ^ b))) = 1
2713wcon2 208 . . . . . 6 ((a ^ b)' == (a' v b')) = 1
2827wran 369 . . . . 5 (((a ^ b)' ^ b) == ((a' v b') ^ b)) = 1
2910, 26, 28w3tr1 374 . . . 4 ((a' ^ b) == ((a ^ b)' ^ b)) = 1
3029wlor 368 . . 3 (((a ^ b) v (a' ^ b)) == ((a ^ b) v ((a ^ b)' ^ b))) = 1
3130wr1 197 . 2 (((a ^ b) v ((a ^ b)' ^ b)) == ((a ^ b) v (a' ^ b))) = 1
32 ax-a2 31 . . . . . 6 ((a ^ b) v b) = (b v (a ^ b))
3332bi1 118 . . . . 5 (((a ^ b) v b) == (b v (a ^ b))) = 1
34 ancom 74 . . . . . . . 8 (a ^ b) = (b ^ a)
3534bi1 118 . . . . . . 7 ((a ^ b) == (b ^ a)) = 1
3635wlor 368 . . . . . 6 ((b v (a ^ b)) == (b v (b ^ a))) = 1
37 orabs 120 . . . . . . 7 (b v (b ^ a)) = b
3837bi1 118 . . . . . 6 ((b v (b ^ a)) == b) = 1
3936, 38wr2 371 . . . . 5 ((b v (a ^ b)) == b) = 1
4033, 39wr2 371 . . . 4 (((a ^ b) v b) == b) = 1
4140wdf-le1 378 . . 3 ((a ^ b) =<2 b) = 1
4241wom4 380 . 2 (((a ^ b) v ((a ^ b)' ^ b)) == b) = 1
43 ancom 74 . . . 4 (a' ^ b) = (b ^ a')
4443bi1 118 . . 3 ((a' ^ b) == (b ^ a')) = 1
4535, 44w2or 372 . 2 (((a ^ b) v (a' ^ b)) == ((b ^ a) v (b ^ a'))) = 1
4631, 42, 45w3tr2 375 1 (b == ((b ^ a) v (b ^ a'))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131
This theorem is referenced by:  wdf-c1  383
  Copyright terms: Public domain W3C validator