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

Theorem mhlemlem1 874
 Description: Lemma for Lemma 7.1 of Kalmbach, p. 91.
Hypothesis
Ref Expression
mhlem.1 (ab) ≤ (cd)
Assertion
Ref Expression
mhlemlem1 (((ab) ∪ c) ∩ (a ∪ (cd))) = (ac)

Proof of Theorem mhlemlem1
StepHypRef Expression
1 leo 158 . . . . 5 a ≤ (ab)
21ler 149 . . . 4 a ≤ ((ab) ∪ c)
32lecom 180 . . 3 a C ((ab) ∪ c)
4 mhlem.1 . . . . . 6 (ab) ≤ (cd)
51, 4letr 137 . . . . 5 a ≤ (cd)
65lecom 180 . . . 4 a C (cd)
76comcom7 460 . . 3 a C (cd)
83, 7fh2 470 . 2 (((ab) ∪ c) ∩ (a ∪ (cd))) = ((((ab) ∪ c) ∩ a) ∪ (((ab) ∪ c) ∩ (cd)))
9 ancom 74 . . . 4 (((ab) ∪ c) ∩ a) = (a ∩ ((ab) ∪ c))
10 ax-a3 32 . . . . 5 ((ab) ∪ c) = (a ∪ (bc))
1110lan 77 . . . 4 (a ∩ ((ab) ∪ c)) = (a ∩ (a ∪ (bc)))
12 anabs 121 . . . 4 (a ∩ (a ∪ (bc))) = a
139, 11, 123tr 65 . . 3 (((ab) ∪ c) ∩ a) = a
14 comor1 461 . . . . 5 (cd) C c
154lecon3 157 . . . . . . 7 (cd) ≤ (ab)
1615lecom 180 . . . . . 6 (cd) C (ab)
1716comcom7 460 . . . . 5 (cd) C (ab)
1814, 17fh1rc 479 . . . 4 (((ab) ∪ c) ∩ (cd)) = (((ab) ∩ (cd)) ∪ (c ∩ (cd)))
194ortha 438 . . . . 5 ((ab) ∩ (cd)) = 0
20 anabs 121 . . . . 5 (c ∩ (cd)) = c
2119, 202or 72 . . . 4 (((ab) ∩ (cd)) ∪ (c ∩ (cd))) = (0 ∪ c)
22 or0r 103 . . . 4 (0 ∪ c) = c
2318, 21, 223tr 65 . . 3 (((ab) ∪ c) ∩ (cd)) = c
2413, 232or 72 . 2 ((((ab) ∪ c) ∩ a) ∪ (((ab) ∪ c) ∩ (cd))) = (ac)
258, 24ax-r2 36 1 (((ab) ∪ c) ∩ (a ∪ (cd))) = (ac)
 Colors of variables: term Syntax hints:   = wb 1   ≤ wle 2  ⊥ 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:  mhlemlem2  875  mhlem  876
 Copyright terms: Public domain W3C validator