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

Theorem mhlem 876
Description: Lemma 7.1 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
Hypothesis
Ref Expression
mhlem.1 (ab) ≤ (cd)
Assertion
Ref Expression
mhlem ((ac) ∩ (bd)) = ((ab) ∪ (cd))

Proof of Theorem mhlem
StepHypRef Expression
1 comor1 461 . . . . . . 7 (ab) C a
2 comor2 462 . . . . . . 7 (ab) C b
31, 2com2an 484 . . . . . 6 (ab) C (ab)
4 mhlem.1 . . . . . . . 8 (ab) ≤ (cd)
54lecom 180 . . . . . . 7 (ab) C (cd)
65comcom7 460 . . . . . 6 (ab) C (cd)
73, 6fh1r 473 . . . . 5 (((ab) ∪ (cd)) ∩ (ab)) = (((ab) ∩ (ab)) ∪ ((cd) ∩ (ab)))
8 comor1 461 . . . . . . 7 (cd) C c
9 comor2 462 . . . . . . 7 (cd) C d
108, 9com2an 484 . . . . . 6 (cd) C (cd)
11 leao1 162 . . . . . . . . . 10 (ab) ≤ (ab)
1211, 4letr 137 . . . . . . . . 9 (ab) ≤ (cd)
1312lecom 180 . . . . . . . 8 (ab) C (cd)
1413comcom7 460 . . . . . . 7 (ab) C (cd)
1514comcom 453 . . . . . 6 (cd) C (ab)
1610, 15fh2rc 480 . . . . 5 (((ab) ∪ (cd)) ∩ (cd)) = (((ab) ∩ (cd)) ∪ ((cd) ∩ (cd)))
177, 162or 72 . . . 4 ((((ab) ∪ (cd)) ∩ (ab)) ∪ (((ab) ∪ (cd)) ∩ (cd))) = ((((ab) ∩ (ab)) ∪ ((cd) ∩ (ab))) ∪ (((ab) ∩ (cd)) ∪ ((cd) ∩ (cd))))
1811lerr 150 . . . . . . . 8 (ab) ≤ ((cd) ∪ (ab))
1918lecom 180 . . . . . . 7 (ab) C ((cd) ∪ (ab))
2014, 19fh3 471 . . . . . 6 ((ab) ∪ ((cd) ∩ ((cd) ∪ (ab)))) = (((ab) ∪ (cd)) ∩ ((ab) ∪ ((cd) ∪ (ab))))
21 id 59 . . . . . . . 8 ((ac) ∩ (bd)) = ((ac) ∩ (bd))
224mhlemlem1 874 . . . . . . . . 9 (((ab) ∪ c) ∩ (a ∪ (cd))) = (ac)
234mhlemlem2 875 . . . . . . . . 9 (((ab) ∪ d) ∩ (b ∪ (cd))) = (bd)
2422, 232an 79 . . . . . . . 8 ((((ab) ∪ c) ∩ (a ∪ (cd))) ∩ (((ab) ∪ d) ∩ (b ∪ (cd)))) = ((ac) ∩ (bd))
2521, 21, 243tr1 63 . . . . . . 7 ((ac) ∩ (bd)) = ((((ab) ∪ c) ∩ (a ∪ (cd))) ∩ (((ab) ∪ d) ∩ (b ∪ (cd))))
26 an4 86 . . . . . . . 8 ((((ab) ∪ c) ∩ (a ∪ (cd))) ∩ (((ab) ∪ d) ∩ (b ∪ (cd)))) = ((((ab) ∪ c) ∩ ((ab) ∪ d)) ∩ ((a ∪ (cd)) ∩ (b ∪ (cd))))
27 ancom 74 . . . . . . . 8 ((((ab) ∪ c) ∩ ((ab) ∪ d)) ∩ ((a ∪ (cd)) ∩ (b ∪ (cd)))) = (((a ∪ (cd)) ∩ (b ∪ (cd))) ∩ (((ab) ∪ c) ∩ ((ab) ∪ d)))
28 ax-a2 31 . . . . . . . . . . 11 ((ab) ∪ (cd)) = ((cd) ∪ (ab))
2911df-le2 131 . . . . . . . . . . . . 13 ((ab) ∪ (ab)) = (ab)
3029lor 70 . . . . . . . . . . . 12 ((cd) ∪ ((ab) ∪ (ab))) = ((cd) ∪ (ab))
3130ax-r1 35 . . . . . . . . . . 11 ((cd) ∪ (ab)) = ((cd) ∪ ((ab) ∪ (ab)))
32 or12 80 . . . . . . . . . . 11 ((cd) ∪ ((ab) ∪ (ab))) = ((ab) ∪ ((cd) ∪ (ab)))
3328, 31, 323tr 65 . . . . . . . . . 10 ((ab) ∪ (cd)) = ((ab) ∪ ((cd) ∪ (ab)))
3433lan 77 . . . . . . . . 9 (((ab) ∪ (cd)) ∩ ((ab) ∪ (cd))) = (((ab) ∪ (cd)) ∩ ((ab) ∪ ((cd) ∪ (ab))))
35 leo 158 . . . . . . . . . . . . . . . 16 a ≤ (ab)
3635, 4letr 137 . . . . . . . . . . . . . . 15 a ≤ (cd)
3736lecom 180 . . . . . . . . . . . . . 14 a C (cd)
3837comcom7 460 . . . . . . . . . . . . 13 a C (cd)
3938comcom 453 . . . . . . . . . . . 12 (cd) C a
40 leor 159 . . . . . . . . . . . . . . . 16 b ≤ (ab)
4140, 4letr 137 . . . . . . . . . . . . . . 15 b ≤ (cd)
4241lecom 180 . . . . . . . . . . . . . 14 b C (cd)
4342comcom7 460 . . . . . . . . . . . . 13 b C (cd)
4443comcom 453 . . . . . . . . . . . 12 (cd) C b
4539, 44fh3r 475 . . . . . . . . . . 11 ((ab) ∪ (cd)) = ((a ∪ (cd)) ∩ (b ∪ (cd)))
46 leo 158 . . . . . . . . . . . . . . . 16 c ≤ (cd)
474lecon3 157 . . . . . . . . . . . . . . . 16 (cd) ≤ (ab)
4846, 47letr 137 . . . . . . . . . . . . . . 15 c ≤ (ab)
4948lecom 180 . . . . . . . . . . . . . 14 c C (ab)
5049comcom7 460 . . . . . . . . . . . . 13 c C (ab)
5150comcom 453 . . . . . . . . . . . 12 (ab) C c
52 leor 159 . . . . . . . . . . . . . . . 16 d ≤ (cd)
5352, 47letr 137 . . . . . . . . . . . . . . 15 d ≤ (ab)
5453lecom 180 . . . . . . . . . . . . . 14 d C (ab)
5554comcom7 460 . . . . . . . . . . . . 13 d C (ab)
5655comcom 453 . . . . . . . . . . . 12 (ab) C d
5751, 56fh3 471 . . . . . . . . . . 11 ((ab) ∪ (cd)) = (((ab) ∪ c) ∩ ((ab) ∪ d))
5845, 572an 79 . . . . . . . . . 10 (((ab) ∪ (cd)) ∩ ((ab) ∪ (cd))) = (((a ∪ (cd)) ∩ (b ∪ (cd))) ∩ (((ab) ∪ c) ∩ ((ab) ∪ d)))
5958ax-r1 35 . . . . . . . . 9 (((a ∪ (cd)) ∩ (b ∪ (cd))) ∩ (((ab) ∪ c) ∩ ((ab) ∪ d))) = (((ab) ∪ (cd)) ∩ ((ab) ∪ (cd)))
6034, 59, 203tr1 63 . . . . . . . 8 (((a ∪ (cd)) ∩ (b ∪ (cd))) ∩ (((ab) ∪ c) ∩ ((ab) ∪ d))) = ((ab) ∪ ((cd) ∩ ((cd) ∪ (ab))))
6126, 27, 603tr 65 . . . . . . 7 ((((ab) ∪ c) ∩ (a ∪ (cd))) ∩ (((ab) ∪ d) ∩ (b ∪ (cd)))) = ((ab) ∪ ((cd) ∩ ((cd) ∪ (ab))))
6225, 61ax-r2 36 . . . . . 6 ((ac) ∩ (bd)) = ((ab) ∪ ((cd) ∩ ((cd) ∪ (ab))))
6320, 62, 343tr1 63 . . . . 5 ((ac) ∩ (bd)) = (((ab) ∪ (cd)) ∩ ((ab) ∪ (cd)))
643, 6com2or 483 . . . . . 6 (ab) C ((ab) ∪ (cd))
65 leao1 162 . . . . . . . . . 10 (cd) ≤ (cd)
6665, 47letr 137 . . . . . . . . 9 (cd) ≤ (ab)
6766lecom 180 . . . . . . . 8 (cd) C (ab)
6867comcom7 460 . . . . . . 7 (cd) C (ab)
6968comcom 453 . . . . . 6 (ab) C (cd)
7064, 69fh2 470 . . . . 5 (((ab) ∪ (cd)) ∩ ((ab) ∪ (cd))) = ((((ab) ∪ (cd)) ∩ (ab)) ∪ (((ab) ∪ (cd)) ∩ (cd)))
7163, 70ax-r2 36 . . . 4 ((ac) ∩ (bd)) = ((((ab) ∪ (cd)) ∩ (ab)) ∪ (((ab) ∪ (cd)) ∩ (cd)))
72 ax-a3 32 . . . 4 (((((ab) ∩ (ab)) ∪ ((cd) ∩ (ab))) ∪ ((ab) ∩ (cd))) ∪ ((cd) ∩ (cd))) = ((((ab) ∩ (ab)) ∪ ((cd) ∩ (ab))) ∪ (((ab) ∩ (cd)) ∪ ((cd) ∩ (cd))))
7317, 71, 723tr1 63 . . 3 ((ac) ∩ (bd)) = (((((ab) ∩ (ab)) ∪ ((cd) ∩ (ab))) ∪ ((ab) ∩ (cd))) ∪ ((cd) ∩ (cd)))
74 ax-a3 32 . . . 4 ((((ab) ∩ (ab)) ∪ ((cd) ∩ (ab))) ∪ ((ab) ∩ (cd))) = (((ab) ∩ (ab)) ∪ (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd))))
7574ax-r5 38 . . 3 (((((ab) ∩ (ab)) ∪ ((cd) ∩ (ab))) ∪ ((ab) ∩ (cd))) ∪ ((cd) ∩ (cd))) = ((((ab) ∩ (ab)) ∪ (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd)))) ∪ ((cd) ∩ (cd)))
7673, 75ax-r2 36 . 2 ((ac) ∩ (bd)) = ((((ab) ∩ (ab)) ∪ (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd)))) ∪ ((cd) ∩ (cd)))
7711, 65le2an 169 . . . . . . . . 9 ((ab) ∩ (cd)) ≤ ((ab) ∩ (cd))
78 ancom 74 . . . . . . . . 9 ((ab) ∩ (cd)) = ((cd) ∩ (ab))
7977, 78lbtr 139 . . . . . . . 8 ((ab) ∩ (cd)) ≤ ((cd) ∩ (ab))
8079df-le2 131 . . . . . . 7 (((ab) ∩ (cd)) ∪ ((cd) ∩ (ab))) = ((cd) ∩ (ab))
81 ax-a2 31 . . . . . . 7 (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd))) = (((ab) ∩ (cd)) ∪ ((cd) ∩ (ab)))
8280, 81, 783tr1 63 . . . . . 6 (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd))) = ((ab) ∩ (cd))
834ortha 438 . . . . . 6 ((ab) ∩ (cd)) = 0
8482, 83ax-r2 36 . . . . 5 (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd))) = 0
8584lor 70 . . . 4 (((ab) ∩ (ab)) ∪ (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd)))) = (((ab) ∩ (ab)) ∪ 0)
86 or0 102 . . . 4 (((ab) ∩ (ab)) ∪ 0) = ((ab) ∩ (ab))
8711df2le2 136 . . . 4 ((ab) ∩ (ab)) = (ab)
8885, 86, 873tr 65 . . 3 (((ab) ∩ (ab)) ∪ (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd)))) = (ab)
89 lear 161 . . . 4 ((cd) ∩ (cd)) ≤ (cd)
90 leid 148 . . . . 5 (cd) ≤ (cd)
9165, 90ler2an 173 . . . 4 (cd) ≤ ((cd) ∩ (cd))
9289, 91lebi 145 . . 3 ((cd) ∩ (cd)) = (cd)
9388, 922or 72 . 2 ((((ab) ∩ (ab)) ∪ (((cd) ∩ (ab)) ∪ ((ab) ∩ (cd)))) ∪ ((cd) ∩ (cd))) = ((ab) ∪ (cd))
9476, 93ax-r2 36 1 ((ac) ∩ (bd)) = ((ab) ∪ (cd))
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:  mhlem2  878
  Copyright terms: Public domain W3C validator