QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wwfh1 Unicode version
Theorem wwfh1 216
Description: Foulis-Holland Theorem (weak).
Hypotheses
Ref Expression
wwfh.1 b C a
wwfh.2 c C a
Assertion
Ref Expression
wwfh1 ((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
Proof of Theorem wwfh1
StepHypRef Expression
1 bicom 96 . 2 ((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = (((a ^ b) v (a ^ c)) == (a ^ (b v c)))
2 ledi 174 . . 3 ((a ^ b) v (a ^ c)) =< (a ^ (b v c))
3 ancom 74 . . . . . 6 (a ^ (b v c)) = ((b v c) ^ a)
4 df-a 40 . . . . . . . . 9 (a ^ b) = (a' v b')'
5 df-a 40 . . . . . . . . 9 (a ^ c) = (a' v c')'
64, 52or 72 . . . . . . . 8 ((a ^ b) v (a ^ c)) = ((a' v b')' v (a' v c')')
7 df-a 40 . . . . . . . . . 10 ((a' v b') ^ (a' v c')) = ((a' v b')' v (a' v c')')'
87ax-r1 35 . . . . . . . . 9 ((a' v b')' v (a' v c')')' = ((a' v b') ^ (a' v c'))
98con3 68 . . . . . . . 8 ((a' v b')' v (a' v c')') = ((a' v b') ^ (a' v c'))'
106, 9ax-r2 36 . . . . . . 7 ((a ^ b) v (a ^ c)) = ((a' v b') ^ (a' v c'))'
1110con2 67 . . . . . 6 ((a ^ b) v (a ^ c))' = ((a' v b') ^ (a' v c'))
123, 112an 79 . . . . 5 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = (((b v c) ^ a) ^ ((a' v b') ^ (a' v c')))
13 anass 76 . . . . . . 7 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = ((b v c) ^ (a ^ ((a' v b') ^ (a' v c'))))
14 ax-a1 30 . . . . . . . . . . . . 13 b = b''
1514ax-r1 35 . . . . . . . . . . . 12 b'' = b
16 wwfh.1 . . . . . . . . . . . 12 b C a
1715, 16bctr 181 . . . . . . . . . . 11 b'' C a
1817wwcom3ii 215 . . . . . . . . . 10 (a ^ (a' v b')) = (a ^ b')
19 ax-a1 30 . . . . . . . . . . . . 13 c = c''
2019ax-r1 35 . . . . . . . . . . . 12 c'' = c
21 wwfh.2 . . . . . . . . . . . 12 c C a
2220, 21bctr 181 . . . . . . . . . . 11 c'' C a
2322wwcom3ii 215 . . . . . . . . . 10 (a ^ (a' v c')) = (a ^ c')
2418, 232an 79 . . . . . . . . 9 ((a ^ (a' v b')) ^ (a ^ (a' v c'))) = ((a ^ b') ^ (a ^ c'))
25 anandi 114 . . . . . . . . 9 (a ^ ((a' v b') ^ (a' v c'))) = ((a ^ (a' v b')) ^ (a ^ (a' v c')))
26 anandi 114 . . . . . . . . 9 (a ^ (b' ^ c')) = ((a ^ b') ^ (a ^ c'))
2724, 25, 263tr1 63 . . . . . . . 8 (a ^ ((a' v b') ^ (a' v c'))) = (a ^ (b' ^ c'))
2827lan 77 . . . . . . 7 ((b v c) ^ (a ^ ((a' v b') ^ (a' v c')))) = ((b v c) ^ (a ^ (b' ^ c')))
2913, 28ax-r2 36 . . . . . 6 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = ((b v c) ^ (a ^ (b' ^ c')))
30 an12 81 . . . . . 6 ((b v c) ^ (a ^ (b' ^ c'))) = (a ^ ((b v c) ^ (b' ^ c')))
3129, 30ax-r2 36 . . . . 5 (((b v c) ^ a) ^ ((a' v b') ^ (a' v c'))) = (a ^ ((b v c) ^ (b' ^ c')))
3212, 31ax-r2 36 . . . 4 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = (a ^ ((b v c) ^ (b' ^ c')))
33 oran 87 . . . . . . . . . 10 (b v c) = (b' ^ c')'
3433ax-r1 35 . . . . . . . . 9 (b' ^ c')' = (b v c)
3534con3 68 . . . . . . . 8 (b' ^ c') = (b v c)'
3635lan 77 . . . . . . 7 ((b v c) ^ (b' ^ c')) = ((b v c) ^ (b v c)')
37 dff 101 . . . . . . . 8 0 = ((b v c) ^ (b v c)')
3837ax-r1 35 . . . . . . 7 ((b v c) ^ (b v c)') = 0
3936, 38ax-r2 36 . . . . . 6 ((b v c) ^ (b' ^ c')) = 0
4039lan 77 . . . . 5 (a ^ ((b v c) ^ (b' ^ c'))) = (a ^ 0)
41 an0 108 . . . . 5 (a ^ 0) = 0
4240, 41ax-r2 36 . . . 4 (a ^ ((b v c) ^ (b' ^ c'))) = 0
4332, 42ax-r2 36 . . 3 ((a ^ (b v c)) ^ ((a ^ b) v (a ^ c))') = 0
442, 43wwoml3 213 . 2 (((a ^ b) v (a ^ c)) == (a ^ (b v c))) = 1
451, 44ax-r2 36 1 ((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
Colors of variables: term
Syntax hints:   = wb 1   C wc 3  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8  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
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:  wwfh3  218
  Copyright terms: Public domain W3C validator