QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  marsdenlem2 Unicode version
Theorem marsdenlem2 881
Description: Lemma for Marsden-Herman distributive law.
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 ((c v d) ^ (b' v c')) = (((b' ^ c) v (c' ^ d)) v (b' ^ d))
Proof of Theorem marsdenlem2
StepHypRef Expression
1 ancom 74 . 2 ((c v d) ^ (b' v c')) = ((b' v c') ^ (c v d))
2 comorr 184 . . . 4 c C (c v d)
32comcom3 454 . . 3 c' C (c v d)
4 marsden.2 . . . . 5 b C c
54comcom4 455 . . . 4 b' C c'
65comcom 453 . . 3 c' C b'
73, 6fh2rc 480 . 2 ((b' v c') ^ (c v d)) = ((b' ^ (c v d)) v (c' ^ (c v d)))
86comcom6 459 . . . . 5 c C b'
9 marsden.3 . . . . 5 c C d
108, 9fh2 470 . . . 4 (b' ^ (c v d)) = ((b' ^ c) v (b' ^ d))
11 comid 187 . . . . . . 7 c C c
1211comcom2 183 . . . . . 6 c C c'
1312, 9fh2 470 . . . . 5 (c' ^ (c v d)) = ((c' ^ c) v (c' ^ d))
14 dff 101 . . . . . . . 8 0 = (c ^ c')
15 ancom 74 . . . . . . . 8 (c ^ c') = (c' ^ c)
1614, 15ax-r2 36 . . . . . . 7 0 = (c' ^ c)
1716ax-r5 38 . . . . . 6 (0 v (c' ^ d)) = ((c' ^ c) v (c' ^ d))
1817ax-r1 35 . . . . 5 ((c' ^ c) v (c' ^ d)) = (0 v (c' ^ d))
19 or0r 103 . . . . 5 (0 v (c' ^ d)) = (c' ^ d)
2013, 18, 193tr 65 . . . 4 (c' ^ (c v d)) = (c' ^ d)
2110, 202or 72 . . 3 ((b' ^ (c v d)) v (c' ^ (c v d))) = (((b' ^ c) v (b' ^ d)) v (c' ^ d))
22 or32 82 . . 3 (((b' ^ c) v (b' ^ d)) v (c' ^ d)) = (((b' ^ c) v (c' ^ d)) v (b' ^ d))
2321, 22ax-r2 36 . 2 ((b' ^ (c v d)) v (c' ^ (c v d))) = (((b' ^ c) v (c' ^ d)) v (b' ^ d))
241, 7, 233tr 65 1 ((c v d) ^ (b' v c')) = (((b' ^ c) v (c' ^ d)) v (b' ^ d))
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: (None)
  Copyright terms: Public domain W3C validator