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

Theorem vneulem13 1143
Description: Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96 (Contributed by NM, 31-Mar-2011.)
Hypothesis
Ref Expression
vneulem13.1 ((ab) ∩ (cd)) = 0
Assertion
Ref Expression
vneulem13 ((cd) ∪ ((ab) ∩ ((cd) ∪ (ab)))) = ((cd) ∪ (ab))

Proof of Theorem vneulem13
StepHypRef Expression
1 leao1 162 . . . . . . 7 (ab) ≤ (ab)
2 leid 148 . . . . . . 7 (ab) ≤ (ab)
31, 2ler2an 173 . . . . . 6 (ab) ≤ ((ab) ∩ (ab))
4 lear 161 . . . . . 6 ((ab) ∩ (ab)) ≤ (ab)
53, 4lebi 145 . . . . 5 (ab) = ((ab) ∩ (ab))
65lor 70 . . . 4 ((cd) ∪ (ab)) = ((cd) ∪ ((ab) ∩ (ab)))
76lan 77 . . 3 ((ab) ∩ ((cd) ∪ (ab))) = ((ab) ∩ ((cd) ∪ ((ab) ∩ (ab))))
8 mldual 1124 . . 3 ((ab) ∩ ((cd) ∪ ((ab) ∩ (ab)))) = (((ab) ∩ (cd)) ∪ ((ab) ∩ (ab)))
9 vneulem13.1 . . . . 5 ((ab) ∩ (cd)) = 0
104, 3lebi 145 . . . . 5 ((ab) ∩ (ab)) = (ab)
119, 102or 72 . . . 4 (((ab) ∩ (cd)) ∪ ((ab) ∩ (ab))) = (0 ∪ (ab))
12 or0r 103 . . . 4 (0 ∪ (ab)) = (ab)
1311, 12tr 62 . . 3 (((ab) ∩ (cd)) ∪ ((ab) ∩ (ab))) = (ab)
147, 8, 133tr 65 . 2 ((ab) ∩ ((cd) ∪ (ab))) = (ab)
1514lor 70 1 ((cd) ∪ ((ab) ∩ ((cd) ∪ (ab)))) = ((cd) ∪ (ab))
Colors of variables: term
Syntax hints:   = wb 1  wo 6  wa 7  0wf 9
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-ml 1122
This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131
This theorem is referenced by:  vneulem14  1144
  Copyright terms: Public domain W3C validator