QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3-u1 Unicode version
Theorem oa3-u1 991
Description: Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA.
Hypothesis
Ref Expression
oa3-u1.1 ((c ->1 c) ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v ((c ->1 c) ^ ((a' ->1 c) ->1 c))) v (((c ^ (b' ->1 c)) v ((c ->1 c) ^ ((b' ->1 c) ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v (((a' ->1 c) ->1 c) ^ ((b' ->1 c) ->1 c)))))))) =< c
Assertion
Ref Expression
oa3-u1 (c v ((a' ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c))))))) =< c
Proof of Theorem oa3-u1
StepHypRef Expression
1 oa3-u1lem 985 . . 3 (1 ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) = (c v ((a' ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))))))
21ax-r1 35 . 2 (c v ((a' ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c))))))) = (1 ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))))
3 le1 146 . . . 4 c' =< 1
4 u1lem9ab 779 . . . 4 (a' ->1 c)' =< (a ->1 c)
5 u1lem9ab 779 . . . 4 (b' ->1 c)' =< (b ->1 c)
6 ax-a2 31 . . . . . . 7 (c v ((b ^ c) v (b' ^ c))) = (((b ^ c) v (b' ^ c)) v c)
7 lear 161 . . . . . . . . 9 (b ^ c) =< c
8 lear 161 . . . . . . . . 9 (b' ^ c) =< c
97, 8lel2or 170 . . . . . . . 8 ((b ^ c) v (b' ^ c)) =< c
109df-le2 131 . . . . . . 7 (((b ^ c) v (b' ^ c)) v c) = c
116, 10ax-r2 36 . . . . . 6 (c v ((b ^ c) v (b' ^ c))) = c
1211ax-r1 35 . . . . 5 c = (c v ((b ^ c) v (b' ^ c)))
13 an1 106 . . . . . . . . 9 (c ^ 1) = c
14 ancom 74 . . . . . . . . . 10 ((a' ->1 c) ^ (a ->1 c)) = ((a ->1 c) ^ (a' ->1 c))
15 u1lem8 776 . . . . . . . . . 10 ((a ->1 c) ^ (a' ->1 c)) = ((a ^ c) v (a' ^ c))
1614, 15ax-r2 36 . . . . . . . . 9 ((a' ->1 c) ^ (a ->1 c)) = ((a ^ c) v (a' ^ c))
1713, 162or 72 . . . . . . . 8 ((c ^ 1) v ((a' ->1 c) ^ (a ->1 c))) = (c v ((a ^ c) v (a' ^ c)))
18 ax-a2 31 . . . . . . . 8 (c v ((a ^ c) v (a' ^ c))) = (((a ^ c) v (a' ^ c)) v c)
19 lear 161 . . . . . . . . . 10 (a ^ c) =< c
20 lear 161 . . . . . . . . . 10 (a' ^ c) =< c
2119, 20lel2or 170 . . . . . . . . 9 ((a ^ c) v (a' ^ c)) =< c
2221df-le2 131 . . . . . . . 8 (((a ^ c) v (a' ^ c)) v c) = c
2317, 18, 223tr 65 . . . . . . 7 ((c ^ 1) v ((a' ->1 c) ^ (a ->1 c))) = c
24 ancom 74 . . . . . . . 8 ((b' ->1 c) ^ (b ->1 c)) = ((b ->1 c) ^ (b' ->1 c))
25 u1lem8 776 . . . . . . . 8 ((b ->1 c) ^ (b' ->1 c)) = ((b ^ c) v (b' ^ c))
2624, 25ax-r2 36 . . . . . . 7 ((b' ->1 c) ^ (b ->1 c)) = ((b ^ c) v (b' ^ c))
2723, 262or 72 . . . . . 6 (((c ^ 1) v ((a' ->1 c) ^ (a ->1 c))) v ((b' ->1 c) ^ (b ->1 c))) = (c v ((b ^ c) v (b' ^ c)))
2827ax-r1 35 . . . . 5 (c v ((b ^ c) v (b' ^ c))) = (((c ^ 1) v ((a' ->1 c) ^ (a ->1 c))) v ((b' ->1 c) ^ (b ->1 c)))
2912, 28ax-r2 36 . . . 4 c = (((c ^ 1) v ((a' ->1 c) ^ (a ->1 c))) v ((b' ->1 c) ^ (b ->1 c)))
30 oa3-u1.1 . . . 4 ((c ->1 c) ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v ((c ->1 c) ^ ((a' ->1 c) ->1 c))) v (((c ^ (b' ->1 c)) v ((c ->1 c) ^ ((b' ->1 c) ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v (((a' ->1 c) ->1 c) ^ ((b' ->1 c) ->1 c)))))))) =< c
313, 4, 5, 29, 30oa4to6dual 964 . . 3 (1 ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) =< c
32 leid 148 . . 3 c =< c
3331, 32letr 137 . 2 (1 ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) =< c
342, 33bltr 138 1 (c v ((a' ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c))))))) =< c
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7  1wt 8   ->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