QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  lem4 Unicode version
Theorem lem4 511
Description: Lemma 4 of Kalmbach p. 240.
Assertion
Ref Expression
lem4 (a ->3 (a ->3 b)) = (a' v b)
Proof of Theorem lem4
StepHypRef Expression
1 df-i3 46 . 2 (a ->3 (a ->3 b)) = (((a' ^ (a ->3 b)) v (a' ^ (a ->3 b)')) v (a ^ (a' v (a ->3 b))))
2 df-i3 46 . . . . . . . 8 (a ->3 b) = (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))
32lan 77 . . . . . . 7 (a' ^ (a ->3 b)) = (a' ^ (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))))
4 lea 160 . . . . . . . . . . . . 13 (a' ^ b) =< a'
5 lea 160 . . . . . . . . . . . . 13 (a' ^ b') =< a'
64, 5le2or 168 . . . . . . . . . . . 12 ((a' ^ b) v (a' ^ b')) =< (a' v a')
7 oridm 110 . . . . . . . . . . . 12 (a' v a') = a'
86, 7lbtr 139 . . . . . . . . . . 11 ((a' ^ b) v (a' ^ b')) =< a'
98lecom 180 . . . . . . . . . 10 ((a' ^ b) v (a' ^ b')) C a'
109comcom 453 . . . . . . . . 9 a' C ((a' ^ b) v (a' ^ b'))
11 lea 160 . . . . . . . . . . . 12 (a ^ (a' v b)) =< a
1211lecom 180 . . . . . . . . . . 11 (a ^ (a' v b)) C a
1312comcom 453 . . . . . . . . . 10 a C (a ^ (a' v b))
1413comcom3 454 . . . . . . . . 9 a' C (a ^ (a' v b))
1510, 14fh1 469 . . . . . . . 8 (a' ^ (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))) = ((a' ^ ((a' ^ b) v (a' ^ b'))) v (a' ^ (a ^ (a' v b))))
16 ancom 74 . . . . . . . . . . 11 ((a' ^ a) ^ (a' v b)) = ((a' v b) ^ (a' ^ a))
17 anass 76 . . . . . . . . . . 11 ((a' ^ a) ^ (a' v b)) = (a' ^ (a ^ (a' v b)))
18 dff 101 . . . . . . . . . . . . . . 15 0 = (a ^ a')
19 ancom 74 . . . . . . . . . . . . . . 15 (a ^ a') = (a' ^ a)
2018, 19ax-r2 36 . . . . . . . . . . . . . 14 0 = (a' ^ a)
2120lan 77 . . . . . . . . . . . . 13 ((a' v b) ^ 0) = ((a' v b) ^ (a' ^ a))
2221ax-r1 35 . . . . . . . . . . . 12 ((a' v b) ^ (a' ^ a)) = ((a' v b) ^ 0)
23 an0 108 . . . . . . . . . . . 12 ((a' v b) ^ 0) = 0
2422, 23ax-r2 36 . . . . . . . . . . 11 ((a' v b) ^ (a' ^ a)) = 0
2516, 17, 243tr2 64 . . . . . . . . . 10 (a' ^ (a ^ (a' v b))) = 0
2625lor 70 . . . . . . . . 9 ((a' ^ ((a' ^ b) v (a' ^ b'))) v (a' ^ (a ^ (a' v b)))) = ((a' ^ ((a' ^ b) v (a' ^ b'))) v 0)
27 or0 102 . . . . . . . . . 10 ((a' ^ ((a' ^ b) v (a' ^ b'))) v 0) = (a' ^ ((a' ^ b) v (a' ^ b')))
28 ancom 74 . . . . . . . . . . 11 (a' ^ ((a' ^ b) v (a' ^ b'))) = (((a' ^ b) v (a' ^ b')) ^ a')
298df2le2 136 . . . . . . . . . . 11 (((a' ^ b) v (a' ^ b')) ^ a') = ((a' ^ b) v (a' ^ b'))
3028, 29ax-r2 36 . . . . . . . . . 10 (a' ^ ((a' ^ b) v (a' ^ b'))) = ((a' ^ b) v (a' ^ b'))
3127, 30ax-r2 36 . . . . . . . . 9 ((a' ^ ((a' ^ b) v (a' ^ b'))) v 0) = ((a' ^ b) v (a' ^ b'))
3226, 31ax-r2 36 . . . . . . . 8 ((a' ^ ((a' ^ b) v (a' ^ b'))) v (a' ^ (a ^ (a' v b)))) = ((a' ^ b) v (a' ^ b'))
3315, 32ax-r2 36 . . . . . . 7 (a' ^ (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))) = ((a' ^ b) v (a' ^ b'))
343, 33ax-r2 36 . . . . . 6 (a' ^ (a ->3 b)) = ((a' ^ b) v (a' ^ b'))
352lor 70 . . . . . . . . 9 (a v (a ->3 b)) = (a v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))))
36 orordi 112 . . . . . . . . . 10 (a v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))) = ((a v ((a' ^ b) v (a' ^ b'))) v (a v (a ^ (a' v b))))
37 orabs 120 . . . . . . . . . . . 12 (a v (a ^ (a' v b))) = a
3837lor 70 . . . . . . . . . . 11 ((a v ((a' ^ b) v (a' ^ b'))) v (a v (a ^ (a' v b)))) = ((a v ((a' ^ b) v (a' ^ b'))) v a)
39 or32 82 . . . . . . . . . . . 12 ((a v ((a' ^ b) v (a' ^ b'))) v a) = ((a v a) v ((a' ^ b) v (a' ^ b')))
40 oridm 110 . . . . . . . . . . . . 13 (a v a) = a
4140ax-r5 38 . . . . . . . . . . . 12 ((a v a) v ((a' ^ b) v (a' ^ b'))) = (a v ((a' ^ b) v (a' ^ b')))
4239, 41ax-r2 36 . . . . . . . . . . 11 ((a v ((a' ^ b) v (a' ^ b'))) v a) = (a v ((a' ^ b) v (a' ^ b')))
4338, 42ax-r2 36 . . . . . . . . . 10 ((a v ((a' ^ b) v (a' ^ b'))) v (a v (a ^ (a' v b)))) = (a v ((a' ^ b) v (a' ^ b')))
4436, 43ax-r2 36 . . . . . . . . 9 (a v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))) = (a v ((a' ^ b) v (a' ^ b')))
4535, 44ax-r2 36 . . . . . . . 8 (a v (a ->3 b)) = (a v ((a' ^ b) v (a' ^ b')))
4645ax-r4 37 . . . . . . 7 (a v (a ->3 b))' = (a v ((a' ^ b) v (a' ^ b')))'
47 oran 87 . . . . . . . 8 (a v (a ->3 b)) = (a' ^ (a ->3 b)')'
4847con2 67 . . . . . . 7 (a v (a ->3 b))' = (a' ^ (a ->3 b)')
49 oran 87 . . . . . . . . 9 (a v ((a' ^ b) v (a' ^ b'))) = (a' ^ ((a' ^ b) v (a' ^ b'))')'
5049con2 67 . . . . . . . 8 (a v ((a' ^ b) v (a' ^ b')))' = (a' ^ ((a' ^ b) v (a' ^ b'))')
51 ancom 74 . . . . . . . 8 (a' ^ ((a' ^ b) v (a' ^ b'))') = (((a' ^ b) v (a' ^ b'))' ^ a')
5250, 51ax-r2 36 . . . . . . 7 (a v ((a' ^ b) v (a' ^ b')))' = (((a' ^ b) v (a' ^ b'))' ^ a')
5346, 48, 523tr2 64 . . . . . 6 (a' ^ (a ->3 b)') = (((a' ^ b) v (a' ^ b'))' ^ a')
5434, 532or 72 . . . . 5 ((a' ^ (a ->3 b)) v (a' ^ (a ->3 b)')) = (((a' ^ b) v (a' ^ b')) v (((a' ^ b) v (a' ^ b'))' ^ a'))
558oml2 451 . . . . 5 (((a' ^ b) v (a' ^ b')) v (((a' ^ b) v (a' ^ b'))' ^ a')) = a'
5654, 55ax-r2 36 . . . 4 ((a' ^ (a ->3 b)) v (a' ^ (a ->3 b)')) = a'
572lor 70 . . . . . . 7 (a' v (a ->3 b)) = (a' v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))))
58 ax-a3 32 . . . . . . . . 9 ((a' v ((a' ^ b) v (a' ^ b'))) v (a ^ (a' v b))) = (a' v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b))))
5958ax-r1 35 . . . . . . . 8 (a' v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))) = ((a' v ((a' ^ b) v (a' ^ b'))) v (a ^ (a' v b)))
60 orordi 112 . . . . . . . . . 10 (a' v ((a' ^ b) v (a' ^ b'))) = ((a' v (a' ^ b)) v (a' v (a' ^ b')))
61 orabs 120 . . . . . . . . . . . 12 (a' v (a' ^ b)) = a'
62 orabs 120 . . . . . . . . . . . 12 (a' v (a' ^ b')) = a'
6361, 622or 72 . . . . . . . . . . 11 ((a' v (a' ^ b)) v (a' v (a' ^ b'))) = (a' v a')
6463, 7ax-r2 36 . . . . . . . . . 10 ((a' v (a' ^ b)) v (a' v (a' ^ b'))) = a'
6560, 64ax-r2 36 . . . . . . . . 9 (a' v ((a' ^ b) v (a' ^ b'))) = a'
6665ax-r5 38 . . . . . . . 8 ((a' v ((a' ^ b) v (a' ^ b'))) v (a ^ (a' v b))) = (a' v (a ^ (a' v b)))
6759, 66ax-r2 36 . . . . . . 7 (a' v (((a' ^ b) v (a' ^ b')) v (a ^ (a' v b)))) = (a' v (a ^ (a' v b)))
6857, 67ax-r2 36 . . . . . 6 (a' v (a ->3 b)) = (a' v (a ^ (a' v b)))
69 omln 446 . . . . . 6 (a' v (a ^ (a' v b))) = (a' v b)
7068, 69ax-r2 36 . . . . 5 (a' v (a ->3 b)) = (a' v b)
7170lan 77 . . . 4 (a ^ (a' v (a ->3 b))) = (a ^ (a' v b))
7256, 712or 72 . . 3 (((a' ^ (a ->3 b)) v (a' ^ (a ->3 b)')) v (a ^ (a' v (a ->3 b)))) = (a' v (a ^ (a' v b)))
7372, 69ax-r2 36 . 2 (((a' ^ (a ->3 b)) v (a' ^ (a ->3 b)')) v (a ^ (a' v (a ->3 b)))) = (a' v b)
741, 73ax-r2 36 1 (a ->3 (a ->3 b)) = (a' v b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  0wf 9   ->3 wi3 14
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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  i0i3  512  i3i0  513  ska14  514  i3abs1  522  i3abs3  524  i3th1  543  i3th2  544  i3th3  545  i3th5  547  i3th7  549  i3th8  550  u3lem4  758  u3lem12  788  u3lemax4  796  u3lemax5  797
  Copyright terms: Public domain W3C validator