[Lattice L46-7]Home PageHome Quantum Logic Explorer < Previous   Next >
Related theorems
Unicode version
Theorem oa3-1lem 962
Description: Lemma for 3-OA(1). Equivalence with substitution into 6-OA dual.
Assertion
Ref Expression
oa3-1lem (1 ^ (0 v (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))))) = (a ^ ((a ->1 c) v ((b ->1 c) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))
Proof of Theorem oa3-1lem
StepHypRef Expression
1 ancom 68 . 2 (1 ^ (0 v (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))))) = ((0 v (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))) ^ 1)
2 an1 98 . 2 ((0 v (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))) ^ 1) = (0 v (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))))
3 ax-a2 30 . . 3 (0 v (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))) = ((a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) v 0)
4 or0 94 . . 3 ((a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) v 0) = (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))
5 ancom 68 . . . . . . . . 9 (0 ^ a) = (a ^ 0)
6 an0 100 . . . . . . . . 9 (a ^ 0) = 0
75, 6ax-r2 35 . . . . . . . 8 (0 ^ a) = 0
8 ancom 68 . . . . . . . . 9 (1 ^ (a ->1 c)) = ((a ->1 c) ^ 1)
9 an1 98 . . . . . . . . 9 ((a ->1 c) ^ 1) = (a ->1 c)
108, 9ax-r2 35 . . . . . . . 8 (1 ^ (a ->1 c)) = (a ->1 c)
117, 102or 67 . . . . . . 7 ((0 ^ a) v (1 ^ (a ->1 c))) = (0 v (a ->1 c))
12 ax-a2 30 . . . . . . 7 (0 v (a ->1 c)) = ((a ->1 c) v 0)
13 or0 94 . . . . . . 7 ((a ->1 c) v 0) = (a ->1 c)
1411, 12, 133tr 62 . . . . . 6 ((0 ^ a) v (1 ^ (a ->1 c))) = (a ->1 c)
1514ax-r5 37 . . . . 5 (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))) = ((a ->1 c) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))
16 ax-a2 30 . . . . . . . 8 ((0 ^ b) v (1 ^ (b ->1 c))) = ((1 ^ (b ->1 c)) v (0 ^ b))
17 ancom 68 . . . . . . . . . 10 (1 ^ (b ->1 c)) = ((b ->1 c) ^ 1)
18 an1 98 . . . . . . . . . 10 ((b ->1 c) ^ 1) = (b ->1 c)
1917, 18ax-r2 35 . . . . . . . . 9 (1 ^ (b ->1 c)) = (b ->1 c)
20 ancom 68 . . . . . . . . . 10 (0 ^ b) = (b ^ 0)
21 an0 100 . . . . . . . . . 10 (b ^ 0) = 0
2220, 21ax-r2 35 . . . . . . . . 9 (0 ^ b) = 0
2319, 222or 67 . . . . . . . 8 ((1 ^ (b ->1 c)) v (0 ^ b)) = ((b ->1 c) v 0)
24 or0 94 . . . . . . . 8 ((b ->1 c) v 0) = (b ->1 c)
2516, 23, 243tr 62 . . . . . . 7 ((0 ^ b) v (1 ^ (b ->1 c))) = (b ->1 c)
2625ran 71 . . . . . 6 (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))) = ((b ->1 c) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))
2726lor 66 . . . . 5 ((a ->1 c) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))) = ((a ->1 c) v ((b ->1 c) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))
2815, 27ax-r2 35 . . . 4 (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))) = ((a ->1 c) v ((b ->1 c) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))
2928lan 70 . . 3 (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))) = (a ^ ((a ->1 c) v ((b ->1 c) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))
303, 4, 293tr 62 . 2 (0 v (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))) = (a ^ ((a ->1 c) v ((b ->1 c) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))
311, 2, 303tr 62 1 (1 ^ (0 v (a ^ (((0 ^ a) v (1 ^ (a ->1 c))) v (((0 ^ b) v (1 ^ (b ->1 c))) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c)))))))) = (a ^ ((a ->1 c) v ((b ->1 c) ^ ((a ^ b) v ((a ->1 c) ^ (b ->1 c))))))
Colors of variables: term
Syntax hints:   = wb 1   v wo 6   ^ wa 7  1wt 9  0wf 10   ->1 wi1 13
This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37
This theorem depends on definitions:  df-a 39  df-t 40  df-f 41
metamath.org