QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3-u2 Unicode version
Theorem oa3-u2 992
Description: Derivation of a "universal" 3-OA. The hypothesis is a substitution instance of the proper 4-OA.
Hypothesis
Ref Expression
oa3-u2.1 (((a' ->1 c) ->1 c) ^ ((a' ->1 c) v (c ^ ((((a' ->1 c) ^ c) v (((a' ->1 c) ->1 c) ^ (c ->1 c))) v ((((a' ->1 c) ^ (b' ->1 c)) v (((a' ->1 c) ->1 c) ^ ((b' ->1 c) ->1 c))) ^ ((c ^ (b' ->1 c)) v ((c ->1 c) ^ ((b' ->1 c) ->1 c)))))))) =< c
Assertion
Ref Expression
oa3-u2 ((a ->1 c) ^ ((a' ->1 c) v (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-u2
StepHypRef Expression
1 oa3-u2lem 986 . . 3 ((a ->1 c) ^ ((a' ->1 c) v (c ^ ((((a' ->1 c) ^ c) v ((a ->1 c) ^ 1)) v ((((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b' ->1 c)) v (1 ^ (b ->1 c)))))))) = ((a ->1 c) ^ ((a' ->1 c) v (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 ((a ->1 c) ^ ((a' ->1 c) v (c ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))))))) = ((a ->1 c) ^ ((a' ->1 c) v (c ^ ((((a' ->1 c) ^ c) v ((a ->1 c) ^ 1)) v ((((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))))))))
3 u1lem9ab 779 . . 3 (a' ->1 c)' =< (a ->1 c)
4 le1 146 . . 3 c' =< 1
5 u1lem9ab 779 . . 3 (b' ->1 c)' =< (b ->1 c)
6 or32 82 . . . . 5 ((((a' ->1 c) ^ (a ->1 c)) v (c ^ 1)) v ((b' ->1 c) ^ (b ->1 c))) = ((((a' ->1 c) ^ (a ->1 c)) v ((b' ->1 c) ^ (b ->1 c))) v (c ^ 1))
7 ancom 74 . . . . . . . 8 ((a' ->1 c) ^ (a ->1 c)) = ((a ->1 c) ^ (a' ->1 c))
8 u1lem8 776 . . . . . . . 8 ((a ->1 c) ^ (a' ->1 c)) = ((a ^ c) v (a' ^ c))
97, 8ax-r2 36 . . . . . . 7 ((a' ->1 c) ^ (a ->1 c)) = ((a ^ c) v (a' ^ c))
10 ancom 74 . . . . . . . 8 ((b' ->1 c) ^ (b ->1 c)) = ((b ->1 c) ^ (b' ->1 c))
11 u1lem8 776 . . . . . . . 8 ((b ->1 c) ^ (b' ->1 c)) = ((b ^ c) v (b' ^ c))
1210, 11ax-r2 36 . . . . . . 7 ((b' ->1 c) ^ (b ->1 c)) = ((b ^ c) v (b' ^ c))
139, 122or 72 . . . . . 6 (((a' ->1 c) ^ (a ->1 c)) v ((b' ->1 c) ^ (b ->1 c))) = (((a ^ c) v (a' ^ c)) v ((b ^ c) v (b' ^ c)))
14 an1 106 . . . . . 6 (c ^ 1) = c
1513, 142or 72 . . . . 5 ((((a' ->1 c) ^ (a ->1 c)) v ((b' ->1 c) ^ (b ->1 c))) v (c ^ 1)) = ((((a ^ c) v (a' ^ c)) v ((b ^ c) v (b' ^ c))) v c)
16 lear 161 . . . . . . . 8 (a ^ c) =< c
17 lear 161 . . . . . . . 8 (a' ^ c) =< c
1816, 17lel2or 170 . . . . . . 7 ((a ^ c) v (a' ^ c)) =< c
19 lear 161 . . . . . . . 8 (b ^ c) =< c
20 lear 161 . . . . . . . 8 (b' ^ c) =< c
2119, 20lel2or 170 . . . . . . 7 ((b ^ c) v (b' ^ c)) =< c
2218, 21lel2or 170 . . . . . 6 (((a ^ c) v (a' ^ c)) v ((b ^ c) v (b' ^ c))) =< c
2322df-le2 131 . . . . 5 ((((a ^ c) v (a' ^ c)) v ((b ^ c) v (b' ^ c))) v c) = c
246, 15, 233tr 65 . . . 4 ((((a' ->1 c) ^ (a ->1 c)) v (c ^ 1)) v ((b' ->1 c) ^ (b ->1 c))) = c
2524ax-r1 35 . . 3 c = ((((a' ->1 c) ^ (a ->1 c)) v (c ^ 1)) v ((b' ->1 c) ^ (b ->1 c)))
26 oa3-u2.1 . . 3 (((a' ->1 c) ->1 c) ^ ((a' ->1 c) v (c ^ ((((a' ->1 c) ^ c) v (((a' ->1 c) ->1 c) ^ (c ->1 c))) v ((((a' ->1 c) ^ (b' ->1 c)) v (((a' ->1 c) ->1 c) ^ ((b' ->1 c) ->1 c))) ^ ((c ^ (b' ->1 c)) v ((c ->1 c) ^ ((b' ->1 c) ->1 c)))))))) =< c
273, 4, 5, 25, 26oa4to6dual 964 . 2 ((a ->1 c) ^ ((a' ->1 c) v (c ^ ((((a' ->1 c) ^ c) v ((a ->1 c) ^ 1)) v ((((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))) ^ ((c ^ (b' ->1 c)) v (1 ^ (b ->1 c)))))))) =< c
282, 27bltr 138 1 ((a ->1 c) ^ ((a' ->1 c) v (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