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 40305
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 7372 . . . . 5 (𝑓𝑇 (𝑓𝑃) = 𝑞) ∈ V
2 cdlemm10.g . . . . 5 𝐺 = (𝑞𝐶 ↦ (𝑓𝑇 (𝑓𝑃) = 𝑞))
31, 2fnmpti 6693 . . . 4 𝐺 Fn 𝐶
4 fvelrnb 6952 . . . 4 (𝐺 Fn 𝐶 → (𝑔 ∈ ran 𝐺 ↔ ∃𝑠𝐶 (𝐺𝑠) = 𝑔))
53, 4ax-mp 5 . . 3 (𝑔 ∈ ran 𝐺 ↔ ∃𝑠𝐶 (𝐺𝑠) = 𝑔)
6 eqeq2 2743 . . . . . . . . . . . 12 (𝑞 = 𝑠 → ((𝑓𝑃) = 𝑞 ↔ (𝑓𝑃) = 𝑠))
76riotabidv 7370 . . . . . . . . . . 11 (𝑞 = 𝑠 → (𝑓𝑇 (𝑓𝑃) = 𝑞) = (𝑓𝑇 (𝑓𝑃) = 𝑠))
8 riotaex 7372 . . . . . . . . . . 11 (𝑓𝑇 (𝑓𝑃) = 𝑠) ∈ V
97, 2, 8fvmpt 6998 . . . . . . . . . 10 (𝑠𝐶 → (𝐺𝑠) = (𝑓𝑇 (𝑓𝑃) = 𝑠))
10 cdlemm10.f . . . . . . . . . 10 𝐹 = (𝑓𝑇 (𝑓𝑃) = 𝑠)
119, 10eqtr4di 2789 . . . . . . . . 9 (𝑠𝐶 → (𝐺𝑠) = 𝐹)
1211adantl 481 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → (𝐺𝑠) = 𝐹)
1312eqeq1d 2733 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → ((𝐺𝑠) = 𝑔𝐹 = 𝑔))
1413rexbidva 3175 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔 ↔ ∃𝑠𝐶 𝐹 = 𝑔))
15 simpl1 1190 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
16 simprl 768 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑔𝑇)
17 simpl2l 1225 . . . . . . . . . . 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 39327 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇𝑃𝐴) → (𝑔𝑃) ∈ 𝐴)
2315, 16, 17, 22syl3anc 1370 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ 𝐴)
24 eqid 2731 . . . . . . . . . . . 12 (Base‘𝐾) = (Base‘𝐾)
25 simpl1l 1223 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝐾 ∈ HL)
2625hllatd 38550 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝐾 ∈ Lat)
2724, 19atbase 38475 . . . . . . . . . . . . . 14 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
2817, 27syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑃 ∈ (Base‘𝐾))
2924, 20, 21ltrncl 39312 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇𝑃 ∈ (Base‘𝐾)) → (𝑔𝑃) ∈ (Base‘𝐾))
3015, 16, 28, 29syl3anc 1370 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ (Base‘𝐾))
31 cdlemm10.j . . . . . . . . . . . . . 14 = (join‘𝐾)
3224, 31latjcl 18399 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑔𝑃) ∈ (Base‘𝐾)) → (𝑃 (𝑔𝑃)) ∈ (Base‘𝐾))
3326, 28, 30, 32syl3anc 1370 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑔𝑃)) ∈ (Base‘𝐾))
34 simpl3l 1227 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑉𝐴)
3524, 31, 19hlatjcl 38553 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑉𝐴) → (𝑃 𝑉) ∈ (Base‘𝐾))
3625, 17, 34, 35syl3anc 1370 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 𝑉) ∈ (Base‘𝐾))
3724, 18, 31latlej2 18409 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑔𝑃) ∈ (Base‘𝐾)) → (𝑔𝑃) (𝑃 (𝑔𝑃)))
3826, 28, 30, 37syl3anc 1370 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) (𝑃 (𝑔𝑃)))
39 simpl2 1191 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
40 cdlemm10.r . . . . . . . . . . . . . . 15 𝑅 = ((trL‘𝐾)‘𝑊)
4118, 31, 19, 20, 21, 40trljat1 39353 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅𝑔)) = (𝑃 (𝑔𝑃)))
4215, 16, 39, 41syl3anc 1370 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑅𝑔)) = (𝑃 (𝑔𝑃)))
43 simprr 770 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑅𝑔) 𝑉)
4424, 20, 21, 40trlcl 39351 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇) → (𝑅𝑔) ∈ (Base‘𝐾))
4515, 16, 44syl2anc 583 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑅𝑔) ∈ (Base‘𝐾))
4624, 19atbase 38475 . . . . . . . . . . . . . . . 16 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
4734, 46syl 17 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑉 ∈ (Base‘𝐾))
4824, 18, 31latjlej2 18414 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ ((𝑅𝑔) ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → ((𝑅𝑔) 𝑉 → (𝑃 (𝑅𝑔)) (𝑃 𝑉)))
4926, 45, 47, 28, 48syl13anc 1371 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ((𝑅𝑔) 𝑉 → (𝑃 (𝑅𝑔)) (𝑃 𝑉)))
5043, 49mpd 15 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑅𝑔)) (𝑃 𝑉))
5142, 50eqbrtrrd 5172 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑔𝑃)) (𝑃 𝑉))
5224, 18, 26, 30, 33, 36, 38, 51lattrd 18406 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) (𝑃 𝑉))
5318, 19, 20, 21ltrnel 39326 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑔𝑃) ∈ 𝐴 ∧ ¬ (𝑔𝑃) 𝑊))
5453simprd 495 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ¬ (𝑔𝑃) 𝑊)
5515, 16, 39, 54syl3anc 1370 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ¬ (𝑔𝑃) 𝑊)
5652, 55jca 511 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊))
57 breq1 5151 . . . . . . . . . . . 12 (𝑟 = (𝑔𝑃) → (𝑟 (𝑃 𝑉) ↔ (𝑔𝑃) (𝑃 𝑉)))
58 breq1 5151 . . . . . . . . . . . . 13 (𝑟 = (𝑔𝑃) → (𝑟 𝑊 ↔ (𝑔𝑃) 𝑊))
5958notbid 318 . . . . . . . . . . . 12 (𝑟 = (𝑔𝑃) → (¬ 𝑟 𝑊 ↔ ¬ (𝑔𝑃) 𝑊))
6057, 59anbi12d 630 . . . . . . . . . . 11 (𝑟 = (𝑔𝑃) → ((𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊) ↔ ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊)))
61 cdlemm10.c . . . . . . . . . . 11 𝐶 = {𝑟𝐴 ∣ (𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊)}
6260, 61elrab2 3686 . . . . . . . . . 10 ((𝑔𝑃) ∈ 𝐶 ↔ ((𝑔𝑃) ∈ 𝐴 ∧ ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊)))
6323, 56, 62sylanbrc 582 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ 𝐶)
6418, 19, 20, 21cdlemeiota 39772 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑔𝑇) → 𝑔 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
6515, 39, 16, 64syl3anc 1370 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑔 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
6665eqcomd 2737 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔)
67 eqeq2 2743 . . . . . . . . . . . . 13 (𝑠 = (𝑔𝑃) → ((𝑓𝑃) = 𝑠 ↔ (𝑓𝑃) = (𝑔𝑃)))
6867riotabidv 7370 . . . . . . . . . . . 12 (𝑠 = (𝑔𝑃) → (𝑓𝑇 (𝑓𝑃) = 𝑠) = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
6910, 68eqtrid 2783 . . . . . . . . . . 11 (𝑠 = (𝑔𝑃) → 𝐹 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
7069eqeq1d 2733 . . . . . . . . . 10 (𝑠 = (𝑔𝑃) → (𝐹 = 𝑔 ↔ (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔))
7170rspcev 3612 . . . . . . . . 9 (((𝑔𝑃) ∈ 𝐶 ∧ (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔) → ∃𝑠𝐶 𝐹 = 𝑔)
7263, 66, 71syl2anc 583 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ∃𝑠𝐶 𝐹 = 𝑔)
7372ex 412 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑔𝑇 ∧ (𝑅𝑔) 𝑉) → ∃𝑠𝐶 𝐹 = 𝑔))
74 breq1 5151 . . . . . . . . . . . . 13 (𝑟 = 𝑠 → (𝑟 (𝑃 𝑉) ↔ 𝑠 (𝑃 𝑉)))
75 breq1 5151 . . . . . . . . . . . . . 14 (𝑟 = 𝑠 → (𝑟 𝑊𝑠 𝑊))
7675notbid 318 . . . . . . . . . . . . 13 (𝑟 = 𝑠 → (¬ 𝑟 𝑊 ↔ ¬ 𝑠 𝑊))
7774, 76anbi12d 630 . . . . . . . . . . . 12 (𝑟 = 𝑠 → ((𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊) ↔ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)))
7877, 61elrab2 3686 . . . . . . . . . . 11 (𝑠𝐶 ↔ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)))
79 simpl1 1190 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
80 simpl2l 1225 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃𝐴)
81 simpl2r 1226 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ¬ 𝑃 𝑊)
82 simprl 768 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠𝐴)
83 simprrr 779 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ¬ 𝑠 𝑊)
8418, 19, 20, 21, 10ltrniotacl 39766 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → 𝐹𝑇)
8518, 19, 20, 21, 10ltrniotaval 39768 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → (𝐹𝑃) = 𝑠)
8684, 85jca 511 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠))
8779, 80, 81, 82, 83, 86syl122anc 1378 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠))
88 simp3l 1200 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → 𝐹𝑇)
89 simp11 1202 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
90 simp12 1203 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
91 eqid 2731 . . . . . . . . . . . . . . . . 17 (meet‘𝐾) = (meet‘𝐾)
9218, 31, 91, 19, 20, 21, 40trlval2 39350 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊))
9389, 88, 90, 92syl3anc 1370 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊))
94 simp3r 1201 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐹𝑃) = 𝑠)
9594oveq2d 7428 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑃 (𝐹𝑃)) = (𝑃 𝑠))
9695oveq1d 7427 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊) = ((𝑃 𝑠)(meet‘𝐾)𝑊))
9793, 96eqtrd 2771 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) = ((𝑃 𝑠)(meet‘𝐾)𝑊))
98 simpl1l 1223 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝐾 ∈ HL)
99 simpl3l 1227 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑉𝐴)
10018, 31, 19hlatlej1 38561 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑉𝐴) → 𝑃 (𝑃 𝑉))
10198, 80, 99, 100syl3anc 1370 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃 (𝑃 𝑉))
102 simprrl 778 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠 (𝑃 𝑉))
10398hllatd 38550 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝐾 ∈ Lat)
10480, 27syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃 ∈ (Base‘𝐾))
10524, 19atbase 38475 . . . . . . . . . . . . . . . . . . . 20 (𝑠𝐴𝑠 ∈ (Base‘𝐾))
106105ad2antrl 725 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠 ∈ (Base‘𝐾))
10798, 80, 99, 35syl3anc 1370 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑉) ∈ (Base‘𝐾))
10824, 18, 31latjle12 18410 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑠 ∈ (Base‘𝐾) ∧ (𝑃 𝑉) ∈ (Base‘𝐾))) → ((𝑃 (𝑃 𝑉) ∧ 𝑠 (𝑃 𝑉)) ↔ (𝑃 𝑠) (𝑃 𝑉)))
109103, 104, 106, 107, 108syl13anc 1371 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 (𝑃 𝑉) ∧ 𝑠 (𝑃 𝑉)) ↔ (𝑃 𝑠) (𝑃 𝑉)))
110101, 102, 109mpbi2and 709 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑠) (𝑃 𝑉))
11124, 31, 19hlatjcl 38553 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑠𝐴) → (𝑃 𝑠) ∈ (Base‘𝐾))
11298, 80, 82, 111syl3anc 1370 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑠) ∈ (Base‘𝐾))
113 simpl1r 1224 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑊𝐻)
11424, 20lhpbase 39185 . . . . . . . . . . . . . . . . . . 19 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
115113, 114syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑊 ∈ (Base‘𝐾))
11624, 18, 91latmlem1 18429 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ ((𝑃 𝑠) ∈ (Base‘𝐾) ∧ (𝑃 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 𝑠) (𝑃 𝑉) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊)))
117103, 112, 107, 115, 116syl13anc 1371 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠) (𝑃 𝑉) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊)))
118110, 117mpd 15 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊))
11918, 31, 91, 19, 20lhpat4N 39231 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑃 𝑉)(meet‘𝐾)𝑊) = 𝑉)
120119adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑉)(meet‘𝐾)𝑊) = 𝑉)
121118, 120breqtrd 5174 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠)(meet‘𝐾)𝑊) 𝑉)
1221213adant3 1131 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → ((𝑃 𝑠)(meet‘𝐾)𝑊) 𝑉)
12397, 122eqbrtrd 5170 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) 𝑉)
12488, 123jca 511 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
12587, 124mpd3an3 1461 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
12678, 125sylan2b 593 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
127126ex 412 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑠𝐶 → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉)))
128 eleq1 2820 . . . . . . . . . . 11 (𝐹 = 𝑔 → (𝐹𝑇𝑔𝑇))
129 fveq2 6891 . . . . . . . . . . . 12 (𝐹 = 𝑔 → (𝑅𝐹) = (𝑅𝑔))
130129breq1d 5158 . . . . . . . . . . 11 (𝐹 = 𝑔 → ((𝑅𝐹) 𝑉 ↔ (𝑅𝑔) 𝑉))
131128, 130anbi12d 630 . . . . . . . . . 10 (𝐹 = 𝑔 → ((𝐹𝑇 ∧ (𝑅𝐹) 𝑉) ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
132131biimpcd 248 . . . . . . . . 9 ((𝐹𝑇 ∧ (𝑅𝐹) 𝑉) → (𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
133127, 132syl6 35 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑠𝐶 → (𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉))))
134133rexlimdv 3152 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
13573, 134impbid 211 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑔𝑇 ∧ (𝑅𝑔) 𝑉) ↔ ∃𝑠𝐶 𝐹 = 𝑔))
13614, 135bitr4d 282 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔 ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
137 fveq2 6891 . . . . . . 7 (𝑓 = 𝑔 → (𝑅𝑓) = (𝑅𝑔))
138137breq1d 5158 . . . . . 6 (𝑓 = 𝑔 → ((𝑅𝑓) 𝑉 ↔ (𝑅𝑔) 𝑉))
139138elrab 3683 . . . . 5 (𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉} ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉))
140136, 139bitr4di 289 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉}))
141 simp1l 1196 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝐾 ∈ HL)
142 simp1r 1197 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑊𝐻)
143 simp3l 1200 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉𝐴)
144143, 46syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉 ∈ (Base‘𝐾))
145 simp3r 1201 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉 𝑊)
146 cdlemm10.i . . . . . . 7 𝐼 = ((DIsoA‘𝐾)‘𝑊)
14724, 18, 20, 21, 40, 146diaval 40219 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 𝑊)) → (𝐼𝑉) = {𝑓𝑇 ∣ (𝑅𝑓) 𝑉})
148141, 142, 144, 145, 147syl22anc 836 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝐼𝑉) = {𝑓𝑇 ∣ (𝑅𝑓) 𝑉})
149148eleq2d 2818 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑔 ∈ (𝐼𝑉) ↔ 𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉}))
150140, 149bitr4d 282 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔𝑔 ∈ (𝐼𝑉)))
1515, 150bitrid 283 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑔 ∈ ran 𝐺𝑔 ∈ (𝐼𝑉)))
152151eqrdv 2729 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ran 𝐺 = (𝐼𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1086   = wceq 1540  wcel 2105  wrex 3069  {crab 3431   class class class wbr 5148  cmpt 5231  ran crn 5677   Fn wfn 6538  cfv 6543  crio 7367  (class class class)co 7412  Basecbs 17151  lecple 17211  joincjn 18271  meetcmee 18272  Latclat 18391  Atomscatm 38449  HLchlt 38536  LHypclh 39171  LTrncltrn 39288  trLctrl 39345  DIsoAcdia 40215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-riotaBAD 38139
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-undef 8264  df-map 8828  df-proset 18255  df-poset 18273  df-plt 18290  df-lub 18306  df-glb 18307  df-join 18308  df-meet 18309  df-p0 18385  df-p1 18386  df-lat 18392  df-clat 18459  df-oposet 38362  df-ol 38364  df-oml 38365  df-covers 38452  df-ats 38453  df-atl 38484  df-cvlat 38508  df-hlat 38537  df-llines 38685  df-lplanes 38686  df-lvols 38687  df-lines 38688  df-psubsp 38690  df-pmap 38691  df-padd 38983  df-lhyp 39175  df-laut 39176  df-ldil 39291  df-ltrn 39292  df-trl 39346  df-disoa 40216
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator