QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  fh2 Unicode version
Theorem fh2 470
Description: Foulis-Holland Theorem.
Hypotheses
Ref Expression
fh.1 a C b
fh.2 a C c
Assertion
Ref Expression
fh2 (b ^ (a v c)) = ((b ^ a) v (b ^ c))
Proof of Theorem fh2
StepHypRef Expression
1 ledi 174 . . 3 ((b ^ a) v (b ^ c)) =< (b ^ (a v c))
2 oran 87 . . . . . . . . . . 11 ((b ^ a) v (b ^ c)) = ((b ^ a)' ^ (b ^ c)')'
3 df-a 40 . . . . . . . . . . . . . 14 (b ^ a) = (b' v a')'
43con2 67 . . . . . . . . . . . . 13 (b ^ a)' = (b' v a')
54ran 78 . . . . . . . . . . . 12 ((b ^ a)' ^ (b ^ c)') = ((b' v a') ^ (b ^ c)')
65ax-r4 37 . . . . . . . . . . 11 ((b ^ a)' ^ (b ^ c)')' = ((b' v a') ^ (b ^ c)')'
72, 6ax-r2 36 . . . . . . . . . 10 ((b ^ a) v (b ^ c)) = ((b' v a') ^ (b ^ c)')'
87con2 67 . . . . . . . . 9 ((b ^ a) v (b ^ c))' = ((b' v a') ^ (b ^ c)')
98lan 77 . . . . . . . 8 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)'))
10 an4 86 . . . . . . . . 9 ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) = ((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)'))
11 fh.1 . . . . . . . . . . . . . 14 a C b
1211comcom 453 . . . . . . . . . . . . 13 b C a
1312comcom2 183 . . . . . . . . . . . 12 b C a'
1413com3ii 457 . . . . . . . . . . 11 (b ^ (b' v a')) = (b ^ a')
15 ancom 74 . . . . . . . . . . 11 (b ^ a') = (a' ^ b)
1614, 15ax-r2 36 . . . . . . . . . 10 (b ^ (b' v a')) = (a' ^ b)
1716ran 78 . . . . . . . . 9 ((b ^ (b' v a')) ^ ((a v c) ^ (b ^ c)')) = ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))
1810, 17ax-r2 36 . . . . . . . 8 ((b ^ (a v c)) ^ ((b' v a') ^ (b ^ c)')) = ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))
199, 18ax-r2 36 . . . . . . 7 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = ((a' ^ b) ^ ((a v c) ^ (b ^ c)'))
20 an4 86 . . . . . . 7 ((a' ^ b) ^ ((a v c) ^ (b ^ c)')) = ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))
2119, 20ax-r2 36 . . . . . 6 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = ((a' ^ (a v c)) ^ (b ^ (b ^ c)'))
22 ax-a1 30 . . . . . . . . . 10 a = a''
2322ax-r5 38 . . . . . . . . 9 (a v c) = (a'' v c)
2423lan 77 . . . . . . . 8 (a' ^ (a v c)) = (a' ^ (a'' v c))
25 fh.2 . . . . . . . . . 10 a C c
2625comcom3 454 . . . . . . . . 9 a' C c
2726com3ii 457 . . . . . . . 8 (a' ^ (a'' v c)) = (a' ^ c)
2824, 27ax-r2 36 . . . . . . 7 (a' ^ (a v c)) = (a' ^ c)
2928ran 78 . . . . . 6 ((a' ^ (a v c)) ^ (b ^ (b ^ c)')) = ((a' ^ c) ^ (b ^ (b ^ c)'))
3021, 29ax-r2 36 . . . . 5 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = ((a' ^ c) ^ (b ^ (b ^ c)'))
31 anass 76 . . . . 5 ((a' ^ c) ^ (b ^ (b ^ c)')) = (a' ^ (c ^ (b ^ (b ^ c)')))
3230, 31ax-r2 36 . . . 4 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = (a' ^ (c ^ (b ^ (b ^ c)')))
33 anass 76 . . . . . . . 8 ((b ^ c) ^ (b ^ c)') = (b ^ (c ^ (b ^ c)'))
3433ax-r1 35 . . . . . . 7 (b ^ (c ^ (b ^ c)')) = ((b ^ c) ^ (b ^ c)')
35 an12 81 . . . . . . 7 (c ^ (b ^ (b ^ c)')) = (b ^ (c ^ (b ^ c)'))
36 dff 101 . . . . . . 7 0 = ((b ^ c) ^ (b ^ c)')
3734, 35, 363tr1 63 . . . . . 6 (c ^ (b ^ (b ^ c)')) = 0
3837lan 77 . . . . 5 (a' ^ (c ^ (b ^ (b ^ c)'))) = (a' ^ 0)
39 an0 108 . . . . 5 (a' ^ 0) = 0
4038, 39ax-r2 36 . . . 4 (a' ^ (c ^ (b ^ (b ^ c)'))) = 0
4132, 40ax-r2 36 . . 3 ((b ^ (a v c)) ^ ((b ^ a) v (b ^ c))') = 0
421, 41oml3 452 . 2 ((b ^ a) v (b ^ c)) = (b ^ (a v c))
4342ax-r1 35 1 (b ^ (a v c)) = ((b ^ a) v (b ^ c))
Colors of variables: term
Syntax hints:   = wb 1   C wc 3  'wn 4   v wo 6   ^ wa 7  0wf 9
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-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  fh4  472  fh2r  474  fh2c  477  i3bi  496  ud3lem1a  566  ud4lem1a  577  ud4lem1b  578  ud5lem1a  586  ud5lem1b  587  ud5lem3a  591  ud5lem3b  592  u1lemle2  715  u2lemle2  716  u4lemle2  718  u21lembi  727  u1lem4  757  u4lem6  768  u3lem11  786  u3lem13b  790  2oath1  826  oale  829  mlalem  832  bi3  839  bi4  840  imp3  841  elimcons  868  mhlemlem1  874  mhlem  876  marsdenlem2  881  e2astlem1  895  oas  925
  Copyright terms: Public domain W3C validator