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

Theorem cdlemm10N 38296
Description: The image of the map 𝐺 is the entire one-dimensional subspace (𝐼𝑉). Remark after Lemma M of [Crawley] p. 121 line 23. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.)
Hypotheses
Ref Expression
cdlemm10.l = (le‘𝐾)
cdlemm10.j = (join‘𝐾)
cdlemm10.a 𝐴 = (Atoms‘𝐾)
cdlemm10.h 𝐻 = (LHyp‘𝐾)
cdlemm10.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemm10.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemm10.i 𝐼 = ((DIsoA‘𝐾)‘𝑊)
cdlemm10.c 𝐶 = {𝑟𝐴 ∣ (𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊)}
cdlemm10.f 𝐹 = (𝑓𝑇 (𝑓𝑃) = 𝑠)
cdlemm10.g 𝐺 = (𝑞𝐶 ↦ (𝑓𝑇 (𝑓𝑃) = 𝑞))
Assertion
Ref Expression
cdlemm10N (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ran 𝐺 = (𝐼𝑉))
Distinct variable groups:   𝑓,𝑟,𝑠,   ,𝑟   𝐴,𝑓,𝑟,𝑠   𝑠,𝑞,𝐶   𝐺,𝑠   𝑓,𝐻,𝑠   𝑓,𝐾,𝑠   𝑓,𝑞,𝑃,𝑟,𝑠   𝑅,𝑓,𝑠   𝑇,𝑓,𝑞,𝑠   𝑓,𝑉,𝑟,𝑠   𝑓,𝑊,𝑟,𝑠
Allowed substitution hints:   𝐴(𝑞)   𝐶(𝑓,𝑟)   𝑅(𝑟,𝑞)   𝑇(𝑟)   𝐹(𝑓,𝑠,𝑟,𝑞)   𝐺(𝑓,𝑟,𝑞)   𝐻(𝑟,𝑞)   𝐼(𝑓,𝑠,𝑟,𝑞)   (𝑓,𝑠,𝑞)   𝐾(𝑟,𝑞)   (𝑞)   𝑉(𝑞)   𝑊(𝑞)

