QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa4uto4g Unicode version
Theorem oa4uto4g 975
Description: Derivation of "Godowski/Greechie" 4-variable proper OA law variant from "universal" variant oa4to4u2 974.
Hypotheses
Ref Expression
oa4uto4g.1 ((b' ->1 d) ^ ((b'' ->1 d) v ((a'' ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b'' ->1 d) ^ (a'' ->1 d))) v ((((b' ->1 d) ^ (c' ->1 d)) v ((b'' ->1 d) ^ (c'' ->1 d))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d)))))))) =< d
oa4uto4g.4 h = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
Assertion
Ref Expression
oa4uto4g ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h)) =< (b ->1 d)
Proof of Theorem oa4uto4g
StepHypRef Expression
1 ancom 74 . . . . . . . 8 (a ^ b) = (b ^ a)
2 ancom 74 . . . . . . . 8 ((a ->1 d) ^ (b ->1 d)) = ((b ->1 d) ^ (a ->1 d))
31, 22or 72 . . . . . . 7 ((a ^ b) v ((a ->1 d) ^ (b ->1 d))) = ((b ^ a) v ((b ->1 d) ^ (a ->1 d)))
43ax-r5 38 . . . . . 6 (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h) = (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)
54lan 77 . . . . 5 ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h)) = ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h))
65lor 70 . . . 4 ((b ->1 d) v ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h))) = ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)))
76lan 77 . . 3 (b ^ ((b ->1 d) v ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h)))) = (b ^ ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h))))
8 u1lem9a 777 . . . . . 6 (b' ->1 d)' =< b'
98lecon1 155 . . . . 5 b =< (b' ->1 d)
10 u1lem9a 777 . . . . . . . . . . 11 (a' ->1 d)' =< a'
1110lecon1 155 . . . . . . . . . 10 a =< (a' ->1 d)
129, 11le2an 169 . . . . . . . . 9 (b ^ a) =< ((b' ->1 d) ^ (a' ->1 d))
1312leror 152 . . . . . . . 8 ((b ^ a) v ((b ->1 d) ^ (a ->1 d))) =< (((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->1 d)))
14 oa4uto4g.4 . . . . . . . . 9 h = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))
15 u1lem9a 777 . . . . . . . . . . . . 13 (c' ->1 d)' =< c'
1615lecon1 155 . . . . . . . . . . . 12 c =< (c' ->1 d)
1711, 16le2an 169 . . . . . . . . . . 11 (a ^ c) =< ((a' ->1 d) ^ (c' ->1 d))
1817leror 152 . . . . . . . . . 10 ((a ^ c) v ((a ->1 d) ^ (c ->1 d))) =< (((a' ->1 d) ^ (c' ->1 d)) v ((a ->1 d) ^ (c ->1 d)))
199, 16le2an 169 . . . . . . . . . . 11 (b ^ c) =< ((b' ->1 d) ^ (c' ->1 d))
2019leror 152 . . . . . . . . . 10 ((b ^ c) v ((b ->1 d) ^ (c ->1 d))) =< (((b' ->1 d) ^ (c' ->1 d)) v ((b ->1 d) ^ (c ->1 d)))
2118, 20le2an 169 . . . . . . . . 9 (((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))))
2214, 21bltr 138 . . . . . . . 8 h =< ((((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))))
2313, 22le2or 168 . . . . . . 7 (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h) =< ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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)))))
2423lelan 167 . . . . . 6 ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)) =< ((a ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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))))))
2524lelor 166 . . . . 5 ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h))) =< ((b ->1 d) v ((a ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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)))))))
269, 25le2an 169 . . . 4 (b ^ ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)))) =< ((b' ->1 d) ^ ((b ->1 d) v ((a ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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))))))))
27 ax-a1 30 . . . . . . . 8 b = b''
2827ud1lem0b 256 . . . . . . 7 (b ->1 d) = (b'' ->1 d)
29 ax-a1 30 . . . . . . . . 9 a = a''
3029ud1lem0b 256 . . . . . . . 8 (a ->1 d) = (a'' ->1 d)
3128, 302an 79 . . . . . . . . . 10 ((b ->1 d) ^ (a ->1 d)) = ((b'' ->1 d) ^ (a'' ->1 d))
3231lor 70 . . . . . . . . 9 (((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->1 d))) = (((b' ->1 d) ^ (a' ->1 d)) v ((b'' ->1 d) ^ (a'' ->1 d)))
33 ancom 74 . . . . . . . . . 10 ((((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)))) = ((((b' ->1 d) ^ (c' ->1 d)) v ((b ->1 d) ^ (c ->1 d))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a ->1 d) ^ (c ->1 d))))
34 ax-a1 30 . . . . . . . . . . . . . 14 c = c''
3534ud1lem0b 256 . . . . . . . . . . . . 13 (c ->1 d) = (c'' ->1 d)
3628, 352an 79 . . . . . . . . . . . 12 ((b ->1 d) ^ (c ->1 d)) = ((b'' ->1 d) ^ (c'' ->1 d))
3736lor 70 . . . . . . . . . . 11 (((b' ->1 d) ^ (c' ->1 d)) v ((b ->1 d) ^ (c ->1 d))) = (((b' ->1 d) ^ (c' ->1 d)) v ((b'' ->1 d) ^ (c'' ->1 d)))
3830, 352an 79 . . . . . . . . . . . 12 ((a ->1 d) ^ (c ->1 d)) = ((a'' ->1 d) ^ (c'' ->1 d))
3938lor 70 . . . . . . . . . . 11 (((a' ->1 d) ^ (c' ->1 d)) v ((a ->1 d) ^ (c ->1 d))) = (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d)))
4037, 392an 79 . . . . . . . . . 10 ((((b' ->1 d) ^ (c' ->1 d)) 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))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d))))
4133, 40ax-r2 36 . . . . . . . . 9 ((((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)))) = ((((b' ->1 d) ^ (c' ->1 d)) v ((b'' ->1 d) ^ (c'' ->1 d))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d))))
4232, 412or 72 . . . . . . . 8 ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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))))) = ((((b' ->1 d) ^ (a' ->1 d)) v ((b'' ->1 d) ^ (a'' ->1 d))) v ((((b' ->1 d) ^ (c' ->1 d)) v ((b'' ->1 d) ^ (c'' ->1 d))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d)))))
4330, 422an 79 . . . . . . 7 ((a ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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)))))) = ((a'' ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b'' ->1 d) ^ (a'' ->1 d))) v ((((b' ->1 d) ^ (c' ->1 d)) v ((b'' ->1 d) ^ (c'' ->1 d))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d))))))
4428, 432or 72 . . . . . 6 ((b ->1 d) v ((a ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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))))))) = ((b'' ->1 d) v ((a'' ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b'' ->1 d) ^ (a'' ->1 d))) v ((((b' ->1 d) ^ (c' ->1 d)) v ((b'' ->1 d) ^ (c'' ->1 d))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d)))))))
4544lan 77 . . . . 5 ((b' ->1 d) ^ ((b ->1 d) v ((a ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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)))))))) = ((b' ->1 d) ^ ((b'' ->1 d) v ((a'' ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b'' ->1 d) ^ (a'' ->1 d))) v ((((b' ->1 d) ^ (c' ->1 d)) v ((b'' ->1 d) ^ (c'' ->1 d))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d))))))))
46 oa4uto4g.1 . . . . 5 ((b' ->1 d) ^ ((b'' ->1 d) v ((a'' ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b'' ->1 d) ^ (a'' ->1 d))) v ((((b' ->1 d) ^ (c' ->1 d)) v ((b'' ->1 d) ^ (c'' ->1 d))) ^ (((a' ->1 d) ^ (c' ->1 d)) v ((a'' ->1 d) ^ (c'' ->1 d)))))))) =< d
4745, 46bltr 138 . . . 4 ((b' ->1 d) ^ ((b ->1 d) v ((a ->1 d) ^ ((((b' ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (a ->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
4826, 47letr 137 . . 3 (b ^ ((b ->1 d) v ((a ->1 d) ^ (((b ^ a) v ((b ->1 d) ^ (a ->1 d))) v h)))) =< d
497, 48bltr 138 . 2 (b ^ ((b ->1 d) v ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h)))) =< d
5049oau 929 1 ((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v h)) =< (b ->1 d)
Colors of variables: term
Syntax hints:   = wb 1   =< 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-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:  4oa  1039
  Copyright terms: Public domain W3C validator