QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3-2to4 Unicode version
Theorem oa3-2to4 988
Description: Derivation of 3-OA variant (4) from (2).
Hypothesis
Ref Expression
oa3-2to4.1 ((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) =< c
Assertion
Ref Expression
oa3-2to4 (a' ^ (a v (b ^ ((a == b) v ((a ->1 c) ^ (b ->1 c)))))) =< c
Proof of Theorem oa3-2to4
StepHypRef Expression
1 oa3-4lem 983 . . 3 (a' ^ (a v (b ^ (((a ^ b) v (a' ^ b')) v (((a ^ c) v (a' ^ 1)) ^ ((b ^ c) v (b' ^ 1))))))) = (a' ^ (a v (b ^ ((a == b) v ((a ->1 c) ^ (b ->1 c))))))
21ax-r1 35 . 2 (a' ^ (a v (b ^ ((a == b) v ((a ->1 c) ^ (b ->1 c)))))) = (a' ^ (a v (b ^ (((a ^ b) v (a' ^ b')) v (((a ^ c) v (a' ^ 1)) ^ ((b ^ c) v (b' ^ 1)))))))
3 leid 148 . . 3 a' =< a'
4 leid 148 . . 3 b' =< b'
5 le1 146 . . 3 c' =< 1
6 an1 106 . . . . . . 7 (c ^ 1) = c
7 dff 101 . . . . . . . . . 10 0 = (a ^ a')
8 dff 101 . . . . . . . . . 10 0 = (b ^ b')
97, 82or 72 . . . . . . . . 9 (0 v 0) = ((a ^ a') v (b ^ b'))
109ax-r1 35 . . . . . . . 8 ((a ^ a') v (b ^ b')) = (0 v 0)
11 or0 102 . . . . . . . 8 (0 v 0) = 0
1210, 11ax-r2 36 . . . . . . 7 ((a ^ a') v (b ^ b')) = 0
136, 122or 72 . . . . . 6 ((c ^ 1) v ((a ^ a') v (b ^ b'))) = (c v 0)
14 or0 102 . . . . . 6 (c v 0) = c
1513, 14ax-r2 36 . . . . 5 ((c ^ 1) v ((a ^ a') v (b ^ b'))) = c
1615ax-r1 35 . . . 4 c = ((c ^ 1) v ((a ^ a') v (b ^ b')))
17 ax-a2 31 . . . 4 ((c ^ 1) v ((a ^ a') v (b ^ b'))) = (((a ^ a') v (b ^ b')) v (c ^ 1))
1816, 17ax-r2 36 . . 3 c = (((a ^ a') v (b ^ b')) v (c ^ 1))
19 oa3-2lemb 979 . . . 4 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ c) v ((a ->1 c) ^ (c ->1 c))) ^ ((b ^ c) v ((b ->1 c) ^ (c ->1 c)))))))) = ((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))
20 oa3-2to4.1 . . . 4 ((a ->1 c) ^ (a v (b ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) =< c
2119, 20bltr 138 . . 3 ((a ->1 c) ^ (a v (b ^ (((a ^ b) v ((a ->1 c) ^ (b ->1 c))) v (((a ^ c) v ((a ->1 c) ^ (c ->1 c))) ^ ((b ^ c) v ((b ->1 c) ^ (c ->1 c)))))))) =< c
223, 4, 5, 18, 21oa4to6dual 964 . 2 (a' ^ (a v (b ^ (((a ^ b) v (a' ^ b')) v (((a ^ c) v (a' ^ 1)) ^ ((b ^ c) v (b' ^ 1))))))) =< c
232, 22bltr 138 1 (a' ^ (a v (b ^ ((a == b) v ((a ->1 c) ^ (b ->1 c)))))) =< c
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8  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: (None)
  Copyright terms: Public domain W3C validator