QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  comanblem1 Unicode version
Theorem comanblem1 870
Description: Lemma for biconditional commutation law.
Assertion
Ref Expression
comanblem1 ((a == c) ^ (b == c)) = (((a v c)' v ((a ^ b) ^ c)) ^ (b ->1 c))
Proof of Theorem comanblem1
StepHypRef Expression
1 an4 86 . 2 (((a ->1 c) ^ (c ->1 a)) ^ ((b ->1 c) ^ (c ->1 b))) = (((a ->1 c) ^ (b ->1 c)) ^ ((c ->1 a) ^ (c ->1 b)))
2 u1lembi 720 . . 3 ((a ->1 c) ^ (c ->1 a)) = (a == c)
3 u1lembi 720 . . 3 ((b ->1 c) ^ (c ->1 b)) = (b == c)
42, 32an 79 . 2 (((a ->1 c) ^ (c ->1 a)) ^ ((b ->1 c) ^ (c ->1 b))) = ((a == c) ^ (b == c))
5 an32 83 . . 3 (((a ->1 c) ^ (b ->1 c)) ^ ((c ->1 a) ^ (c ->1 b))) = (((a ->1 c) ^ ((c ->1 a) ^ (c ->1 b))) ^ (b ->1 c))
6 df-i1 44 . . . . . . . 8 (c ->1 a) = (c' v (c ^ a))
7 df-i1 44 . . . . . . . 8 (c ->1 b) = (c' v (c ^ b))
86, 72an 79 . . . . . . 7 ((c ->1 a) ^ (c ->1 b)) = ((c' v (c ^ a)) ^ (c' v (c ^ b)))
9 comanr1 464 . . . . . . . . . 10 c C (c ^ a)
109comcom3 454 . . . . . . . . 9 c' C (c ^ a)
11 comanr1 464 . . . . . . . . . 10 c C (c ^ b)
1211comcom3 454 . . . . . . . . 9 c' C (c ^ b)
1310, 12fh3 471 . . . . . . . 8 (c' v ((c ^ a) ^ (c ^ b))) = ((c' v (c ^ a)) ^ (c' v (c ^ b)))
1413ax-r1 35 . . . . . . 7 ((c' v (c ^ a)) ^ (c' v (c ^ b))) = (c' v ((c ^ a) ^ (c ^ b)))
158, 14ax-r2 36 . . . . . 6 ((c ->1 a) ^ (c ->1 b)) = (c' v ((c ^ a) ^ (c ^ b)))
1615lan 77 . . . . 5 ((a ->1 c) ^ ((c ->1 a) ^ (c ->1 b))) = ((a ->1 c) ^ (c' v ((c ^ a) ^ (c ^ b))))
17 df-i1 44 . . . . . 6 (a ->1 c) = (a' v (a ^ c))
1817ran 78 . . . . 5 ((a ->1 c) ^ (c' v ((c ^ a) ^ (c ^ b)))) = ((a' v (a ^ c)) ^ (c' v ((c ^ a) ^ (c ^ b))))
19 lea 160 . . . . . . . . 9 ((c ^ a) ^ (c ^ b)) =< (c ^ a)
20 ancom 74 . . . . . . . . . 10 (c ^ a) = (a ^ c)
21 leor 159 . . . . . . . . . 10 (a ^ c) =< (a' v (a ^ c))
2220, 21bltr 138 . . . . . . . . 9 (c ^ a) =< (a' v (a ^ c))
2319, 22letr 137 . . . . . . . 8 ((c ^ a) ^ (c ^ b)) =< (a' v (a ^ c))
2423lecom 180 . . . . . . 7 ((c ^ a) ^ (c ^ b)) C (a' v (a ^ c))
2510, 12com2an 484 . . . . . . . 8 c' C ((c ^ a) ^ (c ^ b))
2625comcom 453 . . . . . . 7 ((c ^ a) ^ (c ^ b)) C c'
2724, 26fh2c 477 . . . . . 6 ((a' v (a ^ c)) ^ (c' v ((c ^ a) ^ (c ^ b)))) = (((a' v (a ^ c)) ^ c') v ((a' v (a ^ c)) ^ ((c ^ a) ^ (c ^ b))))
28 coman2 186 . . . . . . . . . 10 (a ^ c) C c
2928comcom2 183 . . . . . . . . 9 (a ^ c) C c'
30 coman1 185 . . . . . . . . . 10 (a ^ c) C a
3130comcom2 183 . . . . . . . . 9 (a ^ c) C a'
3229, 31fh2rc 480 . . . . . . . 8 ((a' v (a ^ c)) ^ c') = ((a' ^ c') v ((a ^ c) ^ c'))
33 anass 76 . . . . . . . . . 10 ((a ^ c) ^ c') = (a ^ (c ^ c'))
34 dff 101 . . . . . . . . . . . 12 0 = (c ^ c')
3534lan 77 . . . . . . . . . . 11 (a ^ 0) = (a ^ (c ^ c'))
3635ax-r1 35 . . . . . . . . . 10 (a ^ (c ^ c')) = (a ^ 0)
37 an0 108 . . . . . . . . . 10 (a ^ 0) = 0
3833, 36, 373tr 65 . . . . . . . . 9 ((a ^ c) ^ c') = 0
3938lor 70 . . . . . . . 8 ((a' ^ c') v ((a ^ c) ^ c')) = ((a' ^ c') v 0)
40 or0 102 . . . . . . . . 9 ((a' ^ c') v 0) = (a' ^ c')
41 anor3 90 . . . . . . . . 9 (a' ^ c') = (a v c)'
4240, 41ax-r2 36 . . . . . . . 8 ((a' ^ c') v 0) = (a v c)'
4332, 39, 423tr 65 . . . . . . 7 ((a' v (a ^ c)) ^ c') = (a v c)'
44 ancom 74 . . . . . . . . . 10 (a ^ c) = (c ^ a)
45 comanr1 464 . . . . . . . . . 10 (c ^ a) C ((c ^ a) ^ (c ^ b))
4644, 45bctr 181 . . . . . . . . 9 (a ^ c) C ((c ^ a) ^ (c ^ b))
4746, 31fh2rc 480 . . . . . . . 8 ((a' v (a ^ c)) ^ ((c ^ a) ^ (c ^ b))) = ((a' ^ ((c ^ a) ^ (c ^ b))) v ((a ^ c) ^ ((c ^ a) ^ (c ^ b))))
48 anandi 114 . . . . . . . . . . . 12 (c ^ (a ^ b)) = ((c ^ a) ^ (c ^ b))
4948ax-r1 35 . . . . . . . . . . 11 ((c ^ a) ^ (c ^ b)) = (c ^ (a ^ b))
50 ancom 74 . . . . . . . . . . 11 (c ^ (a ^ b)) = ((a ^ b) ^ c)
5149, 50ax-r2 36 . . . . . . . . . 10 ((c ^ a) ^ (c ^ b)) = ((a ^ b) ^ c)
5251lan 77 . . . . . . . . 9 (a' ^ ((c ^ a) ^ (c ^ b))) = (a' ^ ((a ^ b) ^ c))
5351lan 77 . . . . . . . . . 10 ((a ^ c) ^ ((c ^ a) ^ (c ^ b))) = ((a ^ c) ^ ((a ^ b) ^ c))
54 ancom 74 . . . . . . . . . 10 ((a ^ c) ^ ((a ^ b) ^ c)) = (((a ^ b) ^ c) ^ (a ^ c))
55 lea 160 . . . . . . . . . . . 12 (a ^ b) =< a
5655leran 153 . . . . . . . . . . 11 ((a ^ b) ^ c) =< (a ^ c)
5756df2le2 136 . . . . . . . . . 10 (((a ^ b) ^ c) ^ (a ^ c)) = ((a ^ b) ^ c)
5853, 54, 573tr 65 . . . . . . . . 9 ((a ^ c) ^ ((c ^ a) ^ (c ^ b))) = ((a ^ b) ^ c)
5952, 582or 72 . . . . . . . 8 ((a' ^ ((c ^ a) ^ (c ^ b))) v ((a ^ c) ^ ((c ^ a) ^ (c ^ b)))) = ((a' ^ ((a ^ b) ^ c)) v ((a ^ b) ^ c))
60 lear 161 . . . . . . . . 9 (a' ^ ((a ^ b) ^ c)) =< ((a ^ b) ^ c)
6160df-le2 131 . . . . . . . 8 ((a' ^ ((a ^ b) ^ c)) v ((a ^ b) ^ c)) = ((a ^ b) ^ c)
6247, 59, 613tr 65 . . . . . . 7 ((a' v (a ^ c)) ^ ((c ^ a) ^ (c ^ b))) = ((a ^ b) ^ c)
6343, 622or 72 . . . . . 6 (((a' v (a ^ c)) ^ c') v ((a' v (a ^ c)) ^ ((c ^ a) ^ (c ^ b)))) = ((a v c)' v ((a ^ b) ^ c))
6427, 63ax-r2 36 . . . . 5 ((a' v (a ^ c)) ^ (c' v ((c ^ a) ^ (c ^ b)))) = ((a v c)' v ((a ^ b) ^ c))
6516, 18, 643tr 65 . . . 4 ((a ->1 c) ^ ((c ->1 a) ^ (c ->1 b))) = ((a v c)' v ((a ^ b) ^ c))
6665ran 78 . . 3 (((a ->1 c) ^ ((c ->1 a) ^ (c ->1 b))) ^ (b ->1 c)) = (((a v c)' v ((a ^ b) ^ c)) ^ (b ->1 c))
675, 66ax-r2 36 . 2 (((a ->1 c) ^ (b ->1 c)) ^ ((c ->1 a) ^ (c ->1 b))) = (((a v c)' v ((a ^ b) ^ c)) ^ (b ->1 c))
681, 4, 673tr2 64 1 ((a == c) ^ (b == c)) = (((a v c)' v ((a ^ b) ^ c)) ^ (b ->1 c))
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  0wf 9   ->1 wi1 12
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-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  comanb  872
  Copyright terms: Public domain W3C validator