QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  negantlem10 Unicode version
Theorem negantlem10 861
Description: Lemma for negated antecedent identity.
Hypothesis
Ref Expression
negant.1 (a ->1 c) = (b ->1 c)
Assertion
Ref Expression
negantlem10 (a ->4 c) =< (b ->4 c)
Proof of Theorem negantlem10
StepHypRef Expression
1 leao4 165 . . . . 5 (a ^ c) =< (b' v c)
2 leor 159 . . . . . . . 8 (a ^ c) =< (a' v (a ^ c))
3 df-i1 44 . . . . . . . . 9 (a ->1 c) = (a' v (a ^ c))
43ax-r1 35 . . . . . . . 8 (a' v (a ^ c)) = (a ->1 c)
52, 4lbtr 139 . . . . . . 7 (a ^ c) =< (a ->1 c)
6 lear 161 . . . . . . 7 (a ^ c) =< c
75, 6ler2an 173 . . . . . 6 (a ^ c) =< ((a ->1 c) ^ c)
8 negant.1 . . . . . . . 8 (a ->1 c) = (b ->1 c)
98ran 78 . . . . . . 7 ((a ->1 c) ^ c) = ((b ->1 c) ^ c)
10 u1lemab 610 . . . . . . . 8 ((b ->1 c) ^ c) = ((b ^ c) v (b' ^ c))
11 leor 159 . . . . . . . . 9 ((b ^ c) v (b' ^ c)) =< (c' v ((b ^ c) v (b' ^ c)))
12 ancom 74 . . . . . . . . . . . . 13 (b ^ c) = (c ^ b)
13 ancom 74 . . . . . . . . . . . . 13 (b' ^ c) = (c ^ b')
1412, 132or 72 . . . . . . . . . . . 12 ((b ^ c) v (b' ^ c)) = ((c ^ b) v (c ^ b'))
15 ax-a2 31 . . . . . . . . . . . 12 ((c ^ b) v (c ^ b')) = ((c ^ b') v (c ^ b))
1614, 15ax-r2 36 . . . . . . . . . . 11 ((b ^ c) v (b' ^ c)) = ((c ^ b') v (c ^ b))
1716lor 70 . . . . . . . . . 10 (c' v ((b ^ c) v (b' ^ c))) = (c' v ((c ^ b') v (c ^ b)))
18 ax-a3 32 . . . . . . . . . . 11 ((c' v (c ^ b')) v (c ^ b)) = (c' v ((c ^ b') v (c ^ b)))
1918ax-r1 35 . . . . . . . . . 10 (c' v ((c ^ b') v (c ^ b))) = ((c' v (c ^ b')) v (c ^ b))
2017, 19ax-r2 36 . . . . . . . . 9 (c' v ((b ^ c) v (b' ^ c))) = ((c' v (c ^ b')) v (c ^ b))
2111, 20lbtr 139 . . . . . . . 8 ((b ^ c) v (b' ^ c)) =< ((c' v (c ^ b')) v (c ^ b))
2210, 21bltr 138 . . . . . . 7 ((b ->1 c) ^ c) =< ((c' v (c ^ b')) v (c ^ b))
239, 22bltr 138 . . . . . 6 ((a ->1 c) ^ c) =< ((c' v (c ^ b')) v (c ^ b))
247, 23letr 137 . . . . 5 (a ^ c) =< ((c' v (c ^ b')) v (c ^ b))
251, 24ler2an 173 . . . 4 (a ^ c) =< ((b' v c) ^ ((c' v (c ^ b')) v (c ^ b)))
26 leao4 165 . . . . 5 (a' ^ c) =< (b' v c)
27 leor 159 . . . . . . . 8 (a' ^ c) =< (a'' v (a' ^ c))
28 df-i1 44 . . . . . . . . 9 (a' ->1 c) = (a'' v (a' ^ c))
2928ax-r1 35 . . . . . . . 8 (a'' v (a' ^ c)) = (a' ->1 c)
3027, 29lbtr 139 . . . . . . 7 (a' ^ c) =< (a' ->1 c)
31 lear 161 . . . . . . 7 (a' ^ c) =< c
3230, 31ler2an 173 . . . . . 6 (a' ^ c) =< ((a' ->1 c) ^ c)
338negant 852 . . . . . . . 8 (a' ->1 c) = (b' ->1 c)
3433ran 78 . . . . . . 7 ((a' ->1 c) ^ c) = ((b' ->1 c) ^ c)
35 u1lemab 610 . . . . . . . 8 ((b' ->1 c) ^ c) = ((b' ^ c) v (b'' ^ c))
36 leor 159 . . . . . . . . 9 ((b' ^ c) v (b'' ^ c)) =< (c' v ((b' ^ c) v (b'' ^ c)))
37 ancom 74 . . . . . . . . . . . . 13 (c ^ b') = (b' ^ c)
38 ancom 74 . . . . . . . . . . . . . 14 (c ^ b) = (b ^ c)
39 ax-a1 30 . . . . . . . . . . . . . . 15 b = b''
4039ran 78 . . . . . . . . . . . . . 14 (b ^ c) = (b'' ^ c)
4138, 40ax-r2 36 . . . . . . . . . . . . 13 (c ^ b) = (b'' ^ c)
4237, 412or 72 . . . . . . . . . . . 12 ((c ^ b') v (c ^ b)) = ((b' ^ c) v (b'' ^ c))
4342lor 70 . . . . . . . . . . 11 (c' v ((c ^ b') v (c ^ b))) = (c' v ((b' ^ c) v (b'' ^ c)))
4443ax-r1 35 . . . . . . . . . 10 (c' v ((b' ^ c) v (b'' ^ c))) = (c' v ((c ^ b') v (c ^ b)))
4544, 19ax-r2 36 . . . . . . . . 9 (c' v ((b' ^ c) v (b'' ^ c))) = ((c' v (c ^ b')) v (c ^ b))
4636, 45lbtr 139 . . . . . . . 8 ((b' ^ c) v (b'' ^ c)) =< ((c' v (c ^ b')) v (c ^ b))
4735, 46bltr 138 . . . . . . 7 ((b' ->1 c) ^ c) =< ((c' v (c ^ b')) v (c ^ b))
4834, 47bltr 138 . . . . . 6 ((a' ->1 c) ^ c) =< ((c' v (c ^ b')) v (c ^ b))
4932, 48letr 137 . . . . 5 (a' ^ c) =< ((c' v (c ^ b')) v (c ^ b))
5026, 49ler2an 173 . . . 4 (a' ^ c) =< ((b' v c) ^ ((c' v (c ^ b')) v (c ^ b)))
5125, 50lel2or 170 . . 3 ((a ^ c) v (a' ^ c)) =< ((b' v c) ^ ((c' v (c ^ b')) v (c ^ b)))
52 lea 160 . . . . 5 ((a' v c) ^ c') =< (a' v c)
538negantlem8 856 . . . . 5 (a' v c) = (b' v c)
5452, 53lbtr 139 . . . 4 ((a' v c) ^ c') =< (b' v c)
55 leao2 163 . . . . 5 ((a' v c) ^ c') =< (c' v (c ^ b'))
5655ler 149 . . . 4 ((a' v c) ^ c') =< ((c' v (c ^ b')) v (c ^ b))
5754, 56ler2an 173 . . 3 ((a' v c) ^ c') =< ((b' v c) ^ ((c' v (c ^ b')) v (c ^ b)))
5851, 57lel2or 170 . 2 (((a ^ c) v (a' ^ c)) v ((a' v c) ^ c')) =< ((b' v c) ^ ((c' v (c ^ b')) v (c ^ b)))
59 df-i4 47 . 2 (a ->4 c) = (((a ^ c) v (a' ^ c)) v ((a' v c) ^ c'))
60 dfi4b 500 . 2 (b ->4 c) = ((b' v c) ^ ((c' v (c ^ b')) v (c ^ b)))
6158, 59, 60le3tr1 140 1 (a ->4 c) =< (b ->4 c)
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6   ^ wa 7   ->1 wi1 12   ->4 wi4 15
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-i3 46  df-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  negant4  862
  Copyright terms: Public domain W3C validator