QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa4uto4 Unicode version
Theorem oa4uto4 977
Description: Derivation of standard 4-variable proper OA law from "universal" variant oa4to4u2 974.
Hypothesis
Ref Expression
oa4uto4.1 ((a ->1 d) ^ ((a' ->1 d) v ((b' ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))))))) =< d
Assertion
Ref Expression
oa4uto4 ((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< d
Proof of Theorem oa4uto4
StepHypRef Expression
1 u1lem9a 777 . . . . 5 (a' ->1 d)' =< a'
21lecon1 155 . . . 4 a =< (a' ->1 d)
3 u1lem9a 777 . . . . . 6 (b' ->1 d)' =< b'
43lecon1 155 . . . . 5 b =< (b' ->1 d)
5 ax-a2 31 . . . . . . 7 ((a ^ b) v ((a ->1 d) ^ (b ->1 d))) = (((a ->1 d) ^ (b ->1 d)) v (a ^ b))
62, 4le2an 169 . . . . . . . 8 (a ^ b) =< ((a' ->1 d) ^ (b' ->1 d))
76lelor 166 . . . . . . 7 (((a ->1 d) ^ (b ->1 d)) v (a ^ b)) =< (((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d)))
85, 7bltr 138 . . . . . 6 ((a ^ b) v ((a ->1 d) ^ (b ->1 d))) =< (((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d)))
9 ax-a2 31 . . . . . . . 8 ((a ^ c) v ((a ->1 d) ^ (c ->1 d))) = (((a ->1 d) ^ (c ->1 d)) v (a ^ c))
10 u1lem9a 777 . . . . . . . . . . 11 (c' ->1 d)' =< c'
1110lecon1 155 . . . . . . . . . 10 c =< (c' ->1 d)
122, 11le2an 169 . . . . . . . . 9 (a ^ c) =< ((a' ->1 d) ^ (c' ->1 d))
1312lelor 166 . . . . . . . 8 (((a ->1 d) ^ (c ->1 d)) v (a ^ c)) =< (((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d)))
149, 13bltr 138 . . . . . . 7 ((a ^ c) v ((a ->1 d) ^ (c ->1 d))) =< (((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d)))
15 ax-a2 31 . . . . . . . 8 ((b ^ c) v ((b ->1 d) ^ (c ->1 d))) = (((b ->1 d) ^ (c ->1 d)) v (b ^ c))
164, 11le2an 169 . . . . . . . . 9 (b ^ c) =< ((b' ->1 d) ^ (c' ->1 d))
1716lelor 166 . . . . . . . 8 (((b ->1 d) ^ (c ->1 d)) v (b ^ c)) =< (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))
1815, 17bltr 138 . . . . . . 7 ((b ^ c) v ((b ->1 d) ^ (c ->1 d))) =< (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))
1914, 18le2an 169 . . . . . 6 (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))) =< ((((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d))))
208, 19le2or 168 . . . . 5 (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))) =< ((((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))))
214, 20le2an 169 . . . 4 (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))) =< ((b' ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d))))))
222, 21le2or 168 . . 3 (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))))) =< ((a' ->1 d) v ((b' ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))))))
2322lelan 167 . 2 ((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< ((a ->1 d) ^ ((a' ->1 d) v ((b' ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d))))))))
24 oa4uto4.1 . 2 ((a ->1 d) ^ ((a' ->1 d) v ((b' ->1 d) ^ ((((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d))) v ((((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d))) ^ (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))))))) =< d
2523, 24letr 137 1 ((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< d
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7   ->1 wi1 12
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131
This theorem is referenced by:  d6oa  997  axoa4  1034
  Copyright terms: Public domain W3C validator