Proof of Theorem cdlemm10N
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 riotaex 7092 . . . . 5 (𝑓𝑇 (𝑓𝑃) = 𝑞) ∈ V
2 cdlemm10.g . . . . 5 𝐺 = (𝑞𝐶 ↦ (𝑓𝑇 (𝑓𝑃) = 𝑞))
31, 2fnmpti 6464 . . . 4 𝐺 Fn 𝐶
4 fvelrnb 6699 . . . 4 (𝐺 Fn 𝐶 → (𝑔 ∈ ran 𝐺 ↔ ∃𝑠𝐶 (𝐺𝑠) = 𝑔))
53, 4ax-mp 5 . . 3 (𝑔 ∈ ran 𝐺 ↔ ∃𝑠𝐶 (𝐺𝑠) = 𝑔)
6 eqeq2 2833 . . . . . . . . . . . 12 (𝑞 = 𝑠 → ((𝑓𝑃) = 𝑞 ↔ (𝑓𝑃) = 𝑠))
76riotabidv 7090 . . . . . . . . . . 11 (𝑞 = 𝑠 → (𝑓𝑇 (𝑓𝑃) = 𝑞) = (𝑓𝑇 (𝑓𝑃) = 𝑠))
8 riotaex 7092 . . . . . . . . . . 11 (𝑓𝑇 (𝑓𝑃) = 𝑠) ∈ V
97, 2, 8fvmpt 6741 . . . . . . . . . 10 (𝑠𝐶 → (𝐺𝑠) = (𝑓𝑇 (𝑓𝑃) = 𝑠))
10 cdlemm10.f . . . . . . . . . 10 𝐹 = (𝑓𝑇 (𝑓𝑃) = 𝑠)
119, 10syl6eqr 2874 . . . . . . . . 9 (𝑠𝐶 → (𝐺𝑠) = 𝐹)
1211adantl 485 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → (𝐺𝑠) = 𝐹)
1312eqeq1d 2823 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → ((𝐺𝑠) = 𝑔𝐹 = 𝑔))
1413rexbidva 3282 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔 ↔ ∃𝑠𝐶 𝐹 = 𝑔))
15 simpl1 1188 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
16 simprl 770 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑔𝑇)
17 simpl2l 1223 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑃𝐴)
18 cdlemm10.l . . . . . . . . . . . 12 = (le‘𝐾)
19 cdlemm10.a . . . . . . . . . . . 12 𝐴 = (Atoms‘𝐾)
20 cdlemm10.h . . . . . . . . . . . 12 𝐻 = (LHyp‘𝐾)
21 cdlemm10.t . . . . . . . . . . . 12 𝑇 = ((LTrn‘𝐾)‘𝑊)
2218, 19, 20, 21ltrnat 37318 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇𝑃𝐴) → (𝑔𝑃) ∈ 𝐴)
2315, 16, 17, 22syl3anc 1368 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ 𝐴)
24 eqid 2821 . . . . . . . . . . . 12 (Base‘𝐾) = (Base‘𝐾)
25 simpl1l 1221 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝐾 ∈ HL)
2625hllatd 36542 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝐾 ∈ Lat)
2724, 19atbase 36467 . . . . . . . . . . . . . 14 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
2817, 27syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑃 ∈ (Base‘𝐾))
2924, 20, 21ltrncl 37303 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇𝑃 ∈ (Base‘𝐾)) → (𝑔𝑃) ∈ (Base‘𝐾))
3015, 16, 28, 29syl3anc 1368 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ (Base‘𝐾))
31 cdlemm10.j . . . . . . . . . . . . . 14 = (join‘𝐾)
3224, 31latjcl 17640 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑔𝑃) ∈ (Base‘𝐾)) → (𝑃 (𝑔𝑃)) ∈ (Base‘𝐾))
3326, 28, 30, 32syl3anc 1368 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑔𝑃)) ∈ (Base‘𝐾))
34 simpl3l 1225 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑉𝐴)
3524, 31, 19hlatjcl 36545 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑉𝐴) → (𝑃 𝑉) ∈ (Base‘𝐾))
3625, 17, 34, 35syl3anc 1368 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 𝑉) ∈ (Base‘𝐾))
3724, 18, 31latlej2 17650 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑔𝑃) ∈ (Base‘𝐾)) → (𝑔𝑃) (𝑃 (𝑔𝑃)))
3826, 28, 30, 37syl3anc 1368 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) (𝑃 (𝑔𝑃)))
39 simpl2 1189 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
40 cdlemm10.r . . . . . . . . . . . . . . 15 𝑅 = ((trL‘𝐾)‘𝑊)
4118, 31, 19, 20, 21, 40trljat1 37344 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅𝑔)) = (𝑃 (𝑔𝑃)))
4215, 16, 39, 41syl3anc 1368 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑅𝑔)) = (𝑃 (𝑔𝑃)))
43 simprr 772 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑅𝑔) 𝑉)
4424, 20, 21, 40trlcl 37342 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇) → (𝑅𝑔) ∈ (Base‘𝐾))
4515, 16, 44syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑅𝑔) ∈ (Base‘𝐾))
4624, 19atbase 36467 . . . . . . . . . . . . . . . 16 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
4734, 46syl 17 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑉 ∈ (Base‘𝐾))
4824, 18, 31latjlej2 17655 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ ((𝑅𝑔) ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → ((𝑅𝑔) 𝑉 → (𝑃 (𝑅𝑔)) (𝑃 𝑉)))
4926, 45, 47, 28, 48syl13anc 1369 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ((𝑅𝑔) 𝑉 → (𝑃 (𝑅𝑔)) (𝑃 𝑉)))
5043, 49mpd 15 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑅𝑔)) (𝑃 𝑉))
5142, 50eqbrtrrd 5063 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑔𝑃)) (𝑃 𝑉))
5224, 18, 26, 30, 33, 36, 38, 51lattrd 17647 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) (𝑃 𝑉))
5318, 19, 20, 21ltrnel 37317 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑔𝑃) ∈ 𝐴 ∧ ¬ (𝑔𝑃) 𝑊))
5453simprd 499 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ¬ (𝑔𝑃) 𝑊)
5515, 16, 39, 54syl3anc 1368 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ¬ (𝑔𝑃) 𝑊)
5652, 55jca 515 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊))
57 breq1 5042 . . . . . . . . . . . 12 (𝑟 = (𝑔𝑃) → (𝑟 (𝑃 𝑉) ↔ (𝑔𝑃) (𝑃 𝑉)))
58 breq1 5042 . . . . . . . . . . . . 13 (𝑟 = (𝑔𝑃) → (𝑟 𝑊 ↔ (𝑔𝑃) 𝑊))
5958notbid 321 . . . . . . . . . . . 12 (𝑟 = (𝑔𝑃) → (¬ 𝑟 𝑊 ↔ ¬ (𝑔𝑃) 𝑊))
6057, 59anbi12d 633 . . . . . . . . . . 11 (𝑟 = (𝑔𝑃) → ((𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊) ↔ ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊)))
61 cdlemm10.c . . . . . . . . . . 11 𝐶 = {𝑟𝐴 ∣ (𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊)}
6260, 61elrab2 3660 . . . . . . . . . 10 ((𝑔𝑃) ∈ 𝐶 ↔ ((𝑔𝑃) ∈ 𝐴 ∧ ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊)))
6323, 56, 62sylanbrc 586 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ 𝐶)
6418, 19, 20, 21cdlemeiota 37763 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑔𝑇) → 𝑔 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
6515, 39, 16, 64syl3anc 1368 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑔 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
6665eqcomd 2827 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔)
67 eqeq2 2833 . . . . . . . . . . . . 13 (𝑠 = (𝑔𝑃) → ((𝑓𝑃) = 𝑠 ↔ (𝑓𝑃) = (𝑔𝑃)))
6867riotabidv 7090 . . . . . . . . . . . 12 (𝑠 = (𝑔𝑃) → (𝑓𝑇 (𝑓𝑃) = 𝑠) = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
6910, 68syl5eq 2868 . . . . . . . . . . 11 (𝑠 = (𝑔𝑃) → 𝐹 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
7069eqeq1d 2823 . . . . . . . . . 10 (𝑠 = (𝑔𝑃) → (𝐹 = 𝑔 ↔ (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔))
7170rspcev 3600 . . . . . . . . 9 (((𝑔𝑃) ∈ 𝐶 ∧ (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔) → ∃𝑠𝐶 𝐹 = 𝑔)
7263, 66, 71syl2anc 587 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ∃𝑠𝐶 𝐹 = 𝑔)
7372ex 416 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑔𝑇 ∧ (𝑅𝑔) 𝑉) → ∃𝑠𝐶 𝐹 = 𝑔))
74 breq1 5042 . . . . . . . . . . . . 13 (𝑟 = 𝑠 → (𝑟 (𝑃 𝑉) ↔ 𝑠 (𝑃 𝑉)))
75 breq1 5042 . . . . . . . . . . . . . 14 (𝑟 = 𝑠 → (𝑟 𝑊𝑠 𝑊))
7675notbid 321 . . . . . . . . . . . . 13 (𝑟 = 𝑠 → (¬ 𝑟 𝑊 ↔ ¬ 𝑠 𝑊))
7774, 76anbi12d 633 . . . . . . . . . . . 12 (𝑟 = 𝑠 → ((𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊) ↔ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)))
7877, 61elrab2 3660 . . . . . . . . . . 11 (𝑠𝐶 ↔ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)))
79 simpl1 1188 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
80 simpl2l 1223 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃𝐴)
81 simpl2r 1224 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ¬ 𝑃 𝑊)
82 simprl 770 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠𝐴)
83 simprrr 781 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ¬ 𝑠 𝑊)
8418, 19, 20, 21, 10ltrniotacl 37757 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → 𝐹𝑇)
8518, 19, 20, 21, 10ltrniotaval 37759 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → (𝐹𝑃) = 𝑠)
8684, 85jca 515 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠))
8779, 80, 81, 82, 83, 86syl122anc 1376 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠))
88 simp3l 1198 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → 𝐹𝑇)
89 simp11 1200 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
90 simp12 1201 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
91 eqid 2821 . . . . . . . . . . . . . . . . 17 (meet‘𝐾) = (meet‘𝐾)
9218, 31, 91, 19, 20, 21, 40trlval2 37341 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊))
9389, 88, 90, 92syl3anc 1368 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊))
94 simp3r 1199 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐹𝑃) = 𝑠)
9594oveq2d 7146 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑃 (𝐹𝑃)) = (𝑃 𝑠))
9695oveq1d 7145 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊) = ((𝑃 𝑠)(meet‘𝐾)𝑊))
9793, 96eqtrd 2856 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) = ((𝑃 𝑠)(meet‘𝐾)𝑊))
98 simpl1l 1221 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝐾 ∈ HL)
99 simpl3l 1225 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑉𝐴)
10018, 31, 19hlatlej1 36553 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑉𝐴) → 𝑃 (𝑃 𝑉))
10198, 80, 99, 100syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃 (𝑃 𝑉))
102 simprrl 780 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠 (𝑃 𝑉))
10398hllatd 36542 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝐾 ∈ Lat)
10480, 27syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃 ∈ (Base‘𝐾))
10524, 19atbase 36467 . . . . . . . . . . . . . . . . . . . 20 (𝑠𝐴𝑠 ∈ (Base‘𝐾))
106105ad2antrl 727 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠 ∈ (Base‘𝐾))
10798, 80, 99, 35syl3anc 1368 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑉) ∈ (Base‘𝐾))
10824, 18, 31latjle12 17651 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑠 ∈ (Base‘𝐾) ∧ (𝑃 𝑉) ∈ (Base‘𝐾))) → ((𝑃 (𝑃 𝑉) ∧ 𝑠 (𝑃 𝑉)) ↔ (𝑃 𝑠) (𝑃 𝑉)))
109103, 104, 106, 107, 108syl13anc 1369 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 (𝑃 𝑉) ∧ 𝑠 (𝑃 𝑉)) ↔ (𝑃 𝑠) (𝑃 𝑉)))
110101, 102, 109mpbi2and 711 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑠) (𝑃 𝑉))
11124, 31, 19hlatjcl 36545 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑠𝐴) → (𝑃 𝑠) ∈ (Base‘𝐾))
11298, 80, 82, 111syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑠) ∈ (Base‘𝐾))
113 simpl1r 1222 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑊𝐻)
11424, 20lhpbase 37176 . . . . . . . . . . . . . . . . . . 19 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
115113, 114syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑊 ∈ (Base‘𝐾))
11624, 18, 91latmlem1 17670 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ ((𝑃 𝑠) ∈ (Base‘𝐾) ∧ (𝑃 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 𝑠) (𝑃 𝑉) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊)))
117103, 112, 107, 115, 116syl13anc 1369 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠) (𝑃 𝑉) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊)))
118110, 117mpd 15 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊))
11918, 31, 91, 19, 20lhpat4N 37222 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑃 𝑉)(meet‘𝐾)𝑊) = 𝑉)
120119adantr 484 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑉)(meet‘𝐾)𝑊) = 𝑉)
121118, 120breqtrd 5065 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠)(meet‘𝐾)𝑊) 𝑉)
1221213adant3 1129 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → ((𝑃 𝑠)(meet‘𝐾)𝑊) 𝑉)
12397, 122eqbrtrd 5061 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) 𝑉)
12488, 123jca 515 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
12587, 124mpd3an3 1459 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
12678, 125sylan2b 596 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
127126ex 416 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑠𝐶 → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉)))
128 eleq1 2899 . . . . . . . . . . 11 (𝐹 = 𝑔 → (𝐹𝑇𝑔𝑇))
129 fveq2 6643 . . . . . . . . . . . 12 (𝐹 = 𝑔 → (𝑅𝐹) = (𝑅𝑔))
130129breq1d 5049 . . . . . . . . . . 11 (𝐹 = 𝑔 → ((𝑅𝐹) 𝑉 ↔ (𝑅𝑔) 𝑉))
131128, 130anbi12d 633 . . . . . . . . . 10 (𝐹 = 𝑔 → ((𝐹𝑇 ∧ (𝑅𝐹) 𝑉) ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
132131biimpcd 252 . . . . . . . . 9 ((𝐹𝑇 ∧ (𝑅𝐹) 𝑉) → (𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
133127, 132syl6 35 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑠𝐶 → (𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉))))
134133rexlimdv 3269 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
13573, 134impbid 215 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑔𝑇 ∧ (𝑅𝑔) 𝑉) ↔ ∃𝑠𝐶 𝐹 = 𝑔))
13614, 135bitr4d 285 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔 ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
137 fveq2 6643 . . . . . . 7 (𝑓 = 𝑔 → (𝑅𝑓) = (𝑅𝑔))
138137breq1d 5049 . . . . . 6 (𝑓 = 𝑔 → ((𝑅𝑓) 𝑉 ↔ (𝑅𝑔) 𝑉))
139138elrab 3657 . . . . 5 (𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉} ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉))
140136, 139syl6bbr 292 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉}))
141 simp1l 1194 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝐾 ∈ HL)
142 simp1r 1195 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑊𝐻)
143 simp3l 1198 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉𝐴)
144143, 46syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉 ∈ (Base‘𝐾))
145 simp3r 1199 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉 𝑊)
146 cdlemm10.i . . . . . . 7 𝐼 = ((DIsoA‘𝐾)‘𝑊)
14724, 18, 20, 21, 40, 146diaval 38210 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 𝑊)) → (𝐼𝑉) = {𝑓𝑇 ∣ (𝑅𝑓) 𝑉})
148141, 142, 144, 145, 147syl22anc 837 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝐼𝑉) = {𝑓𝑇 ∣ (𝑅𝑓) 𝑉})
149148eleq2d 2897 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑔 ∈ (𝐼𝑉) ↔ 𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉}))
150140, 149bitr4d 285 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔𝑔 ∈ (𝐼𝑉)))
1515, 150syl5bb 286 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑔 ∈ ran 𝐺𝑔 ∈ (𝐼𝑉)))
152151eqrdv 2819 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ran 𝐺 = (𝐼𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2115  wrex 3127  {crab 3130   class class class wbr 5039  cmpt 5119  ran crn 5529   Fn wfn 6323  cfv 6328  crio 7087  (class class class)co 7130  Basecbs 16462  lecple 16551  joincjn 17533  meetcmee 17534  Latclat 17634  Atomscatm 36441  HLchlt 36528  LHypclh 37162  LTrncltrn 37279  trLctrl 37336  DIsoAcdia 38206
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-riotaBAD 36131
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-iun 4894  df-iin 4895  df-br 5040  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-1st 7664  df-2nd 7665  df-undef 7914  df-map 8383  df-proset 17517  df-poset 17535  df-plt 17547  df-lub 17563  df-glb 17564  df-join 17565  df-meet 17566  df-p0 17628  df-p1 17629  df-lat 17635  df-clat 17697  df-oposet 36354  df-ol 36356  df-oml 36357  df-covers 36444  df-ats 36445  df-atl 36476  df-cvlat 36500  df-hlat 36529  df-llines 36676  df-lplanes 36677  df-lvols 36678  df-lines 36679  df-psubsp 36681  df-pmap 36682  df-padd 36974  df-lhyp 37166  df-laut 37167  df-ldil 37282  df-ltrn 37283  df-trl 37337  df-disoa 38207
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator