QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  mlaconj4 Unicode version
Theorem mlaconj4 844
Description: For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper.
Hypotheses
Ref Expression
mlaconj4.1 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< (d == c)
mlaconj4.2 d = (a v b)
mlaconj4.3 e = (a ^ b)
Assertion
Ref Expression
mlaconj4 ((a == b) ^ ((a == c) v (b == c))) =< (a == c)
Proof of Theorem mlaconj4
StepHypRef Expression
1 biao 799 . . . . 5 (a == b) = ((a ^ b) == (a v b))
2 bicom 96 . . . . 5 ((a ^ b) == (a v b)) = ((a v b) == (a ^ b))
31, 2ax-r2 36 . . . 4 (a == b) = ((a v b) == (a ^ b))
43bile 142 . . 3 (a == b) =< ((a v b) == (a ^ b))
5 orbile 843 . . . 4 ((a == c) v (b == c)) =< (((a ^ b) ->2 c) ^ (c ->1 (a v b)))
6 imp3 841 . . . 4 (((a ^ b) ->2 c) ^ (c ->1 (a v b))) = (((a ^ b)' ^ c') v (c ^ (a v b)))
75, 6lbtr 139 . . 3 ((a == c) v (b == c)) =< (((a ^ b)' ^ c') v (c ^ (a v b)))
84, 7le2an 169 . 2 ((a == b) ^ ((a == c) v (b == c))) =< (((a v b) == (a ^ b)) ^ (((a ^ b)' ^ c') v (c ^ (a v b))))
9 mlaconj4.2 . . . . . 6 d = (a v b)
10 mlaconj4.3 . . . . . 6 e = (a ^ b)
119, 102bi 99 . . . . 5 (d == e) = ((a v b) == (a ^ b))
1210ax-r4 37 . . . . . . 7 e' = (a ^ b)'
1312ran 78 . . . . . 6 (e' ^ c') = ((a ^ b)' ^ c')
14 ancom 74 . . . . . . 7 (d ^ c) = (c ^ d)
159lan 77 . . . . . . 7 (c ^ d) = (c ^ (a v b))
1614, 15ax-r2 36 . . . . . 6 (d ^ c) = (c ^ (a v b))
1713, 162or 72 . . . . 5 ((e' ^ c') v (d ^ c)) = (((a ^ b)' ^ c') v (c ^ (a v b)))
1811, 172an 79 . . . 4 ((d == e) ^ ((e' ^ c') v (d ^ c))) = (((a v b) == (a ^ b)) ^ (((a ^ b)' ^ c') v (c ^ (a v b))))
1918ax-r1 35 . . 3 (((a v b) == (a ^ b)) ^ (((a ^ b)' ^ c') v (c ^ (a v b)))) = ((d == e) ^ ((e' ^ c') v (d ^ c)))
20 lea 160 . . . . . 6 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< (d == e)
21 bicom 96 . . . . . . 7 ((a v b) == (a ^ b)) = ((a ^ b) == (a v b))
2221, 11, 13tr1 63 . . . . . 6 (d == e) = (a == b)
2320, 22lbtr 139 . . . . 5 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< (a == b)
24 mlaconj4.1 . . . . . 6 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< (d == c)
259rbi 98 . . . . . 6 (d == c) = ((a v b) == c)
2624, 25lbtr 139 . . . . 5 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< ((a v b) == c)
2723, 26ler2an 173 . . . 4 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< ((a == b) ^ ((a v b) == c))
28 anass 76 . . . . . . . . . . 11 ((a' ^ b') ^ c') = (a' ^ (b' ^ c'))
29 coman1 185 . . . . . . . . . . . 12 (a' ^ (b' ^ c')) C a'
3029comcom7 460 . . . . . . . . . . 11 (a' ^ (b' ^ c')) C a
3128, 30bctr 181 . . . . . . . . . 10 ((a' ^ b') ^ c') C a
32 an32 83 . . . . . . . . . . 11 ((a' ^ b') ^ c') = ((a' ^ c') ^ b')
33 coman2 186 . . . . . . . . . . . 12 ((a' ^ c') ^ b') C b'
3433comcom7 460 . . . . . . . . . . 11 ((a' ^ c') ^ b') C b
3532, 34bctr 181 . . . . . . . . . 10 ((a' ^ b') ^ c') C b
3631, 35com2an 484 . . . . . . . . 9 ((a' ^ b') ^ c') C (a ^ b)
37 coman1 185 . . . . . . . . 9 ((a' ^ b') ^ c') C (a' ^ b')
3836, 37com2or 483 . . . . . . . 8 ((a' ^ b') ^ c') C ((a ^ b) v (a' ^ b'))
3931, 35com2or 483 . . . . . . . . 9 ((a' ^ b') ^ c') C (a v b)
40 coman2 186 . . . . . . . . . 10 ((a' ^ b') ^ c') C c'
4140comcom7 460 . . . . . . . . 9 ((a' ^ b') ^ c') C c
4239, 41com2an 484 . . . . . . . 8 ((a' ^ b') ^ c') C ((a v b) ^ c)
4338, 42fh2c 477 . . . . . . 7 (((a ^ b) v (a' ^ b')) ^ (((a v b) ^ c) v ((a' ^ b') ^ c'))) = ((((a ^ b) v (a' ^ b')) ^ ((a v b) ^ c)) v (((a ^ b) v (a' ^ b')) ^ ((a' ^ b') ^ c')))
44 anor3 90 . . . . . . . . . . 11 (a' ^ b') = (a v b)'
45 comanr1 464 . . . . . . . . . . . 12 (a v b) C ((a v b) ^ c)
4645comcom3 454 . . . . . . . . . . 11 (a v b)' C ((a v b) ^ c)
4744, 46bctr 181 . . . . . . . . . 10 (a' ^ b') C ((a v b) ^ c)
48 coman1 185 . . . . . . . . . . . 12 (a' ^ b') C a'
4948comcom7 460 . . . . . . . . . . 11 (a' ^ b') C a
50 coman2 186 . . . . . . . . . . . 12 (a' ^ b') C b'
5150comcom7 460 . . . . . . . . . . 11 (a' ^ b') C b
5249, 51com2an 484 . . . . . . . . . 10 (a' ^ b') C (a ^ b)
5347, 52fh2rc 480 . . . . . . . . 9 (((a ^ b) v (a' ^ b')) ^ ((a v b) ^ c)) = (((a ^ b) ^ ((a v b) ^ c)) v ((a' ^ b') ^ ((a v b) ^ c)))
54 anass 76 . . . . . . . . . . . 12 (((a ^ b) ^ (a v b)) ^ c) = ((a ^ b) ^ ((a v b) ^ c))
5554ax-r1 35 . . . . . . . . . . 11 ((a ^ b) ^ ((a v b) ^ c)) = (((a ^ b) ^ (a v b)) ^ c)
56 leao1 162 . . . . . . . . . . . . 13 (a ^ b) =< (a v b)
5756df2le2 136 . . . . . . . . . . . 12 ((a ^ b) ^ (a v b)) = (a ^ b)
5857ran 78 . . . . . . . . . . 11 (((a ^ b) ^ (a v b)) ^ c) = ((a ^ b) ^ c)
5955, 58ax-r2 36 . . . . . . . . . 10 ((a ^ b) ^ ((a v b) ^ c)) = ((a ^ b) ^ c)
60 dff 101 . . . . . . . . . . . . . 14 0 = ((a' ^ b') ^ (a' ^ b')')
61 oran 87 . . . . . . . . . . . . . . . 16 (a v b) = (a' ^ b')'
6261lan 77 . . . . . . . . . . . . . . 15 ((a' ^ b') ^ (a v b)) = ((a' ^ b') ^ (a' ^ b')')
6362ax-r1 35 . . . . . . . . . . . . . 14 ((a' ^ b') ^ (a' ^ b')') = ((a' ^ b') ^ (a v b))
6460, 63ax-r2 36 . . . . . . . . . . . . 13 0 = ((a' ^ b') ^ (a v b))
6564ran 78 . . . . . . . . . . . 12 (0 ^ c) = (((a' ^ b') ^ (a v b)) ^ c)
6665ax-r1 35 . . . . . . . . . . 11 (((a' ^ b') ^ (a v b)) ^ c) = (0 ^ c)
67 anass 76 . . . . . . . . . . 11 (((a' ^ b') ^ (a v b)) ^ c) = ((a' ^ b') ^ ((a v b) ^ c))
68 an0r 109 . . . . . . . . . . 11 (0 ^ c) = 0
6966, 67, 683tr2 64 . . . . . . . . . 10 ((a' ^ b') ^ ((a v b) ^ c)) = 0
7059, 692or 72 . . . . . . . . 9 (((a ^ b) ^ ((a v b) ^ c)) v ((a' ^ b') ^ ((a v b) ^ c))) = (((a ^ b) ^ c) v 0)
71 or0 102 . . . . . . . . 9 (((a ^ b) ^ c) v 0) = ((a ^ b) ^ c)
7253, 70, 713tr 65 . . . . . . . 8 (((a ^ b) v (a' ^ b')) ^ ((a v b) ^ c)) = ((a ^ b) ^ c)
73 comanr1 464 . . . . . . . . . 10 (a' ^ b') C ((a' ^ b') ^ c')
7473, 52fh2rc 480 . . . . . . . . 9 (((a ^ b) v (a' ^ b')) ^ ((a' ^ b') ^ c')) = (((a ^ b) ^ ((a' ^ b') ^ c')) v ((a' ^ b') ^ ((a' ^ b') ^ c')))
75 an4 86 . . . . . . . . . . 11 ((a ^ b) ^ ((a' ^ b') ^ c')) = ((a ^ (a' ^ b')) ^ (b ^ c'))
76 dff 101 . . . . . . . . . . . . . . 15 0 = (a ^ a')
7776ran 78 . . . . . . . . . . . . . 14 (0 ^ b') = ((a ^ a') ^ b')
78 an0r 109 . . . . . . . . . . . . . 14 (0 ^ b') = 0
79 anass 76 . . . . . . . . . . . . . 14 ((a ^ a') ^ b') = (a ^ (a' ^ b'))
8077, 78, 793tr2 64 . . . . . . . . . . . . 13 0 = (a ^ (a' ^ b'))
8180ran 78 . . . . . . . . . . . 12 (0 ^ (b ^ c')) = ((a ^ (a' ^ b')) ^ (b ^ c'))
8281ax-r1 35 . . . . . . . . . . 11 ((a ^ (a' ^ b')) ^ (b ^ c')) = (0 ^ (b ^ c'))
83 an0r 109 . . . . . . . . . . 11 (0 ^ (b ^ c')) = 0
8475, 82, 833tr 65 . . . . . . . . . 10 ((a ^ b) ^ ((a' ^ b') ^ c')) = 0
85 anass 76 . . . . . . . . . . . 12 (((a' ^ b') ^ (a' ^ b')) ^ c') = ((a' ^ b') ^ ((a' ^ b') ^ c'))
8685ax-r1 35 . . . . . . . . . . 11 ((a' ^ b') ^ ((a' ^ b') ^ c')) = (((a' ^ b') ^ (a' ^ b')) ^ c')
87 anidm 111 . . . . . . . . . . . 12 ((a' ^ b') ^ (a' ^ b')) = (a' ^ b')
8887ran 78 . . . . . . . . . . 11 (((a' ^ b') ^ (a' ^ b')) ^ c') = ((a' ^ b') ^ c')
8986, 88ax-r2 36 . . . . . . . . . 10 ((a' ^ b') ^ ((a' ^ b') ^ c')) = ((a' ^ b') ^ c')
9084, 892or 72 . . . . . . . . 9 (((a ^ b) ^ ((a' ^ b') ^ c')) v ((a' ^ b') ^ ((a' ^ b') ^ c'))) = (0 v ((a' ^ b') ^ c'))
91 or0r 103 . . . . . . . . 9 (0 v ((a' ^ b') ^ c')) = ((a' ^ b') ^ c')
9274, 90, 913tr 65 . . . . . . . 8 (((a ^ b) v (a' ^ b')) ^ ((a' ^ b') ^ c')) = ((a' ^ b') ^ c')
9372, 922or 72 . . . . . . 7 ((((a ^ b) v (a' ^ b')) ^ ((a v b) ^ c)) v (((a ^ b) v (a' ^ b')) ^ ((a' ^ b') ^ c'))) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
9443, 93ax-r2 36 . . . . . 6 (((a ^ b) v (a' ^ b')) ^ (((a v b) ^ c) v ((a' ^ b') ^ c'))) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
95 dfb 94 . . . . . . 7 (a == b) = ((a ^ b) v (a' ^ b'))
96 dfb 94 . . . . . . . 8 ((a v b) == c) = (((a v b) ^ c) v ((a v b)' ^ c'))
9744ran 78 . . . . . . . . . 10 ((a' ^ b') ^ c') = ((a v b)' ^ c')
9897lor 70 . . . . . . . . 9 (((a v b) ^ c) v ((a' ^ b') ^ c')) = (((a v b) ^ c) v ((a v b)' ^ c'))
9998ax-r1 35 . . . . . . . 8 (((a v b) ^ c) v ((a v b)' ^ c')) = (((a v b) ^ c) v ((a' ^ b') ^ c'))
10096, 99ax-r2 36 . . . . . . 7 ((a v b) == c) = (((a v b) ^ c) v ((a' ^ b') ^ c'))
10195, 1002an 79 . . . . . 6 ((a == b) ^ ((a v b) == c)) = (((a ^ b) v (a' ^ b')) ^ (((a v b) ^ c) v ((a' ^ b') ^ c')))
102 bi3 839 . . . . . 6 ((a == b) ^ (b == c)) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
10394, 101, 1023tr1 63 . . . . 5 ((a == b) ^ ((a v b) == c)) = ((a == b) ^ (b == c))
104 mlaoml 833 . . . . 5 ((a == b) ^ (b == c)) =< (a == c)
105103, 104bltr 138 . . . 4 ((a == b) ^ ((a v b) == c)) =< (a == c)
10627, 105letr 137 . . 3 ((d == e) ^ ((e' ^ c') v (d ^ c))) =< (a == c)
10719, 106bltr 138 . 2 (((a v b) == (a ^ b)) ^ (((a ^ b)' ^ c') v (c ^ (a v b)))) =< (a == c)
1088, 107letr 137 1 ((a == b) ^ ((a == c) v (b == c))) =< (a == c)
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   == tb 5   v wo 6   ^ wa 7  0wf 9   ->1 wi1 12   ->2 wi2 13
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-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator