Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdleme3b Structured version   Visualization version   GIF version

Theorem cdleme3b 36117
Description: Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 36124 and cdleme3 36125. (Contributed by NM, 6-Jun-2012.)
Hypotheses
Ref Expression
cdleme1.l = (le‘𝐾)
cdleme1.j = (join‘𝐾)
cdleme1.m = (meet‘𝐾)
cdleme1.a 𝐴 = (Atoms‘𝐾)
cdleme1.h 𝐻 = (LHyp‘𝐾)
cdleme1.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme1.f 𝐹 = ((𝑅 𝑈) (𝑄 ((𝑃 𝑅) 𝑊)))
Assertion
Ref Expression
cdleme3b (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝐹𝑅)

Proof of Theorem cdleme3b
StepHypRef Expression
1 simpll 783 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝐾 ∈ HL)
2 simpr3l 1313 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑅𝐴)
3 eqid 2764 . . . . 5 (Base‘𝐾) = (Base‘𝐾)
4 cdleme1.a . . . . 5 𝐴 = (Atoms‘𝐾)
53, 4atbase 35177 . . . 4 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
62, 5syl 17 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑅 ∈ (Base‘𝐾))
7 hllat 35251 . . . . 5 (𝐾 ∈ HL → 𝐾 ∈ Lat)
87ad2antrr 717 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝐾 ∈ Lat)
9 cdleme1.f . . . . 5 𝐹 = ((𝑅 𝑈) (𝑄 ((𝑃 𝑅) 𝑊)))
10 cdleme1.l . . . . . . . . . 10 = (le‘𝐾)
11 cdleme1.j . . . . . . . . . 10 = (join‘𝐾)
12 cdleme1.m . . . . . . . . . 10 = (meet‘𝐾)
13 cdleme1.h . . . . . . . . . 10 𝐻 = (LHyp‘𝐾)
14 cdleme1.u . . . . . . . . . 10 𝑈 = ((𝑃 𝑄) 𝑊)
1510, 11, 12, 4, 13, 14lhpat2 35933 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
16153adant3r3 1235 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑈𝐴)
173, 4atbase 35177 . . . . . . . 8 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
1816, 17syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑈 ∈ (Base‘𝐾))
193, 11latjcl 17318 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾)) → (𝑅 𝑈) ∈ (Base‘𝐾))
208, 6, 18, 19syl3anc 1490 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑅 𝑈) ∈ (Base‘𝐾))
21 simpr2l 1309 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑄𝐴)
223, 4atbase 35177 . . . . . . . 8 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
2321, 22syl 17 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑄 ∈ (Base‘𝐾))
24 simpr1l 1305 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑃𝐴)
253, 4atbase 35177 . . . . . . . . . 10 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
2624, 25syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑃 ∈ (Base‘𝐾))
273, 11latjcl 17318 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑃 𝑅) ∈ (Base‘𝐾))
288, 26, 6, 27syl3anc 1490 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑃 𝑅) ∈ (Base‘𝐾))
293, 13lhpbase 35886 . . . . . . . . 9 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3029ad2antlr 718 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑊 ∈ (Base‘𝐾))
313, 12latmcl 17319 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑃 𝑅) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑅) 𝑊) ∈ (Base‘𝐾))
328, 28, 30, 31syl3anc 1490 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → ((𝑃 𝑅) 𝑊) ∈ (Base‘𝐾))
333, 11latjcl 17318 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ ((𝑃 𝑅) 𝑊) ∈ (Base‘𝐾)) → (𝑄 ((𝑃 𝑅) 𝑊)) ∈ (Base‘𝐾))
348, 23, 32, 33syl3anc 1490 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑄 ((𝑃 𝑅) 𝑊)) ∈ (Base‘𝐾))
353, 12latmcl 17319 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑅 𝑈) ∈ (Base‘𝐾) ∧ (𝑄 ((𝑃 𝑅) 𝑊)) ∈ (Base‘𝐾)) → ((𝑅 𝑈) (𝑄 ((𝑃 𝑅) 𝑊))) ∈ (Base‘𝐾))
368, 20, 34, 35syl3anc 1490 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → ((𝑅 𝑈) (𝑄 ((𝑃 𝑅) 𝑊))) ∈ (Base‘𝐾))
379, 36syl5eqel 2847 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝐹 ∈ (Base‘𝐾))
383, 11latjcl 17318 . . . 4 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝐹 ∈ (Base‘𝐾)) → (𝑅 𝐹) ∈ (Base‘𝐾))
398, 6, 37, 38syl3anc 1490 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑅 𝐹) ∈ (Base‘𝐾))
403, 11latjcl 17318 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑃 𝑄) ∈ (Base‘𝐾))
418, 26, 23, 40syl3anc 1490 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑃 𝑄) ∈ (Base‘𝐾))
423, 10, 12latmle2 17344 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑊) 𝑊)
438, 41, 30, 42syl3anc 1490 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → ((𝑃 𝑄) 𝑊) 𝑊)
4414, 43syl5eqbr 4843 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑈 𝑊)
45 simpr3r 1315 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → ¬ 𝑅 𝑊)
46 nbrne2 4828 . . . . . . 7 ((𝑈 𝑊 ∧ ¬ 𝑅 𝑊) → 𝑈𝑅)
4744, 45, 46syl2anc 579 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑈𝑅)
4847necomd 2991 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑅𝑈)
49 eqid 2764 . . . . . . 7 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
5011, 49, 4atcvr1 35305 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → (𝑅𝑈𝑅( ⋖ ‘𝐾)(𝑅 𝑈)))
511, 2, 16, 50syl3anc 1490 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑅𝑈𝑅( ⋖ ‘𝐾)(𝑅 𝑈)))
5248, 51mpbid 223 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑅( ⋖ ‘𝐾)(𝑅 𝑈))
53 simpr3 1252 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑅𝐴 ∧ ¬ 𝑅 𝑊))
5424, 21, 533jca 1158 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)))
5510, 11, 12, 4, 13, 14, 9cdleme1 36115 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑅 𝐹) = (𝑅 𝑈))
5654, 55syldan 585 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑅 𝐹) = (𝑅 𝑈))
5752, 56breqtrrd 4836 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑅( ⋖ ‘𝐾)(𝑅 𝐹))
583, 49cvrne 35169 . . 3 (((𝐾 ∈ HL ∧ 𝑅 ∈ (Base‘𝐾) ∧ (𝑅 𝐹) ∈ (Base‘𝐾)) ∧ 𝑅( ⋖ ‘𝐾)(𝑅 𝐹)) → 𝑅 ≠ (𝑅 𝐹))
591, 6, 39, 57, 58syl31anc 1492 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝑅 ≠ (𝑅 𝐹))
60 oveq2 6849 . . . . . 6 (𝐹 = 𝑅 → (𝑅 𝐹) = (𝑅 𝑅))
6160adantl 473 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) ∧ 𝐹 = 𝑅) → (𝑅 𝐹) = (𝑅 𝑅))
6211, 4hlatjidm 35257 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑅𝐴) → (𝑅 𝑅) = 𝑅)
631, 2, 62syl2anc 579 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑅 𝑅) = 𝑅)
6463adantr 472 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) ∧ 𝐹 = 𝑅) → (𝑅 𝑅) = 𝑅)
6561, 64eqtr2d 2799 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) ∧ 𝐹 = 𝑅) → 𝑅 = (𝑅 𝐹))
6665ex 401 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝐹 = 𝑅𝑅 = (𝑅 𝐹)))
6766necon3d 2957 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → (𝑅 ≠ (𝑅 𝐹) → 𝐹𝑅))
6859, 67mpd 15 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊))) → 𝐹𝑅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wne 2936   class class class wbr 4808  cfv 6067  (class class class)co 6841  Basecbs 16131  lecple 16222  joincjn 17211  meetcmee 17212  Latclat 17312  ccvr 35150  Atomscatm 35151  HLchlt 35238  LHypclh 35872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-1st 7365  df-2nd 7366  df-proset 17195  df-poset 17213  df-plt 17225  df-lub 17241  df-glb 17242  df-join 17243  df-meet 17244  df-p0 17306  df-p1 17307  df-lat 17313  df-clat 17375  df-oposet 35064  df-ol 35066  df-oml 35067  df-covers 35154  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239  df-psubsp 35391  df-pmap 35392  df-padd 35684  df-lhyp 35876
This theorem is referenced by:  cdleme36m  36349
  Copyright terms: Public domain W3C validator