QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa4to4u Unicode version
Theorem oa4to4u 973
Description: A "universal" 4-OA. The hypotheses are the standard proper 4-OA and substitutions into it.
Hypotheses
Ref Expression
oa4to4u.1 ((e ->1 d) ^ (e v (f ^ (((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)))))))) =< (((e ^ d) v (f ^ d)) v (g ^ d))
oa4to4u.2 e = (a' ->1 d)
oa4to4u3 f = (b' ->1 d)
oa4to4u.4 g = (c' ->1 d)
Assertion
Ref Expression
oa4to4u ((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)))))))) =< ((((a ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (b' ->1 d))) v ((c ->1 d) ^ (c' ->1 d)))
Proof of Theorem oa4to4u
StepHypRef Expression
1 oa4to4u.1 . . 3 ((e ->1 d) ^ (e v (f ^ (((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)))))))) =< (((e ^ d) v (f ^ d)) v (g ^ d))
2 oa4to4u.2 . . . . 5 e = (a' ->1 d)
32ud1lem0b 256 . . . 4 (e ->1 d) = ((a' ->1 d) ->1 d)
4 oa4to4u3 . . . . . 6 f = (b' ->1 d)
52, 42an 79 . . . . . . . 8 (e ^ f) = ((a' ->1 d) ^ (b' ->1 d))
64ud1lem0b 256 . . . . . . . . 9 (f ->1 d) = ((b' ->1 d) ->1 d)
73, 62an 79 . . . . . . . 8 ((e ->1 d) ^ (f ->1 d)) = (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))
85, 72or 72 . . . . . . 7 ((e ^ f) v ((e ->1 d) ^ (f ->1 d))) = (((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d)))
9 oa4to4u.4 . . . . . . . . . 10 g = (c' ->1 d)
102, 92an 79 . . . . . . . . 9 (e ^ g) = ((a' ->1 d) ^ (c' ->1 d))
119ud1lem0b 256 . . . . . . . . . 10 (g ->1 d) = ((c' ->1 d) ->1 d)
123, 112an 79 . . . . . . . . 9 ((e ->1 d) ^ (g ->1 d)) = (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))
1310, 122or 72 . . . . . . . 8 ((e ^ g) v ((e ->1 d) ^ (g ->1 d))) = (((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)))
144, 92an 79 . . . . . . . . 9 (f ^ g) = ((b' ->1 d) ^ (c' ->1 d))
156, 112an 79 . . . . . . . . 9 ((f ->1 d) ^ (g ->1 d)) = (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))
1614, 152or 72 . . . . . . . 8 ((f ^ g) v ((f ->1 d) ^ (g ->1 d))) = (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)))
1713, 162an 79 . . . . . . 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) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))))
188, 172or 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) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)))))
194, 182an 79 . . . . 5 (f ^ (((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) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))))))
202, 192or 72 . . . 4 (e v (f ^ (((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) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)))))))
213, 202an 79 . . 3 ((e ->1 d) ^ (e v (f ^ (((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) ->1 d) ^ ((a' ->1 d) v ((b' ->1 d) ^ ((((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))))))))
222ran 78 . . . . 5 (e ^ d) = ((a' ->1 d) ^ d)
234ran 78 . . . . 5 (f ^ d) = ((b' ->1 d) ^ d)
2422, 232or 72 . . . 4 ((e ^ d) v (f ^ d)) = (((a' ->1 d) ^ d) v ((b' ->1 d) ^ d))
259ran 78 . . . 4 (g ^ d) = ((c' ->1 d) ^ d)
2624, 252or 72 . . 3 (((e ^ d) v (f ^ d)) v (g ^ d)) = ((((a' ->1 d) ^ d) v ((b' ->1 d) ^ d)) v ((c' ->1 d) ^ d))
271, 21, 26le3tr2 141 . 2 (((a' ->1 d) ->1 d) ^ ((a' ->1 d) v ((b' ->1 d) ^ ((((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)))))))) =< ((((a' ->1 d) ^ d) v ((b' ->1 d) ^ d)) v ((c' ->1 d) ^ d))
28 u1lem11 780 . . 3 ((a' ->1 d) ->1 d) = (a ->1 d)
29 ax-a2 31 . . . . . . 7 (((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))) = ((((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d)) v ((a' ->1 d) ^ (b' ->1 d)))
30 u1lem11 780 . . . . . . . . 9 ((b' ->1 d) ->1 d) = (b ->1 d)
3128, 302an 79 . . . . . . . 8 (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d)) = ((a ->1 d) ^ (b ->1 d))
3231ax-r5 38 . . . . . . 7 ((((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d)) v ((a' ->1 d) ^ (b' ->1 d))) = (((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d)))
3329, 32ax-r2 36 . . . . . 6 (((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))) = (((a ->1 d) ^ (b ->1 d)) v ((a' ->1 d) ^ (b' ->1 d)))
34 ax-a2 31 . . . . . . . 8 (((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) = ((((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)) v ((a' ->1 d) ^ (c' ->1 d)))
35 u1lem11 780 . . . . . . . . . 10 ((c' ->1 d) ->1 d) = (c ->1 d)
3628, 352an 79 . . . . . . . . 9 (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)) = ((a ->1 d) ^ (c ->1 d))
3736ax-r5 38 . . . . . . . 8 ((((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)) v ((a' ->1 d) ^ (c' ->1 d))) = (((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d)))
3834, 37ax-r2 36 . . . . . . 7 (((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) = (((a ->1 d) ^ (c ->1 d)) v ((a' ->1 d) ^ (c' ->1 d)))
39 ax-a2 31 . . . . . . . 8 (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) = ((((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))
4030, 352an 79 . . . . . . . . 9 (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)) = ((b ->1 d) ^ (c ->1 d))
4140ax-r5 38 . . . . . . . 8 ((((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d)) v ((b' ->1 d) ^ (c' ->1 d))) = (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))
4239, 41ax-r2 36 . . . . . . 7 (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) = (((b ->1 d) ^ (c ->1 d)) v ((b' ->1 d) ^ (c' ->1 d)))
4338, 422an 79 . . . . . 6 ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->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))))
4433, 432or 72 . . . . 5 ((((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->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)))))
4544lan 77 . . . 4 ((b' ->1 d) ^ ((((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->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))))))
4645lor 70 . . 3 ((a' ->1 d) v ((b' ->1 d) ^ ((((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->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)))))))
4728, 462an 79 . 2 (((a' ->1 d) ->1 d) ^ ((a' ->1 d) v ((b' ->1 d) ^ ((((a' ->1 d) ^ (b' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((b' ->1 d) ->1 d))) v ((((a' ->1 d) ^ (c' ->1 d)) v (((a' ->1 d) ->1 d) ^ ((c' ->1 d) ->1 d))) ^ (((b' ->1 d) ^ (c' ->1 d)) v (((b' ->1 d) ->1 d) ^ ((c' ->1 d) ->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))))))))
48 u1lemab 610 . . . . 5 ((a' ->1 d) ^ d) = ((a' ^ d) v (a'' ^ d))
49 u1lem8 776 . . . . . . 7 ((a ->1 d) ^ (a' ->1 d)) = ((a ^ d) v (a' ^ d))
50 ax-a2 31 . . . . . . 7 ((a ^ d) v (a' ^ d)) = ((a' ^ d) v (a ^ d))
51 ax-a1 30 . . . . . . . . 9 a = a''
5251ran 78 . . . . . . . 8 (a ^ d) = (a'' ^ d)
5352lor 70 . . . . . . 7 ((a' ^ d) v (a ^ d)) = ((a' ^ d) v (a'' ^ d))
5449, 50, 533tr 65 . . . . . 6 ((a ->1 d) ^ (a' ->1 d)) = ((a' ^ d) v (a'' ^ d))
5554ax-r1 35 . . . . 5 ((a' ^ d) v (a'' ^ d)) = ((a ->1 d) ^ (a' ->1 d))
5648, 55ax-r2 36 . . . 4 ((a' ->1 d) ^ d) = ((a ->1 d) ^ (a' ->1 d))
57 u1lemab 610 . . . . 5 ((b' ->1 d) ^ d) = ((b' ^ d) v (b'' ^ d))
58 u1lem8 776 . . . . . . 7 ((b ->1 d) ^ (b' ->1 d)) = ((b ^ d) v (b' ^ d))
59 ax-a2 31 . . . . . . 7 ((b ^ d) v (b' ^ d)) = ((b' ^ d) v (b ^ d))
60 ax-a1 30 . . . . . . . . 9 b = b''
6160ran 78 . . . . . . . 8 (b ^ d) = (b'' ^ d)
6261lor 70 . . . . . . 7 ((b' ^ d) v (b ^ d)) = ((b' ^ d) v (b'' ^ d))
6358, 59, 623tr 65 . . . . . 6 ((b ->1 d) ^ (b' ->1 d)) = ((b' ^ d) v (b'' ^ d))
6463ax-r1 35 . . . . 5 ((b' ^ d) v (b'' ^ d)) = ((b ->1 d) ^ (b' ->1 d))
6557, 64ax-r2 36 . . . 4 ((b' ->1 d) ^ d) = ((b ->1 d) ^ (b' ->1 d))
6656, 652or 72 . . 3 (((a' ->1 d) ^ d) v ((b' ->1 d) ^ d)) = (((a ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (b' ->1 d)))
67 u1lemab 610 . . . 4 ((c' ->1 d) ^ d) = ((c' ^ d) v (c'' ^ d))
68 u1lem8 776 . . . . . 6 ((c ->1 d) ^ (c' ->1 d)) = ((c ^ d) v (c' ^ d))
69 ax-a2 31 . . . . . 6 ((c ^ d) v (c' ^ d)) = ((c' ^ d) v (c ^ d))
70 ax-a1 30 . . . . . . . 8 c = c''
7170ran 78 . . . . . . 7 (c ^ d) = (c'' ^ d)
7271lor 70 . . . . . 6 ((c' ^ d) v (c ^ d)) = ((c' ^ d) v (c'' ^ d))
7368, 69, 723tr 65 . . . . 5 ((c ->1 d) ^ (c' ->1 d)) = ((c' ^ d) v (c'' ^ d))
7473ax-r1 35 . . . 4 ((c' ^ d) v (c'' ^ d)) = ((c ->1 d) ^ (c' ->1 d))
7567, 74ax-r2 36 . . 3 ((c' ->1 d) ^ d) = ((c ->1 d) ^ (c' ->1 d))
7666, 752or 72 . 2 ((((a' ->1 d) ^ d) v ((b' ->1 d) ^ d)) v ((c' ->1 d) ^ d)) = ((((a ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (b' ->1 d))) v ((c ->1 d) ^ (c' ->1 d)))
7727, 47, 76le3tr2 141 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)))))))) =< ((((a ->1 d) ^ (a' ->1 d)) v ((b ->1 d) ^ (b' ->1 d))) v ((c ->1 d) ^ (c' ->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:  oa4to4u2  974
  Copyright terms: Public domain W3C validator