Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  wwfh1 GIF 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 ∩ (bc)) ≡ ((ab) ∪ (ac))) = 1

Proof of Theorem wwfh1
StepHypRef Expression
1 bicom 96 . 2 ((a ∩ (bc)) ≡ ((ab) ∪ (ac))) = (((ab) ∪ (ac)) ≡ (a ∩ (bc)))
2 ledi 174 . . 3 ((ab) ∪ (ac)) ≤ (a ∩ (bc))
3 ancom 74 . . . . . 6 (a ∩ (bc)) = ((bc) ∩ a)
4 df-a 40 . . . . . . . . 9 (ab) = (ab )
5 df-a 40 . . . . . . . . 9 (ac) = (ac )
64, 52or 72 . . . . . . . 8 ((ab) ∪ (ac)) = ((ab ) ∪ (ac ) )
7 df-a 40 . . . . . . . . . 10 ((ab ) ∩ (ac )) = ((ab ) ∪ (ac ) )
87ax-r1 35 . . . . . . . . 9 ((ab ) ∪ (ac ) ) = ((ab ) ∩ (ac ))
98con3 68 . . . . . . . 8 ((ab ) ∪ (ac ) ) = ((ab ) ∩ (ac ))
106, 9ax-r2 36 . . . . . . 7 ((ab) ∪ (ac)) = ((ab ) ∩ (ac ))
1110con2 67 . . . . . 6 ((ab) ∪ (ac)) = ((ab ) ∩ (ac ))
123, 112an 79 . . . . 5 ((a ∩ (bc)) ∩ ((ab) ∪ (ac)) ) = (((bc) ∩ a) ∩ ((ab ) ∩ (ac )))
13 anass 76 . . . . . . 7 (((bc) ∩ a) ∩ ((ab ) ∩ (ac ))) = ((bc) ∩ (a ∩ ((ab ) ∩ (ac ))))
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 ∩ (ab )) = (ab )
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 ∩ (ac )) = (ac )
2418, 232an 79 . . . . . . . . 9 ((a ∩ (ab )) ∩ (a ∩ (ac ))) = ((ab ) ∩ (ac ))
25 anandi 114 . . . . . . . . 9 (a ∩ ((ab ) ∩ (ac ))) = ((a ∩ (ab )) ∩ (a ∩ (ac )))
26 anandi 114 . . . . . . . . 9 (a ∩ (bc )) = ((ab ) ∩ (ac ))
2724, 25, 263tr1 63 . . . . . . . 8 (a ∩ ((ab ) ∩ (ac ))) = (a ∩ (bc ))
2827lan 77 . . . . . . 7 ((bc) ∩ (a ∩ ((ab ) ∩ (ac )))) = ((bc) ∩ (a ∩ (bc )))
2913, 28ax-r2 36 . . . . . 6 (((bc) ∩ a) ∩ ((ab ) ∩ (ac ))) = ((bc) ∩ (a ∩ (bc )))
30 an12 81 . . . . . 6 ((bc) ∩ (a ∩ (bc ))) = (a ∩ ((bc) ∩ (bc )))
3129, 30ax-r2 36 . . . . 5 (((bc) ∩ a) ∩ ((ab ) ∩ (ac ))) = (a ∩ ((bc) ∩ (bc )))
3212, 31ax-r2 36 . . . 4 ((a ∩ (bc)) ∩ ((ab) ∪ (ac)) ) = (a ∩ ((bc) ∩ (bc )))
33 oran 87 . . . . . . . . . 10 (bc) = (bc )
3433ax-r1 35 . . . . . . . . 9 (bc ) = (bc)
3534con3 68 . . . . . . . 8 (bc ) = (bc)
3635lan 77 . . . . . . 7 ((bc) ∩ (bc )) = ((bc) ∩ (bc) )
37 dff 101 . . . . . . . 8 0 = ((bc) ∩ (bc) )
3837ax-r1 35 . . . . . . 7 ((bc) ∩ (bc) ) = 0
3936, 38ax-r2 36 . . . . . 6 ((bc) ∩ (bc )) = 0
4039lan 77 . . . . 5 (a ∩ ((bc) ∩ (bc ))) = (a ∩ 0)
41 an0 108 . . . . 5 (a ∩ 0) = 0
4240, 41ax-r2 36 . . . 4 (a ∩ ((bc) ∩ (bc ))) = 0
4332, 42ax-r2 36 . . 3 ((a ∩ (bc)) ∩ ((ab) ∪ (ac)) ) = 0
442, 43wwoml3 213 . 2 (((ab) ∪ (ac)) ≡ (a ∩ (bc))) = 1
451, 44ax-r2 36 1 ((a ∩ (bc)) ≡ ((ab) ∪ (ac))) = 1
 Colors of variables: term Syntax hints:   = wb 1   C wc 3  ⊥ wn 4   ≡ tb 5   ∪ 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