QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  fh1 Unicode version
Theorem fh1 469
Description: Foulis-Holland Theorem.
Hypotheses
Ref Expression
fh.1 a C b
fh.2 a C c
Assertion
Ref Expression
fh1 (a ^ (b v c)) = ((a ^ b) v (a ^ c))
Proof of Theorem fh1
StepHypRef Expression
1 ledi 174 . . 3 ((a ^ b) v (a ^ c)) =< (a ^ (b v c))
2 ancom 74 . . . . . 6 (a ^ (b v c)) = ((b v c) ^ a)
3 df-a 40 . . . . . . . . 9 (a ^ b) = (a' v b')'
4 df-a 40 . . . . . . . . 9 (a ^ c) = (a' v c')'
53, 42or 72 . . . . . . . 8 ((a ^ b) v (a ^ c)) = ((a' v b')' v (a' v c')')
6 df-a 40 . . . . . . . . . 10 ((a' v b') ^ (a' v c')) = ((a' v b')' v (a' v c')')'
76ax-r1 35 . . . . . . . . 9 ((a' v b')' v (a' v c')')' = ((a' v b') ^ (a' v c'))
87con3 68 . . . . . . . 8 ((a' v b')' v (a' v c')') = ((a' v b') ^ (a' v c'))'
95, 8ax-r2 36 . . . . . . 7 ((a ^ b) v (a ^ c)) = ((a' v b') ^ (a' v c'))'
109con2 67 . . . . . 6 ((a ^ b) v (a ^ c))' = ((a' v b') ^ (a' v c'))
112, 102an 79 . . . . 5 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = (((b v c) ^ a) ^ ((a' v b') ^ (a' v c')))
12 anass 76 . . . . . . 7 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = ((b v c) ^ (a ^ ((a' v b') ^ (a' v c'))))
13 fh.1 . . . . . . . . . . . 12 a C b
1413comcom2 183 . . . . . . . . . . 11 a C b'
1514com3ii 457 . . . . . . . . . 10 (a ^ (a' v b')) = (a ^ b')
16 fh.2 . . . . . . . . . . . 12 a C c
1716comcom2 183 . . . . . . . . . . 11 a C c'
1817com3ii 457 . . . . . . . . . 10 (a ^ (a' v c')) = (a ^ c')
1915, 182an 79 . . . . . . . . 9 ((a ^ (a' v b')) ^ (a ^ (a' v c'))) = ((a ^ b') ^ (a ^ c'))
20 anandi 114 . . . . . . . . 9 (a ^ ((a' v b') ^ (a' v c'))) = ((a ^ (a' v b')) ^ (a ^ (a' v c')))
21 anandi 114 . . . . . . . . 9 (a ^ (b' ^ c')) = ((a ^ b') ^ (a ^ c'))
2219, 20, 213tr1 63 . . . . . . . 8 (a ^ ((a' v b') ^ (a' v c'))) = (a ^ (b' ^ c'))
2322lan 77 . . . . . . 7 ((b v c) ^ (a ^ ((a' v b') ^ (a' v c')))) = ((b v c) ^ (a ^ (b' ^ c')))
2412, 23ax-r2 36 . . . . . 6 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = ((b v c) ^ (a ^ (b' ^ c')))
25 an12 81 . . . . . 6 ((b v c) ^ (a ^ (b' ^ c'))) = (a ^ ((b v c) ^ (b' ^ c')))
2624, 25ax-r2 36 . . . . 5 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = (a ^ ((b v c) ^ (b' ^ c')))
2711, 26ax-r2 36 . . . 4 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = (a ^ ((b v c) ^ (b' ^ c')))
28 oran 87 . . . . . . . . . 10 (b v c) = (b' ^ c')'
2928ax-r1 35 . . . . . . . . 9 (b' ^ c')' = (b v c)
3029con3 68 . . . . . . . 8 (b' ^ c') = (b v c)'
3130lan 77 . . . . . . 7 ((b v c) ^ (b' ^ c')) = ((b v c) ^ (b v c)')
32 dff 101 . . . . . . . 8 0 = ((b v c) ^ (b v c)')
3332ax-r1 35 . . . . . . 7 ((b v c) ^ (b v c)') = 0
3431, 33ax-r2 36 . . . . . 6 ((b v c) ^ (b' ^ c')) = 0
3534lan 77 . . . . 5 (a ^ ((b v c) ^ (b' ^ c'))) = (a ^ 0)
36 an0 108 . . . . 5 (a ^ 0) = 0
3735, 36ax-r2 36 . . . 4 (a ^ ((b v c) ^ (b' ^ c'))) = 0
3827, 37ax-r2 36 . . 3 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = 0
391, 38oml3 452 . 2 ((a ^ b) v (a ^ c)) = (a ^ (b v c))
4039ax-r1 35 1 (a ^ (b v c)) = ((a ^ b) v (a ^ 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:  fh3  471  fh1r  473  com2or  483  nbdi  486  oml4  487  gsth  489  i3bi  496  dfi3b  499  i3lem1  504  lem4  511  i3abs3  524  i3orlem7  558  i3orlem8  559  ud3lem1b  567  ud4lem1a  577  ud4lem1d  580  u5lemaa  604  u3lemc4  703  u4lemle2  718  u5lemle2  719  u5lembi  725  u12lembi  726  u24lem  770  u3lem13a  789  bi1o1a  798  3vded21  817  3vded3  819  comanblem2  871  mhlem1  877  mlaconjolem  885  lem4.6.2e1  1080
  Copyright terms: Public domain W3C validator