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

Theorem cdleme7e 37269
 Description: Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 37270 and cdleme7 37271. (Contributed by NM, 8-Jun-2012.)
Hypotheses
Ref Expression
cdleme4.l = (le‘𝐾)
cdleme4.j = (join‘𝐾)
cdleme4.m = (meet‘𝐾)
cdleme4.a 𝐴 = (Atoms‘𝐾)
cdleme4.h 𝐻 = (LHyp‘𝐾)
cdleme4.u 𝑈 = ((𝑃 𝑄) 𝑊)
cdleme4.f 𝐹 = ((𝑆 𝑈) (𝑄 ((𝑃 𝑆) 𝑊)))
cdleme4.g 𝐺 = ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊)))
cdleme7.v 𝑉 = ((𝑅 𝑆) 𝑊)
Assertion
Ref Expression
cdleme7e ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐺 ≠ (0.‘𝐾))

Proof of Theorem cdleme7e
StepHypRef Expression
1 simp11l 1278 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐾 ∈ HL)
21hllatd 36386 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐾 ∈ Lat)
3 simp2ll 1234 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅𝐴)
4 eqid 2826 . . . . . . 7 (Base‘𝐾) = (Base‘𝐾)
5 cdleme4.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
64, 5atbase 36311 . . . . . 6 (𝑅𝐴𝑅 ∈ (Base‘𝐾))
73, 6syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅 ∈ (Base‘𝐾))
8 hlop 36384 . . . . . 6 (𝐾 ∈ HL → 𝐾 ∈ OP)
9 eqid 2826 . . . . . . 7 (0.‘𝐾) = (0.‘𝐾)
104, 9op0cl 36206 . . . . . 6 (𝐾 ∈ OP → (0.‘𝐾) ∈ (Base‘𝐾))
111, 8, 103syl 18 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (0.‘𝐾) ∈ (Base‘𝐾))
12 cdleme4.j . . . . . 6 = (join‘𝐾)
134, 12latjcl 17656 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ (0.‘𝐾) ∈ (Base‘𝐾)) → (𝑅 (0.‘𝐾)) ∈ (Base‘𝐾))
142, 7, 11, 13syl3anc 1365 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅 (0.‘𝐾)) ∈ (Base‘𝐾))
15 cdleme4.g . . . . . 6 𝐺 = ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊)))
16 simp12l 1280 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑃𝐴)
17 simp13l 1282 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑄𝐴)
184, 12, 5hlatjcl 36389 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴) → (𝑃 𝑄) ∈ (Base‘𝐾))
191, 16, 17, 18syl3anc 1365 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑃 𝑄) ∈ (Base‘𝐾))
20 simp11 1197 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
21 simp2rl 1236 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑆𝐴)
22 cdleme4.l . . . . . . . . . 10 = (le‘𝐾)
23 cdleme4.m . . . . . . . . . 10 = (meet‘𝐾)
24 cdleme4.h . . . . . . . . . 10 𝐻 = (LHyp‘𝐾)
25 cdleme4.u . . . . . . . . . 10 𝑈 = ((𝑃 𝑄) 𝑊)
26 cdleme4.f . . . . . . . . . 10 𝐹 = ((𝑆 𝑈) (𝑄 ((𝑃 𝑆) 𝑊)))
2722, 12, 23, 5, 24, 25, 26, 4cdleme1b 37248 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴𝑆𝐴)) → 𝐹 ∈ (Base‘𝐾))
2820, 16, 17, 21, 27syl13anc 1366 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐹 ∈ (Base‘𝐾))
294, 12, 5hlatjcl 36389 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑆𝐴) → (𝑅 𝑆) ∈ (Base‘𝐾))
301, 3, 21, 29syl3anc 1365 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅 𝑆) ∈ (Base‘𝐾))
31 simp11r 1279 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑊𝐻)
324, 24lhpbase 37020 . . . . . . . . . 10 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3331, 32syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑊 ∈ (Base‘𝐾))
344, 23latmcl 17657 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑅 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑅 𝑆) 𝑊) ∈ (Base‘𝐾))
352, 30, 33, 34syl3anc 1365 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝑅 𝑆) 𝑊) ∈ (Base‘𝐾))
364, 12latjcl 17656 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝐹 ∈ (Base‘𝐾) ∧ ((𝑅 𝑆) 𝑊) ∈ (Base‘𝐾)) → (𝐹 ((𝑅 𝑆) 𝑊)) ∈ (Base‘𝐾))
372, 28, 35, 36syl3anc 1365 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝐹 ((𝑅 𝑆) 𝑊)) ∈ (Base‘𝐾))
384, 23latmcl 17657 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ (𝐹 ((𝑅 𝑆) 𝑊)) ∈ (Base‘𝐾)) → ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊))) ∈ (Base‘𝐾))
392, 19, 37, 38syl3anc 1365 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝑃 𝑄) (𝐹 ((𝑅 𝑆) 𝑊))) ∈ (Base‘𝐾))
4015, 39eqeltrid 2922 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐺 ∈ (Base‘𝐾))
414, 12latjcl 17656 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝐺 ∈ (Base‘𝐾)) → (𝑅 𝐺) ∈ (Base‘𝐾))
422, 7, 40, 41syl3anc 1365 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅 𝐺) ∈ (Base‘𝐾))
434, 22, 23latmle2 17682 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 𝑄) 𝑊) 𝑊)
442, 19, 33, 43syl3anc 1365 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ((𝑃 𝑄) 𝑊) 𝑊)
4525, 44eqbrtrid 5098 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑈 𝑊)
46 simp2lr 1235 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → ¬ 𝑅 𝑊)
47 nbrne2 5083 . . . . . . . 8 ((𝑈 𝑊 ∧ ¬ 𝑅 𝑊) → 𝑈𝑅)
4847necomd 3076 . . . . . . 7 ((𝑈 𝑊 ∧ ¬ 𝑅 𝑊) → 𝑅𝑈)
4945, 46, 48syl2anc 584 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅𝑈)
50 simp12 1198 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
51 simp31 1203 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑃𝑄)
5222, 12, 23, 5, 24, 25lhpat2 37067 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴𝑃𝑄)) → 𝑈𝐴)
5320, 50, 17, 51, 52syl112anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑈𝐴)
54 eqid 2826 . . . . . . . 8 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
5512, 54, 5atcvr1 36439 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑅𝐴𝑈𝐴) → (𝑅𝑈𝑅( ⋖ ‘𝐾)(𝑅 𝑈)))
561, 3, 53, 55syl3anc 1365 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅𝑈𝑅( ⋖ ‘𝐾)(𝑅 𝑈)))
5749, 56mpbid 233 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅( ⋖ ‘𝐾)(𝑅 𝑈))
58 hlol 36383 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ OL)
591, 58syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐾 ∈ OL)
604, 12, 9olj01 36247 . . . . . 6 ((𝐾 ∈ OL ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑅 (0.‘𝐾)) = 𝑅)
6159, 7, 60syl2anc 584 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅 (0.‘𝐾)) = 𝑅)
62 simp2l 1193 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅𝐴 ∧ ¬ 𝑅 𝑊))
63 simp2r 1194 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑆𝐴 ∧ ¬ 𝑆 𝑊))
64 simp32 1204 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝑅 (𝑃 𝑄))
6522, 12, 23, 5, 24, 25, 26, 15cdleme5 37262 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ ((𝑆𝐴 ∧ ¬ 𝑆 𝑊) ∧ 𝑅 (𝑃 𝑄))) → (𝑅 𝐺) = (𝑃 𝑄))
6620, 16, 17, 62, 63, 64, 65syl132anc 1382 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅 𝐺) = (𝑃 𝑄))
6722, 12, 23, 5, 24, 25cdleme4 37260 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴𝑄𝐴 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝑅 (𝑃 𝑄)) → (𝑃 𝑄) = (𝑅 𝑈))
6820, 16, 17, 62, 64, 67syl131anc 1377 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑃 𝑄) = (𝑅 𝑈))
6966, 68eqtrd 2861 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅 𝐺) = (𝑅 𝑈))
7057, 61, 693brtr4d 5095 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅 (0.‘𝐾))( ⋖ ‘𝐾)(𝑅 𝐺))
714, 54cvrne 36303 . . . 4 (((𝐾 ∈ HL ∧ (𝑅 (0.‘𝐾)) ∈ (Base‘𝐾) ∧ (𝑅 𝐺) ∈ (Base‘𝐾)) ∧ (𝑅 (0.‘𝐾))( ⋖ ‘𝐾)(𝑅 𝐺)) → (𝑅 (0.‘𝐾)) ≠ (𝑅 𝐺))
721, 14, 42, 70, 71syl31anc 1367 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (𝑅 (0.‘𝐾)) ≠ (𝑅 𝐺))
73 oveq2 7158 . . . 4 ((0.‘𝐾) = 𝐺 → (𝑅 (0.‘𝐾)) = (𝑅 𝐺))
7473necon3i 3053 . . 3 ((𝑅 (0.‘𝐾)) ≠ (𝑅 𝐺) → (0.‘𝐾) ≠ 𝐺)
7572, 74syl 17 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → (0.‘𝐾) ≠ 𝐺)
7675necomd 3076 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ ((𝑅𝐴 ∧ ¬ 𝑅 𝑊) ∧ (𝑆𝐴 ∧ ¬ 𝑆 𝑊)) ∧ (𝑃𝑄𝑅 (𝑃 𝑄) ∧ ¬ 𝑆 (𝑃 𝑄))) → 𝐺 ≠ (0.‘𝐾))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107   ≠ wne 3021   class class class wbr 5063  ‘cfv 6354  (class class class)co 7150  Basecbs 16478  lecple 16567  joincjn 17549  meetcmee 17550  0.cp0 17642  Latclat 17650  OPcops 36194  OLcol 36196   ⋖ ccvr 36284  Atomscatm 36285  HLchlt 36372  LHypclh 37006 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-iin 4920  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7685  df-2nd 7686  df-proset 17533  df-poset 17551  df-plt 17563  df-lub 17579  df-glb 17580  df-join 17581  df-meet 17582  df-p0 17644  df-p1 17645  df-lat 17651  df-clat 17713  df-oposet 36198  df-ol 36200  df-oml 36201  df-covers 36288  df-ats 36289  df-atl 36320  df-cvlat 36344  df-hlat 36373  df-psubsp 36525  df-pmap 36526  df-padd 36818  df-lhyp 37010 This theorem is referenced by:  cdleme7ga  37270
 Copyright terms: Public domain W3C validator