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 35219
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 6493 . . . . 5 (𝑓𝑇 (𝑓𝑃) = 𝑞) ∈ V
2 cdlemm10.g . . . . 5 𝐺 = (𝑞𝐶 ↦ (𝑓𝑇 (𝑓𝑃) = 𝑞))
31, 2fnmpti 5921 . . . 4 𝐺 Fn 𝐶
4 fvelrnb 6138 . . . 4 (𝐺 Fn 𝐶 → (𝑔 ∈ ran 𝐺 ↔ ∃𝑠𝐶 (𝐺𝑠) = 𝑔))
53, 4ax-mp 5 . . 3 (𝑔 ∈ ran 𝐺 ↔ ∃𝑠𝐶 (𝐺𝑠) = 𝑔)
6 eqeq2 2621 . . . . . . . . . . . 12 (𝑞 = 𝑠 → ((𝑓𝑃) = 𝑞 ↔ (𝑓𝑃) = 𝑠))
76riotabidv 6491 . . . . . . . . . . 11 (𝑞 = 𝑠 → (𝑓𝑇 (𝑓𝑃) = 𝑞) = (𝑓𝑇 (𝑓𝑃) = 𝑠))
8 riotaex 6493 . . . . . . . . . . 11 (𝑓𝑇 (𝑓𝑃) = 𝑠) ∈ V
97, 2, 8fvmpt 6176 . . . . . . . . . 10 (𝑠𝐶 → (𝐺𝑠) = (𝑓𝑇 (𝑓𝑃) = 𝑠))
10 cdlemm10.f . . . . . . . . . 10 𝐹 = (𝑓𝑇 (𝑓𝑃) = 𝑠)
119, 10syl6eqr 2662 . . . . . . . . 9 (𝑠𝐶 → (𝐺𝑠) = 𝐹)
1211adantl 481 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → (𝐺𝑠) = 𝐹)
1312eqeq1d 2612 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → ((𝐺𝑠) = 𝑔𝐹 = 𝑔))
1413rexbidva 3031 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔 ↔ ∃𝑠𝐶 𝐹 = 𝑔))
15 simpl1 1057 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
16 simprl 790 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑔𝑇)
17 simpl2l 1107 . . . . . . . . . . 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 34238 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇𝑃𝐴) → (𝑔𝑃) ∈ 𝐴)
2315, 16, 17, 22syl3anc 1318 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ 𝐴)
24 eqid 2610 . . . . . . . . . . . 12 (Base‘𝐾) = (Base‘𝐾)
25 simpl1l 1105 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝐾 ∈ HL)
26 hllat 33462 . . . . . . . . . . . . 13 (𝐾 ∈ HL → 𝐾 ∈ Lat)
2725, 26syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝐾 ∈ Lat)
2824, 19atbase 33388 . . . . . . . . . . . . . 14 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
2917, 28syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑃 ∈ (Base‘𝐾))
3024, 20, 21ltrncl 34223 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇𝑃 ∈ (Base‘𝐾)) → (𝑔𝑃) ∈ (Base‘𝐾))
3115, 16, 29, 30syl3anc 1318 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ (Base‘𝐾))
32 cdlemm10.j . . . . . . . . . . . . . 14 = (join‘𝐾)
3324, 32latjcl 16823 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑔𝑃) ∈ (Base‘𝐾)) → (𝑃 (𝑔𝑃)) ∈ (Base‘𝐾))
3427, 29, 31, 33syl3anc 1318 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑔𝑃)) ∈ (Base‘𝐾))
35 simpl3l 1109 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑉𝐴)
3624, 32, 19hlatjcl 33465 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑉𝐴) → (𝑃 𝑉) ∈ (Base‘𝐾))
3725, 17, 35, 36syl3anc 1318 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 𝑉) ∈ (Base‘𝐾))
3824, 18, 32latlej2 16833 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝑔𝑃) ∈ (Base‘𝐾)) → (𝑔𝑃) (𝑃 (𝑔𝑃)))
3927, 29, 31, 38syl3anc 1318 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) (𝑃 (𝑔𝑃)))
40 simpl2 1058 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
41 cdlemm10.r . . . . . . . . . . . . . . 15 𝑅 = ((trL‘𝐾)‘𝑊)
4218, 32, 19, 20, 21, 41trljat1 34265 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑅𝑔)) = (𝑃 (𝑔𝑃)))
4315, 16, 40, 42syl3anc 1318 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑅𝑔)) = (𝑃 (𝑔𝑃)))
44 simprr 792 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑅𝑔) 𝑉)
4524, 20, 21, 41trlcl 34263 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇) → (𝑅𝑔) ∈ (Base‘𝐾))
4615, 16, 45syl2anc 691 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑅𝑔) ∈ (Base‘𝐾))
4724, 19atbase 33388 . . . . . . . . . . . . . . . 16 (𝑉𝐴𝑉 ∈ (Base‘𝐾))
4835, 47syl 17 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑉 ∈ (Base‘𝐾))
4924, 18, 32latjlej2 16838 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ ((𝑅𝑔) ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ 𝑃 ∈ (Base‘𝐾))) → ((𝑅𝑔) 𝑉 → (𝑃 (𝑅𝑔)) (𝑃 𝑉)))
5027, 46, 48, 29, 49syl13anc 1320 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ((𝑅𝑔) 𝑉 → (𝑃 (𝑅𝑔)) (𝑃 𝑉)))
5144, 50mpd 15 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑅𝑔)) (𝑃 𝑉))
5243, 51eqbrtrrd 4602 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑃 (𝑔𝑃)) (𝑃 𝑉))
5324, 18, 27, 31, 34, 37, 39, 52lattrd 16830 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) (𝑃 𝑉))
5418, 19, 20, 21ltrnel 34237 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑔𝑃) ∈ 𝐴 ∧ ¬ (𝑔𝑃) 𝑊))
5554simprd 478 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑔𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ¬ (𝑔𝑃) 𝑊)
5615, 16, 40, 55syl3anc 1318 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ¬ (𝑔𝑃) 𝑊)
5753, 56jca 553 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊))
58 breq1 4581 . . . . . . . . . . . 12 (𝑟 = (𝑔𝑃) → (𝑟 (𝑃 𝑉) ↔ (𝑔𝑃) (𝑃 𝑉)))
59 breq1 4581 . . . . . . . . . . . . 13 (𝑟 = (𝑔𝑃) → (𝑟 𝑊 ↔ (𝑔𝑃) 𝑊))
6059notbid 307 . . . . . . . . . . . 12 (𝑟 = (𝑔𝑃) → (¬ 𝑟 𝑊 ↔ ¬ (𝑔𝑃) 𝑊))
6158, 60anbi12d 743 . . . . . . . . . . 11 (𝑟 = (𝑔𝑃) → ((𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊) ↔ ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊)))
62 cdlemm10.c . . . . . . . . . . 11 𝐶 = {𝑟𝐴 ∣ (𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊)}
6361, 62elrab2 3333 . . . . . . . . . 10 ((𝑔𝑃) ∈ 𝐶 ↔ ((𝑔𝑃) ∈ 𝐴 ∧ ((𝑔𝑃) (𝑃 𝑉) ∧ ¬ (𝑔𝑃) 𝑊)))
6423, 57, 63sylanbrc 695 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑔𝑃) ∈ 𝐶)
6518, 19, 20, 21cdlemeiota 34685 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ 𝑔𝑇) → 𝑔 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
6615, 40, 16, 65syl3anc 1318 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → 𝑔 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
6766eqcomd 2616 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔)
68 eqeq2 2621 . . . . . . . . . . . . 13 (𝑠 = (𝑔𝑃) → ((𝑓𝑃) = 𝑠 ↔ (𝑓𝑃) = (𝑔𝑃)))
6968riotabidv 6491 . . . . . . . . . . . 12 (𝑠 = (𝑔𝑃) → (𝑓𝑇 (𝑓𝑃) = 𝑠) = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
7010, 69syl5eq 2656 . . . . . . . . . . 11 (𝑠 = (𝑔𝑃) → 𝐹 = (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)))
7170eqeq1d 2612 . . . . . . . . . 10 (𝑠 = (𝑔𝑃) → (𝐹 = 𝑔 ↔ (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔))
7271rspcev 3282 . . . . . . . . 9 (((𝑔𝑃) ∈ 𝐶 ∧ (𝑓𝑇 (𝑓𝑃) = (𝑔𝑃)) = 𝑔) → ∃𝑠𝐶 𝐹 = 𝑔)
7364, 67, 72syl2anc 691 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)) → ∃𝑠𝐶 𝐹 = 𝑔)
7473ex 449 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑔𝑇 ∧ (𝑅𝑔) 𝑉) → ∃𝑠𝐶 𝐹 = 𝑔))
75 breq1 4581 . . . . . . . . . . . . 13 (𝑟 = 𝑠 → (𝑟 (𝑃 𝑉) ↔ 𝑠 (𝑃 𝑉)))
76 breq1 4581 . . . . . . . . . . . . . 14 (𝑟 = 𝑠 → (𝑟 𝑊𝑠 𝑊))
7776notbid 307 . . . . . . . . . . . . 13 (𝑟 = 𝑠 → (¬ 𝑟 𝑊 ↔ ¬ 𝑠 𝑊))
7875, 77anbi12d 743 . . . . . . . . . . . 12 (𝑟 = 𝑠 → ((𝑟 (𝑃 𝑉) ∧ ¬ 𝑟 𝑊) ↔ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)))
7978, 62elrab2 3333 . . . . . . . . . . 11 (𝑠𝐶 ↔ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)))
80 simpl1 1057 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
81 simpl2l 1107 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃𝐴)
82 simpl2r 1108 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ¬ 𝑃 𝑊)
83 simprl 790 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠𝐴)
84 simprrr 801 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ¬ 𝑠 𝑊)
8518, 19, 20, 21, 10ltrniotacl 34679 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → 𝐹𝑇)
8618, 19, 20, 21, 10ltrniotaval 34681 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → (𝐹𝑃) = 𝑠)
8785, 86jca 553 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑠𝐴 ∧ ¬ 𝑠 𝑊)) → (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠))
8880, 81, 82, 83, 84, 87syl122anc 1327 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠))
89 simp3l 1082 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → 𝐹𝑇)
90 simp11 1084 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
91 simp12 1085 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
92 eqid 2610 . . . . . . . . . . . . . . . . 17 (meet‘𝐾) = (meet‘𝐾)
9318, 32, 92, 19, 20, 21, 41trlval2 34262 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊))
9490, 89, 91, 93syl3anc 1318 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) = ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊))
95 simp3r 1083 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐹𝑃) = 𝑠)
9695oveq2d 6543 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑃 (𝐹𝑃)) = (𝑃 𝑠))
9796oveq1d 6542 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → ((𝑃 (𝐹𝑃))(meet‘𝐾)𝑊) = ((𝑃 𝑠)(meet‘𝐾)𝑊))
9894, 97eqtrd 2644 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) = ((𝑃 𝑠)(meet‘𝐾)𝑊))
99 simpl1l 1105 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝐾 ∈ HL)
100 simpl3l 1109 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑉𝐴)
10118, 32, 19hlatlej1 33473 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑉𝐴) → 𝑃 (𝑃 𝑉))
10299, 81, 100, 101syl3anc 1318 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃 (𝑃 𝑉))
103 simprrl 800 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠 (𝑃 𝑉))
10499, 26syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝐾 ∈ Lat)
10581, 28syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑃 ∈ (Base‘𝐾))
10624, 19atbase 33388 . . . . . . . . . . . . . . . . . . . 20 (𝑠𝐴𝑠 ∈ (Base‘𝐾))
107106ad2antrl 760 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑠 ∈ (Base‘𝐾))
10899, 81, 100, 36syl3anc 1318 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑉) ∈ (Base‘𝐾))
10924, 18, 32latjle12 16834 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑠 ∈ (Base‘𝐾) ∧ (𝑃 𝑉) ∈ (Base‘𝐾))) → ((𝑃 (𝑃 𝑉) ∧ 𝑠 (𝑃 𝑉)) ↔ (𝑃 𝑠) (𝑃 𝑉)))
110104, 105, 107, 108, 109syl13anc 1320 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 (𝑃 𝑉) ∧ 𝑠 (𝑃 𝑉)) ↔ (𝑃 𝑠) (𝑃 𝑉)))
111102, 103, 110mpbi2and 958 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑠) (𝑃 𝑉))
11224, 32, 19hlatjcl 33465 . . . . . . . . . . . . . . . . . . 19 ((𝐾 ∈ HL ∧ 𝑃𝐴𝑠𝐴) → (𝑃 𝑠) ∈ (Base‘𝐾))
11399, 81, 83, 112syl3anc 1318 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝑃 𝑠) ∈ (Base‘𝐾))
114 simpl1r 1106 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑊𝐻)
11524, 20lhpbase 34096 . . . . . . . . . . . . . . . . . . 19 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
116114, 115syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → 𝑊 ∈ (Base‘𝐾))
11724, 18, 92latmlem1 16853 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ Lat ∧ ((𝑃 𝑠) ∈ (Base‘𝐾) ∧ (𝑃 𝑉) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 𝑠) (𝑃 𝑉) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊)))
118104, 113, 108, 116, 117syl13anc 1320 . . . . . . . . . . . . . . . . 17 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠) (𝑃 𝑉) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊)))
119111, 118mpd 15 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠)(meet‘𝐾)𝑊) ((𝑃 𝑉)(meet‘𝐾)𝑊))
12018, 32, 92, 19, 20lhpat4N 34142 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑃 𝑉)(meet‘𝐾)𝑊) = 𝑉)
121120adantr 480 . . . . . . . . . . . . . . . 16 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑉)(meet‘𝐾)𝑊) = 𝑉)
122119, 121breqtrd 4604 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → ((𝑃 𝑠)(meet‘𝐾)𝑊) 𝑉)
1231223adant3 1074 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → ((𝑃 𝑠)(meet‘𝐾)𝑊) 𝑉)
12498, 123eqbrtrd 4600 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝑅𝐹) 𝑉)
12589, 124jca 553 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊)) ∧ (𝐹𝑇 ∧ (𝐹𝑃) = 𝑠)) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
12688, 125mpd3an3 1417 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ (𝑠𝐴 ∧ (𝑠 (𝑃 𝑉) ∧ ¬ 𝑠 𝑊))) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
12779, 126sylan2b 491 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) ∧ 𝑠𝐶) → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉))
128127ex 449 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑠𝐶 → (𝐹𝑇 ∧ (𝑅𝐹) 𝑉)))
129 eleq1 2676 . . . . . . . . . . 11 (𝐹 = 𝑔 → (𝐹𝑇𝑔𝑇))
130 fveq2 6088 . . . . . . . . . . . 12 (𝐹 = 𝑔 → (𝑅𝐹) = (𝑅𝑔))
131130breq1d 4588 . . . . . . . . . . 11 (𝐹 = 𝑔 → ((𝑅𝐹) 𝑉 ↔ (𝑅𝑔) 𝑉))
132129, 131anbi12d 743 . . . . . . . . . 10 (𝐹 = 𝑔 → ((𝐹𝑇 ∧ (𝑅𝐹) 𝑉) ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
133132biimpcd 238 . . . . . . . . 9 ((𝐹𝑇 ∧ (𝑅𝐹) 𝑉) → (𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
134128, 133syl6 34 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑠𝐶 → (𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉))))
135134rexlimdv 3012 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 𝐹 = 𝑔 → (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
13674, 135impbid 201 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ((𝑔𝑇 ∧ (𝑅𝑔) 𝑉) ↔ ∃𝑠𝐶 𝐹 = 𝑔))
13714, 136bitr4d 270 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔 ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉)))
138 fveq2 6088 . . . . . . 7 (𝑓 = 𝑔 → (𝑅𝑓) = (𝑅𝑔))
139138breq1d 4588 . . . . . 6 (𝑓 = 𝑔 → ((𝑅𝑓) 𝑉 ↔ (𝑅𝑔) 𝑉))
140139elrab 3331 . . . . 5 (𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉} ↔ (𝑔𝑇 ∧ (𝑅𝑔) 𝑉))
141137, 140syl6bbr 277 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉}))
142 simp1l 1078 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝐾 ∈ HL)
143 simp1r 1079 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑊𝐻)
144 simp3l 1082 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉𝐴)
145144, 47syl 17 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉 ∈ (Base‘𝐾))
146 simp3r 1083 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → 𝑉 𝑊)
147 cdlemm10.i . . . . . . 7 𝐼 = ((DIsoA‘𝐾)‘𝑊)
14824, 18, 20, 21, 41, 147diaval 35133 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑉 𝑊)) → (𝐼𝑉) = {𝑓𝑇 ∣ (𝑅𝑓) 𝑉})
149142, 143, 145, 146, 148syl22anc 1319 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝐼𝑉) = {𝑓𝑇 ∣ (𝑅𝑓) 𝑉})
150149eleq2d 2673 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑔 ∈ (𝐼𝑉) ↔ 𝑔 ∈ {𝑓𝑇 ∣ (𝑅𝑓) 𝑉}))
151141, 150bitr4d 270 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (∃𝑠𝐶 (𝐺𝑠) = 𝑔𝑔 ∈ (𝐼𝑉)))
1525, 151syl5bb 271 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → (𝑔 ∈ ran 𝐺𝑔 ∈ (𝐼𝑉)))
153152eqrdv 2608 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑉𝐴𝑉 𝑊)) → ran 𝐺 = (𝐼𝑉))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wrex 2897  {crab 2900   class class class wbr 4578  cmpt 4638  ran crn 5029   Fn wfn 5785  cfv 5790  crio 6488  (class class class)co 6527  Basecbs 15644  lecple 15724  joincjn 16716  meetcmee 16717  Latclat 16817  Atomscatm 33362  HLchlt 33449  LHypclh 34082  LTrncltrn 34199  trLctrl 34257  DIsoAcdia 35129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-riotaBAD 33051
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-iun 4452  df-iin 4453  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7037  df-2nd 7038  df-undef 7264  df-map 7724  df-preset 16700  df-poset 16718  df-plt 16730  df-lub 16746  df-glb 16747  df-join 16748  df-meet 16749  df-p0 16811  df-p1 16812  df-lat 16818  df-clat 16880  df-oposet 33275  df-ol 33277  df-oml 33278  df-covers 33365  df-ats 33366  df-atl 33397  df-cvlat 33421  df-hlat 33450  df-llines 33596  df-lplanes 33597  df-lvols 33598  df-lines 33599  df-psubsp 33601  df-pmap 33602  df-padd 33894  df-lhyp 34086  df-laut 34087  df-ldil 34202  df-ltrn 34203  df-trl 34258  df-disoa 35130
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator