QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  marsdenlem2 GIF version

Theorem marsdenlem2 881
Description: Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
Hypotheses
Ref Expression
marsden.1 a C b
marsden.2 b C c
marsden.3 c C d
marsden.4 d C a
Assertion
Ref Expression
marsdenlem2 ((cd) ∩ (bc )) = (((bc) ∪ (cd)) ∪ (bd))

Proof of Theorem marsdenlem2
StepHypRef Expression
1 ancom 74 . 2 ((cd) ∩ (bc )) = ((bc ) ∩ (cd))
2 comorr 184 . . . 4 c C (cd)
32comcom3 454 . . 3 c C (cd)
4 marsden.2 . . . . 5 b C c
54comcom4 455 . . . 4 b C c
65comcom 453 . . 3 c C b
73, 6fh2rc 480 . 2 ((bc ) ∩ (cd)) = ((b ∩ (cd)) ∪ (c ∩ (cd)))
86comcom6 459 . . . . 5 c C b
9 marsden.3 . . . . 5 c C d
108, 9fh2 470 . . . 4 (b ∩ (cd)) = ((bc) ∪ (bd))
11 comid 187 . . . . . . 7 c C c
1211comcom2 183 . . . . . 6 c C c
1312, 9fh2 470 . . . . 5 (c ∩ (cd)) = ((cc) ∪ (cd))
14 dff 101 . . . . . . . 8 0 = (cc )
15 ancom 74 . . . . . . . 8 (cc ) = (cc)
1614, 15ax-r2 36 . . . . . . 7 0 = (cc)
1716ax-r5 38 . . . . . 6 (0 ∪ (cd)) = ((cc) ∪ (cd))
1817ax-r1 35 . . . . 5 ((cc) ∪ (cd)) = (0 ∪ (cd))
19 or0r 103 . . . . 5 (0 ∪ (cd)) = (cd)
2013, 18, 193tr 65 . . . 4 (c ∩ (cd)) = (cd)
2110, 202or 72 . . 3 ((b ∩ (cd)) ∪ (c ∩ (cd))) = (((bc) ∪ (bd)) ∪ (cd))
22 or32 82 . . 3 (((bc) ∪ (bd)) ∪ (cd)) = (((bc) ∪ (cd)) ∪ (bd))
2321, 22ax-r2 36 . 2 ((b ∩ (cd)) ∪ (c ∩ (cd))) = (((bc) ∪ (cd)) ∪ (bd))
241, 7, 233tr 65 1 ((cd) ∩ (bc )) = (((bc) ∪ (cd)) ∪ (bd))
Colors of variables: term
Syntax hints:   = wb 1   C wc 3   wn 4  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: (None)
  Copyright terms: Public domain W3C validator