QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ska4 Unicode version
Theorem ska4 433
Description: Soundness theorem for Kalmbach's quantum propositional logic axiom KA4.
Assertion
Ref Expression
ska4 ((a == b)' v ((a ^ c) == (b ^ c))) = 1
Proof of Theorem ska4
StepHypRef Expression
1 dfnb 95 . . 3 (a == b)' = ((a v b) ^ (a' v b'))
2 dfb 94 . . 3 ((a ^ c) == (b ^ c)) = (((a ^ c) ^ (b ^ c)) v ((a ^ c)' ^ (b ^ c)'))
31, 22or 72 . 2 ((a == b)' v ((a ^ c) == (b ^ c))) = (((a v b) ^ (a' v b')) v (((a ^ c) ^ (b ^ c)) v ((a ^ c)' ^ (b ^ c)')))
4 ax-a2 31 . 2 (((a v b) ^ (a' v b')) v (((a ^ c) ^ (b ^ c)) v ((a ^ c)' ^ (b ^ c)'))) = ((((a ^ c) ^ (b ^ c)) v ((a ^ c)' ^ (b ^ c)')) v ((a v b) ^ (a' v b')))
5 ax-a3 32 . . 3 ((((a ^ c) ^ (b ^ c)) v ((a ^ c)' ^ (b ^ c)')) v ((a v b) ^ (a' v b'))) = (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v ((a v b) ^ (a' v b'))))
6 le1 146 . . . . . . . . 9 (((a ^ c)' ^ (b ^ c)') v (a v b)) =< 1
7 df-t 41 . . . . . . . . . . 11 1 = ((a' ^ b') v (a' ^ b')')
8 oran 87 . . . . . . . . . . . . 13 (a v b) = (a' ^ b')'
98lor 70 . . . . . . . . . . . 12 ((a' ^ b') v (a v b)) = ((a' ^ b') v (a' ^ b')')
109ax-r1 35 . . . . . . . . . . 11 ((a' ^ b') v (a' ^ b')') = ((a' ^ b') v (a v b))
117, 10ax-r2 36 . . . . . . . . . 10 1 = ((a' ^ b') v (a v b))
12 lea 160 . . . . . . . . . . . . 13 (a ^ c) =< a
1312lecon 154 . . . . . . . . . . . 12 a' =< (a ^ c)'
14 lea 160 . . . . . . . . . . . . 13 (b ^ c) =< b
1514lecon 154 . . . . . . . . . . . 12 b' =< (b ^ c)'
1613, 15le2an 169 . . . . . . . . . . 11 (a' ^ b') =< ((a ^ c)' ^ (b ^ c)')
1716leror 152 . . . . . . . . . 10 ((a' ^ b') v (a v b)) =< (((a ^ c)' ^ (b ^ c)') v (a v b))
1811, 17bltr 138 . . . . . . . . 9 1 =< (((a ^ c)' ^ (b ^ c)') v (a v b))
196, 18lebi 145 . . . . . . . 8 (((a ^ c)' ^ (b ^ c)') v (a v b)) = 1
2019ran 78 . . . . . . 7 ((((a ^ c)' ^ (b ^ c)') v (a v b)) ^ (((a ^ c)' ^ (b ^ c)') v (a' v b'))) = (1 ^ (((a ^ c)' ^ (b ^ c)') v (a' v b')))
21 ancom 74 . . . . . . 7 (1 ^ (((a ^ c)' ^ (b ^ c)') v (a' v b'))) = ((((a ^ c)' ^ (b ^ c)') v (a' v b')) ^ 1)
22 an1 106 . . . . . . 7 ((((a ^ c)' ^ (b ^ c)') v (a' v b')) ^ 1) = (((a ^ c)' ^ (b ^ c)') v (a' v b'))
2320, 21, 223tr 65 . . . . . 6 ((((a ^ c)' ^ (b ^ c)') v (a v b)) ^ (((a ^ c)' ^ (b ^ c)') v (a' v b'))) = (((a ^ c)' ^ (b ^ c)') v (a' v b'))
2423lor 70 . . . . 5 (((a ^ c) ^ (b ^ c)) v ((((a ^ c)' ^ (b ^ c)') v (a v b)) ^ (((a ^ c)' ^ (b ^ c)') v (a' v b')))) = (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v (a' v b')))
25 le1 146 . . . . . 6 (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v (a' v b'))) =< 1
26 df-t 41 . . . . . . . 8 1 = (((a ^ b) ^ c) v ((a ^ b) ^ c)')
27 anandir 115 . . . . . . . . 9 ((a ^ b) ^ c) = ((a ^ c) ^ (b ^ c))
28 oran3 93 . . . . . . . . . . . . 13 (a' v b') = (a ^ b)'
2928ax-r5 38 . . . . . . . . . . . 12 ((a' v b') v c') = ((a ^ b)' v c')
30 oran3 93 . . . . . . . . . . . 12 ((a ^ b)' v c') = ((a ^ b) ^ c)'
3129, 30ax-r2 36 . . . . . . . . . . 11 ((a' v b') v c') = ((a ^ b) ^ c)'
3231ax-r1 35 . . . . . . . . . 10 ((a ^ b) ^ c)' = ((a' v b') v c')
33 ax-a2 31 . . . . . . . . . 10 ((a' v b') v c') = (c' v (a' v b'))
3432, 33ax-r2 36 . . . . . . . . 9 ((a ^ b) ^ c)' = (c' v (a' v b'))
3527, 342or 72 . . . . . . . 8 (((a ^ b) ^ c) v ((a ^ b) ^ c)') = (((a ^ c) ^ (b ^ c)) v (c' v (a' v b')))
3626, 35ax-r2 36 . . . . . . 7 1 = (((a ^ c) ^ (b ^ c)) v (c' v (a' v b')))
37 lear 161 . . . . . . . . . . 11 (a ^ c) =< c
3837lecon 154 . . . . . . . . . 10 c' =< (a ^ c)'
39 lear 161 . . . . . . . . . . 11 (b ^ c) =< c
4039lecon 154 . . . . . . . . . 10 c' =< (b ^ c)'
4138, 40ler2an 173 . . . . . . . . 9 c' =< ((a ^ c)' ^ (b ^ c)')
4241leror 152 . . . . . . . 8 (c' v (a' v b')) =< (((a ^ c)' ^ (b ^ c)') v (a' v b'))
4342lelor 166 . . . . . . 7 (((a ^ c) ^ (b ^ c)) v (c' v (a' v b'))) =< (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v (a' v b')))
4436, 43bltr 138 . . . . . 6 1 =< (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v (a' v b')))
4525, 44lebi 145 . . . . 5 (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v (a' v b'))) = 1
4624, 45ax-r2 36 . . . 4 (((a ^ c) ^ (b ^ c)) v ((((a ^ c)' ^ (b ^ c)') v (a v b)) ^ (((a ^ c)' ^ (b ^ c)') v (a' v b')))) = 1
47 wlea 388 . . . . . . . . . . 11 ((a ^ c) =<2 a) = 1
48 wleo 387 . . . . . . . . . . 11 (a =<2 (a v b)) = 1
4947, 48wletr 396 . . . . . . . . . 10 ((a ^ c) =<2 (a v b)) = 1
5049wlecom 409 . . . . . . . . 9 C ((a ^ c), (a v b)) = 1
5150wcomcom 414 . . . . . . . 8 C ((a v b), (a ^ c)) = 1
5251wcomcom2 415 . . . . . . 7 C ((a v b), (a ^ c)') = 1
53 wlea 388 . . . . . . . . . . 11 ((b ^ c) =<2 b) = 1
54 wleo 387 . . . . . . . . . . . 12 (b =<2 (b v a)) = 1
55 ax-a2 31 . . . . . . . . . . . . 13 (b v a) = (a v b)
5655bi1 118 . . . . . . . . . . . 12 ((b v a) == (a v b)) = 1
5754, 56wlbtr 398 . . . . . . . . . . 11 (b =<2 (a v b)) = 1
5853, 57wletr 396 . . . . . . . . . 10 ((b ^ c) =<2 (a v b)) = 1
5958wlecom 409 . . . . . . . . 9 C ((b ^ c), (a v b)) = 1
6059wcomcom 414 . . . . . . . 8 C ((a v b), (b ^ c)) = 1
6160wcomcom2 415 . . . . . . 7 C ((a v b), (b ^ c)') = 1
6252, 61wcom2an 428 . . . . . 6 C ((a v b), ((a ^ c)' ^ (b ^ c)')) = 1
63 wcomorr 412 . . . . . . . . 9 C (a, (a v b)) = 1
6463wcomcom 414 . . . . . . . 8 C ((a v b), a) = 1
6564wcomcom2 415 . . . . . . 7 C ((a v b), a') = 1
66 wcomorr 412 . . . . . . . . . 10 C (b, (b v a)) = 1
6766, 56wcbtr 411 . . . . . . . . 9 C (b, (a v b)) = 1
6867wcomcom 414 . . . . . . . 8 C ((a v b), b) = 1
6968wcomcom2 415 . . . . . . 7 C ((a v b), b') = 1
7065, 69wcom2or 427 . . . . . 6 C ((a v b), (a' v b')) = 1
7162, 70wfh4 426 . . . . 5 ((((a ^ c)' ^ (b ^ c)') v ((a v b) ^ (a' v b'))) == ((((a ^ c)' ^ (b ^ c)') v (a v b)) ^ (((a ^ c)' ^ (b ^ c)') v (a' v b')))) = 1
7271wlor 368 . . . 4 ((((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v ((a v b) ^ (a' v b')))) == (((a ^ c) ^ (b ^ c)) v ((((a ^ c)' ^ (b ^ c)') v (a v b)) ^ (((a ^ c)' ^ (b ^ c)') v (a' v b'))))) = 1
7346, 72wwbmpr 206 . . 3 (((a ^ c) ^ (b ^ c)) v (((a ^ c)' ^ (b ^ c)') v ((a v b) ^ (a' v b')))) = 1
745, 73ax-r2 36 . 2 ((((a ^ c) ^ (b ^ c)) v ((a ^ c)' ^ (b ^ c)')) v ((a v b) ^ (a' v b'))) = 1
753, 4, 743tr 65 1 ((a == b)' v ((a ^ c) == (b ^ c))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8
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-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134
This theorem is referenced by:  wom2  434  u3lemax4  796
  Copyright terms: Public domain W3C validator