QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa4gto4u Unicode version
Theorem oa4gto4u 976
Description: A "universal" 4-OA derived from the Godowski/Greechie form. The hypotheses are the Godowski/Greechie form of the proper 4-OA and substitutions into it.
Hypotheses
Ref Expression
oa4gto4u.1 ((e ->1 d) ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))) =< (f ->1 d)
oa4gto4u.2 f = (a ->1 d)
oa4gto4u3 e = (b ->1 d)
oa4gto4u.4 g = (c ->1 d)
Assertion
Ref Expression
oa4gto4u ((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
Proof of Theorem oa4gto4u
StepHypRef Expression
1 oa4gto4u.2 . . . 4 f = (a ->1 d)
21ud1lem0b 256 . . . . . 6 (f ->1 d) = ((a ->1 d) ->1 d)
3 u1lem12 781 . . . . . 6 ((a ->1 d) ->1 d) = (a' ->1 d)
42, 3ax-r2 36 . . . . 5 (f ->1 d) = (a' ->1 d)
5 oa4gto4u3 . . . . . . . 8 e = (b ->1 d)
65ud1lem0b 256 . . . . . . 7 (e ->1 d) = ((b ->1 d) ->1 d)
7 u1lem12 781 . . . . . . 7 ((b ->1 d) ->1 d) = (b' ->1 d)
86, 7ax-r2 36 . . . . . 6 (e ->1 d) = (b' ->1 d)
9 ancom 74 . . . . . . . . 9 (e ^ f) = (f ^ e)
101, 52an 79 . . . . . . . . 9 (f ^ e) = ((a ->1 d) ^ (b ->1 d))
119, 10ax-r2 36 . . . . . . . 8 (e ^ f) = ((a ->1 d) ^ (b ->1 d))
12 ancom 74 . . . . . . . . 9 ((e ->1 d) ^ (f ->1 d)) = ((f ->1 d) ^ (e ->1 d))
134, 82an 79 . . . . . . . . 9 ((f ->1 d) ^ (e ->1 d)) = ((a' ->1 d) ^ (b' ->1 d))
1412, 13ax-r2 36 . . . . . . . 8 ((e ->1 d) ^ (f ->1 d)) = ((a' ->1 d) ^ (b' ->1 d))
1511, 142or 72 . . . . . . 7 ((e ^ f) v ((e ->1 d) ^ (f ->1 d))) = (((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d)))
16 ancom 74 . . . . . . . 8 (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))) = (((f ^ g) v ((f ->1 d) ^ (g ->1 d))) ^ ((e ^ g) v ((e ->1 d) ^ (g ->1 d))))
17 oa4gto4u.4 . . . . . . . . . . 11 g = (c ->1 d)
181, 172an 79 . . . . . . . . . 10 (f ^ g) = ((a ->1 d) ^ (c ->1 d))
1917ud1lem0b 256 . . . . . . . . . . . 12 (g ->1 d) = ((c ->1 d) ->1 d)
20 u1lem12 781 . . . . . . . . . . . 12 ((c ->1 d) ->1 d) = (c' ->1 d)
2119, 20ax-r2 36 . . . . . . . . . . 11 (g ->1 d) = (c' ->1 d)
224, 212an 79 . . . . . . . . . 10 ((f ->1 d) ^ (g ->1 d)) = ((a' ->1 d) ^ (c' ->1 d))
2318, 222or 72 . . . . . . . . 9 ((f ^ g) v ((f ->1 d) ^ (g ->1 d))) = (((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d)))
245, 172an 79 . . . . . . . . . 10 (e ^ g) = ((b ->1 d) ^ (c ->1 d))
258, 212an 79 . . . . . . . . . 10 ((e ->1 d) ^ (g ->1 d)) = ((b' ->1 d) ^ (c' ->1 d))
2624, 252or 72 . . . . . . . . 9 ((e ^ g) v ((e ->1 d) ^ (g ->1 d))) = (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))
2723, 262an 79 . . . . . . . 8 (((f ^ g) v ((f ->1 d) ^ (g ->1 d))) ^ ((e ^ g) v ((e ->1 d) ^ (g ->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))))
2816, 27ax-r2 36 . . . . . . 7 (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->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))))
2915, 282or 72 . . . . . 6 (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->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)))))
308, 292an 79 . . . . 5 ((e ->1 d) ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->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))))))
314, 302or 72 . . . 4 ((f ->1 d) v ((e ->1 d) ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->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)))))))
321, 312an 79 . . 3 (f ^ ((f ->1 d) v ((e ->1 d) ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->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))))))))
3332ax-r1 35 . 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)))))))) = (f ^ ((f ->1 d) v ((e ->1 d) ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d))))))))
34 oa4gto4u.1 . . 3 ((e ->1 d) ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))) =< (f ->1 d)
3534oaur 930 . 2 (f ^ ((f ->1 d) v ((e ->1 d) ^ (((e ^ f) v ((e ->1 d) ^ (f ->1 d))) v (((e ^ g) v ((e ->1 d) ^ (g ->1 d))) ^ ((f ^ g) v ((f ->1 d) ^ (g ->1 d)))))))) =< d
3633, 35bltr 138 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
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:  d6oa  997  axoa4  1034
  Copyright terms: Public domain W3C validator