QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa3-u1lem Unicode version
Theorem oa3-u1lem 985
Description: Lemma for a "universal" 3-OA. Equivalence with substitution into 6-OA dual.
Assertion
Ref Expression
oa3-u1lem (1 ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) = (c v ((a' ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))))))
Proof of Theorem oa3-u1lem
StepHypRef Expression
1 ancom 74 . 2 (1 ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) = ((c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))) ^ 1)
2 an1 106 . 2 ((c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))) ^ 1) = (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))
3 lea 160 . . . . . . . . 9 (a' ^ c) =< a'
4 leo 158 . . . . . . . . 9 a' =< (a' v (a ^ c))
53, 4letr 137 . . . . . . . 8 (a' ^ c) =< (a' v (a ^ c))
6 leor 159 . . . . . . . 8 (a ^ c) =< (a' v (a ^ c))
75, 6lel2or 170 . . . . . . 7 ((a' ^ c) v (a ^ c)) =< (a' v (a ^ c))
87df-le2 131 . . . . . 6 (((a' ^ c) v (a ^ c)) v (a' v (a ^ c))) = (a' v (a ^ c))
9 ancom 74 . . . . . . . 8 (c ^ (a' ->1 c)) = ((a' ->1 c) ^ c)
10 u1lemab 610 . . . . . . . 8 ((a' ->1 c) ^ c) = ((a' ^ c) v (a'' ^ c))
11 ax-a1 30 . . . . . . . . . . 11 a = a''
1211ax-r1 35 . . . . . . . . . 10 a'' = a
1312ran 78 . . . . . . . . 9 (a'' ^ c) = (a ^ c)
1413lor 70 . . . . . . . 8 ((a' ^ c) v (a'' ^ c)) = ((a' ^ c) v (a ^ c))
159, 10, 143tr 65 . . . . . . 7 (c ^ (a' ->1 c)) = ((a' ^ c) v (a ^ c))
16 ancom 74 . . . . . . . 8 (1 ^ (a ->1 c)) = ((a ->1 c) ^ 1)
17 an1 106 . . . . . . . 8 ((a ->1 c) ^ 1) = (a ->1 c)
18 df-i1 44 . . . . . . . 8 (a ->1 c) = (a' v (a ^ c))
1916, 17, 183tr 65 . . . . . . 7 (1 ^ (a ->1 c)) = (a' v (a ^ c))
2015, 192or 72 . . . . . 6 ((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) = (((a' ^ c) v (a ^ c)) v (a' v (a ^ c)))
218, 20, 183tr1 63 . . . . 5 ((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) = (a ->1 c)
22 lea 160 . . . . . . . . . 10 (b' ^ c) =< b'
23 leo 158 . . . . . . . . . 10 b' =< (b' v (b ^ c))
2422, 23letr 137 . . . . . . . . 9 (b' ^ c) =< (b' v (b ^ c))
25 leor 159 . . . . . . . . 9 (b ^ c) =< (b' v (b ^ c))
2624, 25lel2or 170 . . . . . . . 8 ((b' ^ c) v (b ^ c)) =< (b' v (b ^ c))
2726df-le2 131 . . . . . . 7 (((b' ^ c) v (b ^ c)) v (b' v (b ^ c))) = (b' v (b ^ c))
28 ancom 74 . . . . . . . . 9 (c ^ (b' ->1 c)) = ((b' ->1 c) ^ c)
29 u1lemab 610 . . . . . . . . 9 ((b' ->1 c) ^ c) = ((b' ^ c) v (b'' ^ c))
30 ax-a1 30 . . . . . . . . . . . 12 b = b''
3130ax-r1 35 . . . . . . . . . . 11 b'' = b
3231ran 78 . . . . . . . . . 10 (b'' ^ c) = (b ^ c)
3332lor 70 . . . . . . . . 9 ((b' ^ c) v (b'' ^ c)) = ((b' ^ c) v (b ^ c))
3428, 29, 333tr 65 . . . . . . . 8 (c ^ (b' ->1 c)) = ((b' ^ c) v (b ^ c))
35 ancom 74 . . . . . . . . 9 (1 ^ (b ->1 c)) = ((b ->1 c) ^ 1)
36 an1 106 . . . . . . . . 9 ((b ->1 c) ^ 1) = (b ->1 c)
37 df-i1 44 . . . . . . . . 9 (b ->1 c) = (b' v (b ^ c))
3835, 36, 373tr 65 . . . . . . . 8 (1 ^ (b ->1 c)) = (b' v (b ^ c))
3934, 382or 72 . . . . . . 7 ((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) = (((b' ^ c) v (b ^ c)) v (b' v (b ^ c)))
4027, 39, 373tr1 63 . . . . . 6 ((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) = (b ->1 c)
41 ax-a2 31 . . . . . 6 (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))) = (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))
4240, 412an 79 . . . . 5 (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))) = ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c))))
4321, 422or 72 . . . 4 (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))))) = ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))))
4443lan 77 . . 3 ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))) = ((a' ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c))))))
4544lor 70 . 2 (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c))))))) = (c v ((a' ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))))))
461, 2, 453tr 65 1 (1 ^ (c v ((a' ->1 c) ^ (((c ^ (a' ->1 c)) v (1 ^ (a ->1 c))) v (((c ^ (b' ->1 c)) v (1 ^ (b ->1 c))) ^ (((a' ->1 c) ^ (b' ->1 c)) v ((a ->1 c) ^ (b ->1 c)))))))) = (c v ((a' ->1 c) ^ ((a ->1 c) v ((b ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))))))
Colors of variables: term
Syntax hints:   = wb 1  '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:  oa3-u1  991
  Copyright terms: Public domain W3C validator