[Lattice L46-7]Home PageHome Quantum Logic Explorer < Previous   Next >
Related theorems
Unicode version
Theorem u4lem5 764
Description: Lemma for unified implication study.
Assertion
Ref Expression
u4lem5 (a ->4 (a ->4 b)) = ((a' ^ b') v b)
Proof of Theorem u4lem5
StepHypRef Expression
1 df-i4 47 . 2 (a ->4 (a ->4 b)) = (((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) v ((a' v (a ->4 b)) ^ (a ->4 b)'))
2 ancom 74 . . . . . . 7 (a ^ (a ->4 b)) = ((a ->4 b) ^ a)
3 u4lemaa 603 . . . . . . 7 ((a ->4 b) ^ a) = (a ^ b)
42, 3ax-r2 36 . . . . . 6 (a ^ (a ->4 b)) = (a ^ b)
5 ancom 74 . . . . . . 7 (a' ^ (a ->4 b)) = ((a ->4 b) ^ a')
6 u4lemana 608 . . . . . . 7 ((a ->4 b) ^ a') = ((a' ^ b) v (a' ^ b'))
75, 6ax-r2 36 . . . . . 6 (a' ^ (a ->4 b)) = ((a' ^ b) v (a' ^ b'))
84, 72or 72 . . . . 5 ((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) = ((a ^ b) v ((a' ^ b) v (a' ^ b')))
9 ax-a3 32 . . . . . 6 (((a ^ b) v (a' ^ b)) v (a' ^ b')) = ((a ^ b) v ((a' ^ b) v (a' ^ b')))
109ax-r1 35 . . . . 5 ((a ^ b) v ((a' ^ b) v (a' ^ b'))) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
118, 10ax-r2 36 . . . 4 ((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) = (((a ^ b) v (a' ^ b)) v (a' ^ b'))
12 ax-a2 31 . . . . . . 7 (a' v (a ->4 b)) = ((a ->4 b) v a')
13 u4lemona 628 . . . . . . 7 ((a ->4 b) v a') = (a' v b)
1412, 13ax-r2 36 . . . . . 6 (a' v (a ->4 b)) = (a' v b)
15 ud4lem0c 280 . . . . . 6 (a ->4 b)' = (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))
1614, 152an 79 . . . . 5 ((a' v (a ->4 b)) ^ (a ->4 b)') = ((a' v b) ^ (((a' v b') ^ (a v b')) ^ ((a ^ b') v b)))
17 ancom 74 . . . . . 6 ((a' v b) ^ (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))) = ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (a' v b))
18 anass 76 . . . . . . 7 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (a' v b)) = (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ (a' v b)))
19 comor1 461 . . . . . . . . . . . . 13 (a' v b) C a'
2019comcom7 460 . . . . . . . . . . . 12 (a' v b) C a
21 comor2 462 . . . . . . . . . . . . 13 (a' v b) C b
2221comcom2 183 . . . . . . . . . . . 12 (a' v b) C b'
2320, 22com2an 484 . . . . . . . . . . 11 (a' v b) C (a ^ b')
2423, 21fh1r 473 . . . . . . . . . 10 (((a ^ b') v b) ^ (a' v b)) = (((a ^ b') ^ (a' v b)) v (b ^ (a' v b)))
25 ax-a2 31 . . . . . . . . . . 11 (((a ^ b') ^ (a' v b)) v (b ^ (a' v b))) = ((b ^ (a' v b)) v ((a ^ b') ^ (a' v b)))
26 leor 159 . . . . . . . . . . . . . 14 b =< (a' v b)
2726df2le2 136 . . . . . . . . . . . . 13 (b ^ (a' v b)) = b
28 oran2 92 . . . . . . . . . . . . . . 15 (a' v b) = (a ^ b')'
2928lan 77 . . . . . . . . . . . . . 14 ((a ^ b') ^ (a' v b)) = ((a ^ b') ^ (a ^ b')')
30 dff 101 . . . . . . . . . . . . . . 15 0 = ((a ^ b') ^ (a ^ b')')
3130ax-r1 35 . . . . . . . . . . . . . 14 ((a ^ b') ^ (a ^ b')') = 0
3229, 31ax-r2 36 . . . . . . . . . . . . 13 ((a ^ b') ^ (a' v b)) = 0
3327, 322or 72 . . . . . . . . . . . 12 ((b ^ (a' v b)) v ((a ^ b') ^ (a' v b))) = (b v 0)
34 or0 102 . . . . . . . . . . . 12 (b v 0) = b
3533, 34ax-r2 36 . . . . . . . . . . 11 ((b ^ (a' v b)) v ((a ^ b') ^ (a' v b))) = b
3625, 35ax-r2 36 . . . . . . . . . 10 (((a ^ b') ^ (a' v b)) v (b ^ (a' v b))) = b
3724, 36ax-r2 36 . . . . . . . . 9 (((a ^ b') v b) ^ (a' v b)) = b
3837lan 77 . . . . . . . 8 (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ (a' v b))) = (((a' v b') ^ (a v b')) ^ b)
39 ancom 74 . . . . . . . 8 (((a' v b') ^ (a v b')) ^ b) = (b ^ ((a' v b') ^ (a v b')))
4038, 39ax-r2 36 . . . . . . 7 (((a' v b') ^ (a v b')) ^ (((a ^ b') v b) ^ (a' v b))) = (b ^ ((a' v b') ^ (a v b')))
4118, 40ax-r2 36 . . . . . 6 ((((a' v b') ^ (a v b')) ^ ((a ^ b') v b)) ^ (a' v b)) = (b ^ ((a' v b') ^ (a v b')))
4217, 41ax-r2 36 . . . . 5 ((a' v b) ^ (((a' v b') ^ (a v b')) ^ ((a ^ b') v b))) = (b ^ ((a' v b') ^ (a v b')))
4316, 42ax-r2 36 . . . 4 ((a' v (a ->4 b)) ^ (a ->4 b)') = (b ^ ((a' v b') ^ (a v b')))
4411, 432or 72 . . 3 (((a ^ (a ->4 b)) v (a' ^ (a ->4 b))) v ((a' v (a ->4 b)) ^ (a ->4 b)')) = ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (b ^ ((a' v b') ^ (a v b'))))
45 comanr2 465 . . . . . . 7 b C (a ^ b)
46 comanr2 465 . . . . . . 7 b C (a' ^ b)
4745, 46com2or 483 . . . . . 6 b C ((a ^ b) v (a' ^ b))
48 comanr2 465 . . . . . . 7 b' C (a' ^ b')
4948comcom6 459 . . . . . 6 b C (a' ^ b')
5047, 49com2or 483 . . . . 5 b C (((a ^ b) v (a' ^ b)) v (a' ^ b'))
51 comorr2 463 . . . . . . 7 b' C (a' v b')
52 comorr2 463 . . . . . . 7 b' C (a v b')
5351, 52com2an 484 . . . . . 6 b' C ((a' v b') ^ (a v b'))
5453comcom6 459 . . . . 5 b C ((a' v b') ^ (a v b'))
5550, 54fh4 472 . . . 4 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v (b ^ ((a' v b') ^ (a v b')))) = (((((a ^ b) v (a' ^ b)) v (a' ^ b')) v b) ^ ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v ((a' v b') ^ (a v b'))))
56 or32 82 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v b) = ((((a ^ b) v (a' ^ b)) v b) v (a' ^ b'))
57 lear 161 . . . . . . . . . 10 (a ^ b) =< b
58 lear 161 . . . . . . . . . 10 (a' ^ b) =< b
5957, 58lel2or 170 . . . . . . . . 9 ((a ^ b) v (a' ^ b)) =< b
6059df-le2 131 . . . . . . . 8 (((a ^ b) v (a' ^ b)) v b) = b
6160ax-r5 38 . . . . . . 7 ((((a ^ b) v (a' ^ b)) v b) v (a' ^ b')) = (b v (a' ^ b'))
6256, 61ax-r2 36 . . . . . 6 ((((a ^ b) v (a' ^ b)) v (a' ^ b')) v b) = (b v (a' ^ b'))
63 comor1 461 . . . . . . . . . . . 12 (a' v b') C a'
6463comcom7 460 . . . . . . . . . . 11 (a' v b') C a
65 comor2 462 . . . . . . . . . . . 12 (a' v b') C b'
6665comcom7 460 . . . . . . . . . . 11 (a' v b') C b
6764, 66com2an 484 . . . . . . . . . 10 (a' v b') C (a ^ b)
6863, 66com2an 484 . . . . . . . . . 10 (a' v b') C (a' ^ b)
6967, 68com2or 483 . . . . . . . . 9 (a' v b') C ((a ^ b) v (a' ^ b))
7063, 65com2an 484 . . . . . . . . 9