QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  mh Unicode version
Theorem mh 879
Description: Marsden-Herman distributive law. Lemma 7.2 of Kalmbach, p. 91.
Hypotheses
Ref Expression
mh.1 a C c
mh.2 a C d
mh.3 b C c
mh.4 b C d
Assertion
Ref Expression
mh ((a v c) ^ (b v d)) = (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))
Proof of Theorem mh
StepHypRef Expression
1 leao1 162 . . . . . 6 (a ^ b) =< (a v c)
2 leao2 163 . . . . . 6 (a ^ b) =< (b v d)
31, 2ler2an 173 . . . . 5 (a ^ b) =< ((a v c) ^ (b v d))
4 leao1 162 . . . . . 6 (a ^ d) =< (a v c)
5 leao4 165 . . . . . 6 (a ^ d) =< (b v d)
64, 5ler2an 173 . . . . 5 (a ^ d) =< ((a v c) ^ (b v d))
73, 6lel2or 170 . . . 4 ((a ^ b) v (a ^ d)) =< ((a v c) ^ (b v d))
8 leao3 164 . . . . . 6 (c ^ b) =< (a v c)
9 leao2 163 . . . . . 6 (c ^ b) =< (b v d)
108, 9ler2an 173 . . . . 5 (c ^ b) =< ((a v c) ^ (b v d))
11 leao3 164 . . . . . 6 (c ^ d) =< (a v c)
12 leao4 165 . . . . . 6 (c ^ d) =< (b v d)
1311, 12ler2an 173 . . . . 5 (c ^ d) =< ((a v c) ^ (b v d))
1410, 13lel2or 170 . . . 4 ((c ^ b) v (c ^ d)) =< ((a v c) ^ (b v d))
157, 14lel2or 170 . . 3 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d))) =< ((a v c) ^ (b v d))
16 anass 76 . . . . . . 7 ((((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) ^ ((a ^ b) v (c ^ d))') = (((a v c) ^ (b v d)) ^ (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))'))
1716ax-r1 35 . . . . . 6 (((a v c) ^ (b v d)) ^ (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))')) = ((((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) ^ ((a ^ b) v (c ^ d))')
18 an4 86 . . . . . . . . 9 (((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) = (((a v c) ^ (c' v b')) ^ ((b v d) ^ (a' v d')))
19 mh.1 . . . . . . . . . 10 a C c
20 mh.2 . . . . . . . . . 10 a C d
21 mh.3 . . . . . . . . . 10 b C c
22 mh.4 . . . . . . . . . 10 b C d
2319, 20, 21, 22mhlem2 878 . . . . . . . . 9 (((a v c) ^ (c' v b')) ^ ((b v d) ^ (a' v d'))) = (((a ^ c') ^ (b ^ d')) v ((c ^ b') ^ (d ^ a')))
2418, 23ax-r2 36 . . . . . . . 8 (((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) = (((a ^ c') ^ (b ^ d')) v ((c ^ b') ^ (d ^ a')))
25 lea 160 . . . . . . . . . . 11 (a ^ c') =< a
26 lea 160 . . . . . . . . . . 11 (b ^ d') =< b
2725, 26le2an 169 . . . . . . . . . 10 ((a ^ c') ^ (b ^ d')) =< (a ^ b)
28 leo 158 . . . . . . . . . 10 (a ^ b) =< ((a ^ b) v (c ^ d))
2927, 28letr 137 . . . . . . . . 9 ((a ^ c') ^ (b ^ d')) =< ((a ^ b) v (c ^ d))
30 lea 160 . . . . . . . . . . 11 (c ^ b') =< c
31 lea 160 . . . . . . . . . . 11 (d ^ a') =< d
3230, 31le2an 169 . . . . . . . . . 10 ((c ^ b') ^ (d ^ a')) =< (c ^ d)
33 leor 159 . . . . . . . . . 10 (c ^ d) =< ((a ^ b) v (c ^ d))
3432, 33letr 137 . . . . . . . . 9 ((c ^ b') ^ (d ^ a')) =< ((a ^ b) v (c ^ d))
3529, 34lel2or 170 . . . . . . . 8 (((a ^ c') ^ (b ^ d')) v ((c ^ b') ^ (d ^ a'))) =< ((a ^ b) v (c ^ d))
3624, 35bltr 138 . . . . . . 7 (((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) =< ((a ^ b) v (c ^ d))
3736leran 153 . . . . . 6 ((((a v c) ^ (b v d)) ^ ((c' v b') ^ (a' v d'))) ^ ((a ^ b) v (c ^ d))') =< (((a ^ b) v (c ^ d)) ^ ((a ^ b) v (c ^ d))')
3817, 37bltr 138 . . . . 5 (((a v c) ^ (b v d)) ^ (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))')) =< (((a ^ b) v (c ^ d)) ^ ((a ^ b) v (c ^ d))')
39 anor3 90 . . . . . . . 8 (((c ^ b) v (a ^ d))' ^ ((a ^ b) v (c ^ d))') = (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))'
4039ax-r1 35 . . . . . . 7 (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))' = (((c ^ b) v (a ^ d))' ^ ((a ^ b) v (c ^ d))')
41 ax-a2 31 . . . . . . . . 9 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d))) = (((c ^ b) v (c ^ d)) v ((a ^ b) v (a ^ d)))
42 or12 80 . . . . . . . . . . . 12 ((c ^ d) v ((a ^ b) v (a ^ d))) = ((a ^ b) v ((c ^ d) v (a ^ d)))
43 ax-a3 32 . . . . . . . . . . . . 13 (((a ^ b) v (c ^ d)) v (a ^ d)) = ((a ^ b) v ((c ^ d) v (a ^ d)))
4443ax-r1 35 . . . . . . . . . . . 12 ((a ^ b) v ((c ^ d) v (a ^ d))) = (((a ^ b) v (c ^ d)) v (a ^ d))
45 ax-a2 31 . . . . . . . . . . . 12 (((a ^ b) v (c ^ d)) v (a ^ d)) = ((a ^ d) v ((a ^ b) v (c ^ d)))
4642, 44, 453tr 65 . . . . . . . . . . 11 ((c ^ d) v ((a ^ b) v (a ^ d))) = ((a ^ d) v ((a ^ b) v (c ^ d)))
4746lor 70 . . . . . . . . . 10 ((c ^ b) v ((c ^ d) v ((a ^ b) v (a ^ d)))) = ((c ^ b) v ((a ^ d) v ((a ^ b) v (c ^ d))))
48 ax-a3 32 . . . . . . . . . 10 (((c ^ b) v (c ^ d)) v ((a ^ b) v (a ^ d))) = ((c ^ b) v ((c ^ d) v ((a ^ b) v (a ^ d))))
49 ax-a3 32 . . . . . . . . . 10 (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d))) = ((c ^ b) v ((a ^ d) v ((a ^ b) v (c ^ d))))
5047, 48, 493tr1 63 . . . . . . . . 9 (((c ^ b) v (c ^ d)) v ((a ^ b) v (a ^ d))) = (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))
5141, 50ax-r2 36 . . . . . . . 8 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d))) = (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))
5251ax-r4 37 . . . . . . 7 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))' = (((c ^ b) v (a ^ d)) v ((a ^ b) v (c ^ d)))'
53 oran3 93 . . . . . . . . . 10 (c' v b') = (c ^ b)'
54 oran3 93 . . . . . . . . . 10 (a' v d') = (a ^ d)'
5553, 542an 79 . . . . . . . . 9 ((c' v b') ^ (a' v d')) = ((c ^ b)' ^ (a ^ d)')
56 anor3 90 . . . . . . . . 9 ((c ^ b)' ^ (a ^ d)') = ((c ^ b) v (a ^ d))'
5755, 56ax-r2 36 . . . . . . . 8 ((c' v b') ^ (a' v d')) = ((c ^ b) v (a ^ d))'
5857ran 78 . . . . . . 7 (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))') = (((c ^ b) v (a ^ d))' ^ ((a ^ b) v (c ^ d))')
5940, 52, 583tr1 63 . . . . . 6 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))' = (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))')
6059lan 77 . . . . 5 (((a v c) ^ (b v d)) ^ (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))') = (((a v c) ^ (b v d)) ^ (((c' v b') ^ (a' v d')) ^ ((a ^ b) v (c ^ d))'))
61 dff 101 . . . . 5 0 = (((a ^ b) v (c ^ d)) ^ ((a ^ b) v (c ^ d))')
6238, 60, 61le3tr1 140 . . . 4 (((a v c) ^ (b v d)) ^ (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))') =< 0
63 le0 147 . . . 4 0 =< (((a v c) ^ (b v d)) ^ (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))')
6462, 63lebi 145 . . 3 (((a v c) ^ (b v d)) ^ (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d)))') = 0
6515, 64oml3 452 . 2 (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ d))) = ((a v c) ^ (b v d))
6665ax-r1 35 1 ((a v c) ^ (b v d)) = (((a ^ b) v (a ^ d)) v ((c ^ b) v (c ^ 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:  mh2  884  mlaconjo  886
  Copyright terms: Public domain W3C validator