[Lattice L46-7]Home PageHome Quantum Logic Explorer < Previous   Next >
Related theorems
GIF version
Theorem mhlem 858
Description: Lemma 7.1 of Kalmbach, p. 91.
Hypothesis
Ref Expression
mhlem.1 (a ∪ b) ≤ (c ∪ d)⊥
Assertion
Ref Expression
mhlem ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Proof of Theorem mhlem
StepHypRef Expression
1 comor1 443 . . . . . . 7 (a ∪ b) C a
2 comor2 444 . . . . . . 7 (a ∪ b) C b
31, 2com2an 466 . . . . . 6 (a ∪ b) C (a ∩ b)
4 mhlem.1 . . . . . . . 8 (a ∪ b) ≤ (c ∪ d)⊥
54lecom 172 . . . . . . 7 (a ∪ b) C (c ∪ d)⊥
65comcom7 442 . . . . . 6 (a ∪ b) C (c ∪ d)
73, 6fh1r 455 . . . . 5 (((a ∩ b) ∪ (c ∪ d)) ∩ (a ∪ b)) = (((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b)))
8 comor1 443 . . . . . . 7 (c ∪ d) C c
9 comor2 444 . . . . . . 7 (c ∪ d) C d
108, 9com2an 466 . . . . . 6 (c ∪ d) C (c ∩ d)
11 leao1 154 . . . . . . . . . 10 (a ∩ b) ≤ (a ∪ b)
1211, 4letr 129 . . . . . . . . 9 (a ∩ b) ≤ (c ∪ d)⊥
1312lecom 172 . . . . . . . 8 (a ∩ b) C (c ∪ d)⊥
1413comcom7 442 . . . . . . 7 (a ∩ b) C (c ∪ d)
1514comcom 435 . . . . . 6 (c ∪ d) C (a ∩ b)
1610, 15fh2rc 462 . . . . 5 (((a ∩ b) ∪ (c ∪ d)) ∩ (c ∩ d)) = (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (c ∩ d)))
177, 162or 67 . . . 4 ((((a ∩ b) ∪ (c ∪ d)) ∩ (a ∪ b)) ∪ (((a ∩ b) ∪ (c ∪ d)) ∩ (c ∩ d))) = ((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (c ∩ d))))
1811lerr 142 . . . . . . . 8 (a ∩ b) ≤ ((c ∩ d) ∪ (a ∪ b))
1918lecom 172 . . . . . . 7 (a ∩ b) C ((c ∩ d) ∪ (a ∪ b))
2014, 19fh3 453 . . . . . 6 ((a ∩ b) ∪ ((c ∪ d) ∩ ((c ∩ d) ∪ (a ∪ b)))) = (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∪ b))))
21 id 58 . . . . . . . 8 ((a ∪ c) ∩ (b ∪ d)) = ((a ∪ c) ∩ (b ∪ d))
224mhlemlem1 856 . . . . . . . . 9 (((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) = (a ∪ c)
234mhlemlem2 857 . . . . . . . . 9 (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d))) = (b ∪ d)
2422, 232an 72 . . . . . . . 8 ((((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d)))) = ((a ∪ c) ∩ (b ∪ d))
2521, 21, 243tr1 60 . . . . . . 7 ((a ∪ c) ∩ (b ∪ d)) = ((((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d))))
26 an4 78 . . . . . . . 8 ((((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d)))) = ((((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)) ∩ ((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))))
27 ancom 68 . . . . . . . 8 ((((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)) ∩ ((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d)))) = (((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)))
28 ax-a2 30 . . . . . . . . . . 11 ((a ∪ b) ∪ (c ∩ d)) = ((c ∩ d) ∪ (a ∪ b))
2911df-le2 123 . . . . . . . . . . . . 13 ((a ∩ b) ∪ (a ∪ b)) = (a ∪ b)
3029lor 66 . . . . . . . . . . . 12 ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∪ b))) = ((c ∩ d) ∪ (a ∪ b))
3130ax-r1 34 . . . . . . . . . . 11 ((c ∩ d) ∪ (a ∪ b)) = ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∪ b)))
32 or12 73 . . . . . . . . . . 11 ((c ∩ d) ∪ ((a ∩ b) ∪ (a ∪ b))) = ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∪ b)))
3328, 31, 323tr 62 . . . . . . . . . 10 ((a ∪ b) ∪ (c ∩ d)) = ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∪ b)))
3433lan 70 . . . . . . . . 9 (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d))) = (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∩ b) ∪ ((c ∩ d) ∪ (a ∪ b))))
35 leo 150 . . . . . . . . . . . . . . . 16 a ≤ (a ∪ b)
3635, 4letr 129 . . . . . . . . . . . . . . 15 a ≤ (c ∪ d)⊥
3736lecom 172 . . . . . . . . . . . . . 14 a C (c ∪ d)⊥
3837comcom7 442 . . . . . . . . . . . . 13 a C (c ∪ d)
3938comcom 435 . . . . . . . . . . . 12 (c ∪ d) C a
40 leor 151 . . . . . . . . . . . . . . . 16 b ≤ (a ∪ b)
4140, 4letr 129 . . . . . . . . . . . . . . 15 b ≤ (c ∪ d)⊥
4241lecom 172 . . . . . . . . . . . . . 14 b C (c ∪ d)⊥
4342comcom7 442 . . . . . . . . . . . . 13 b C (c ∪ d)
4443comcom 435 . . . . . . . . . . . 12 (c ∪ d) C b
4539, 44fh3r 457 . . . . . . . . . . 11 ((a ∩ b) ∪ (c ∪ d)) = ((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d)))
46 leo 150 . . . . . . . . . . . . . . . 16 c ≤ (c ∪ d)
474lecon3 149 . . . . . . . . . . . . . . . 16 (c ∪ d) ≤ (a ∪ b)⊥
4846, 47letr 129 . . . . . . . . . . . . . . 15 c ≤ (a ∪ b)⊥
4948lecom 172 . . . . . . . . . . . . . 14 c C (a ∪ b)⊥
5049comcom7 442 . . . . . . . . . . . . 13 c C (a ∪ b)
5150comcom 435 . . . . . . . . . . . 12 (a ∪ b) C c
52 leor 151 . . . . . . . . . . . . . . . 16 d ≤ (c ∪ d)
5352, 47letr 129 . . . . . . . . . . . . . . 15 d ≤ (a ∪ b)⊥
5453lecom 172 . . . . . . . . . . . . . 14 d C (a ∪ b)⊥
5554comcom7 442 . . . . . . . . . . . . 13 d C (a ∪ b)
5655comcom 435 . . . . . . . . . . . 12 (a ∪ b) C d
5751, 56fh3 453 . . . . . . . . . . 11 ((a ∪ b) ∪ (c ∩ d)) = (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d))
5845, 572an 72 . . . . . . . . . 10 (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d))) = (((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d)))
5958ax-r1 34 . . . . . . . . 9 (((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d))) = (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d)))
6034, 59, 203tr1 60 . . . . . . . 8 (((a ∪ (c ∪ d)) ∩ (b ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ c) ∩ ((a ∪ b) ∪ d))) = ((a ∩ b) ∪ ((c ∪ d) ∩ ((c ∩ d) ∪ (a ∪ b))))
6126, 27, 603tr 62 . . . . . . 7 ((((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) ∩ (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d)))) = ((a ∩ b) ∪ ((c ∪ d) ∩ ((c ∩ d) ∪ (a ∪ b))))
6225, 61ax-r2 35 . . . . . 6 ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ ((c ∪ d) ∩ ((c ∩ d) ∪ (a ∪ b))))
6320, 62, 343tr1 60 . . . . 5 ((a ∪ c) ∩ (b ∪ d)) = (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d)))
643, 6com2or 465 . . . . . 6 (a ∪ b) C ((a ∩ b) ∪ (c ∪ d))
65 leao1 154 . . . . . . . . . 10 (c ∩ d) ≤ (c ∪ d)
6665, 47letr 129 . . . . . . . . 9 (c ∩ d) ≤ (a ∪ b)⊥
6766lecom 172 . . . . . . . 8 (c ∩ d) C (a ∪ b)⊥
6867comcom7 442 . . . . . . 7 (c ∩ d) C (a ∪ b)
6968comcom 435 . . . . . 6 (a ∪ b) C (c ∩ d)
7064, 69fh2 452 . . . . 5 (((a ∩ b) ∪ (c ∪ d)) ∩ ((a ∪ b) ∪ (c ∩ d))) = ((((a ∩ b) ∪ (c ∪ d)) ∩ (a ∪ b)) ∪ (((a ∩ b) ∪ (c ∪ d)) ∩ (c ∩ d)))
7163, 70ax-r2 35 . . . 4 ((a ∪ c) ∩ (b ∪ d)) = ((((a ∩ b) ∪ (c ∪ d)) ∩ (a ∪ b)) ∪ (((a ∩ b) ∪ (c ∪ d)) ∩ (c ∩ d)))
72 ax-a3 31 . . . 4 (((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ ((a ∩ b) ∩ (c ∩ d))) ∪ ((c ∪ d) ∩ (c ∩ d))) = ((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (c ∩ d))))
7317, 71, 723tr1 60 . . 3 ((a ∪ c) ∩ (b ∪ d)) = (((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ ((a ∩ b) ∩ (c ∩ d))) ∪ ((c ∪ d) ∩ (c ∩ d)))
74 ax-a3 31 . . . 4 ((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ ((a ∩ b) ∩ (c ∩ d))) = (((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d))))
7574ax-r5 37 . . 3 (((((a ∩ b) ∩ (a ∪ b)) ∪ ((c ∪ d) ∩ (a ∪ b))) ∪ ((a ∩ b) ∩ (c ∩ d))) ∪ ((c ∪ d) ∩ (c ∩ d))) = ((((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) ∪ ((c ∪ d) ∩ (c ∩ d)))
7673, 75ax-r2 35 . 2 ((a ∪ c) ∩ (b ∪ d)) = ((((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) ∪ ((c ∪ d) ∩ (c ∩ d)))
7711, 65le2an 161 . . . . . . . . 9 ((a ∩ b) ∩ (c ∩ d)) ≤ ((a ∪ b) ∩ (c ∪ d))
78 ancom 68 . . . . . . . . 9 ((a ∪ b) ∩ (c ∪ d)) = ((c ∪ d) ∩ (a ∪ b))
7977, 78lbtr 131 . . . . . . . 8 ((a ∩ b) ∩ (c ∩ d)) ≤ ((c ∪ d) ∩ (a ∪ b))
8079df-le2 123 . . . . . . 7 (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (a ∪ b))) = ((c ∪ d) ∩ (a ∪ b))
81 ax-a2 30 . . . . . . 7 (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d))) = (((a ∩ b) ∩ (c ∩ d)) ∪ ((c ∪ d) ∩ (a ∪ b)))
8280, 81, 783tr1 60 . . . . . 6 (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d))) = ((a ∪ b) ∩ (c ∪ d))
834ortha 420 . . . . . 6 ((a ∪ b) ∩ (c ∪ d)) = 0
8482, 83ax-r2 35 . . . . 5 (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d))) = 0
8584lor 66 . . . 4 (((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) = (((a ∩ b) ∩ (a ∪ b)) ∪ 0)
86 or0 94 . . . 4 (((a ∩ b) ∩ (a ∪ b)) ∪ 0) = ((a ∩ b) ∩ (a ∪ b))
8711df2le2 128 . . . 4 ((a ∩ b) ∩ (a ∪ b)) = (a ∩ b)
8885, 86, 873tr 62 . . 3 (((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) = (a ∩ b)
89 lear 153 . . . 4 ((c ∪ d) ∩ (c ∩ d)) ≤ (c ∩ d)
90 leid 140 . . . . 5 (c ∩ d) ≤ (c ∩ d)
9165, 90ler2an 165 . . . 4 (c ∩ d) ≤ ((c ∪ d) ∩ (c ∩ d))
9289, 91lebi 137 . . 3 ((c ∪ d) ∩ (c ∩ d)) = (c ∩ d)
9388, 922or 67 . 2 ((((a ∩ b) ∩ (a ∪ b)) ∪ (((c ∪ d) ∩ (a ∪ b)) ∪ ((a ∩ b) ∩ (c ∩ d)))) ∪ ((c ∪ d) ∩ (c ∩ d))) = ((a ∩ b) ∪ (c ∩ d))
9476, 93ax-r2 35 1 ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Colors of variables: term
Syntax hints:   = wb 1   ≤ wle 2  ⊥ wn 4   ∪ wo 6   ∩ wa 7  0wf 10
This theorem is referenced by:  mhlem2 860
This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421
This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125
metamath.org