QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa23 Unicode version
Theorem oa23 936
Description: Derivation of OA from Godowski/Greechie Eq. II.
Hypothesis
Ref Expression
oa23.1 (c' ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) =< a'
Assertion
Ref Expression
oa23 ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Proof of Theorem oa23
StepHypRef Expression
1 ax-a2 31 . . . . . . 7 (b v c) = (c v b)
21ax-r4 37 . . . . . 6 (b v c)' = (c v b)'
3 ancom 74 . . . . . 6 ((a ->2 b) ^ (a ->2 c)) = ((a ->2 c) ^ (a ->2 b))
42, 32or 72 . . . . 5 ((b v c)' v ((a ->2 b) ^ (a ->2 c))) = ((c v b)' v ((a ->2 c) ^ (a ->2 b)))
54lan 77 . . . 4 ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))
65ax-r5 38 . . 3 (((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) v (a ->2 c)) = (((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))) v (a ->2 c))
7 ax-a2 31 . . 3 (((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))) v (a ->2 c)) = ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))
8 ax-a3 32 . . . . . . . . . 10 (((a ->2 c) v (a ->2 c)) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) = ((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))))
98ax-r1 35 . . . . . . . . 9 ((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) = (((a ->2 c) v (a ->2 c)) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))
10 oridm 110 . . . . . . . . . 10 ((a ->2 c) v (a ->2 c)) = (a ->2 c)
1110ax-r5 38 . . . . . . . . 9 (((a ->2 c) v (a ->2 c)) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) = ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))
129, 11ax-r2 36 . . . . . . . 8 ((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) = ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))
13 u2lemonb 636 . . . . . . . 8 ((a ->2 c) v c') = 1
1412, 132an 79 . . . . . . 7 (((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) ^ ((a ->2 c) v c')) = (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ 1)
1514ax-r1 35 . . . . . 6 (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ 1) = (((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) ^ ((a ->2 c) v c'))
16 an1 106 . . . . . . 7 (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ 1) = ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))
1716ax-r1 35 . . . . . 6 ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) = (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ 1)
18 comorr 184 . . . . . . 7 (a ->2 c) C ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))
19 u2lemc1 681 . . . . . . . . 9 c C (a ->2 c)
2019comcom 453 . . . . . . . 8 (a ->2 c) C c
2120comcom2 183 . . . . . . 7 (a ->2 c) C c'
2218, 21fh3 471 . . . . . 6 ((a ->2 c) v (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ c')) = (((a ->2 c) v ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) ^ ((a ->2 c) v c'))
2315, 17, 223tr1 63 . . . . 5 ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) = ((a ->2 c) v (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ c'))
24 oa23.1 . . . . . . . . 9 (c' ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) =< a'
25 lea 160 . . . . . . . . 9 (c' ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) =< c'
2624, 25ler2an 173 . . . . . . . 8 (c' ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))) =< (a' ^ c')
27 ancom 74 . . . . . . . 8 (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ c') = (c' ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))))
28 u2lemanb 616 . . . . . . . 8 ((a ->2 c) ^ c') = (a' ^ c')
2926, 27, 28le3tr1 140 . . . . . . 7 (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ c') =< ((a ->2 c) ^ c')
3029lelor 166 . . . . . 6 ((a ->2 c) v (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ c')) =< ((a ->2 c) v ((a ->2 c) ^ c'))
31 orabs 120 . . . . . 6 ((a ->2 c) v ((a ->2 c) ^ c')) = (a ->2 c)
3230, 31lbtr 139 . . . . 5 ((a ->2 c) v (((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) ^ c')) =< (a ->2 c)
3323, 32bltr 138 . . . 4 ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) =< (a ->2 c)
34 leo 158 . . . 4 (a ->2 c) =< ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b)))))
3533, 34lebi 145 . . 3 ((a ->2 c) v ((a ->2 b) ^ ((c v b)' v ((a ->2 c) ^ (a ->2 b))))) = (a ->2 c)
366, 7, 353tr 65 . 2 (((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) v (a ->2 c)) = (a ->2 c)
3736df-le1 130 1 ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7  1wt 8   ->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-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  oa43v  1028  oa63v  1032
  Copyright terms: Public domain W3C validator