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

Theorem cdlemg6c 40321
Description: TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)
Hypotheses
Ref Expression
cdlemg4.l = (le‘𝐾)
cdlemg4.a 𝐴 = (Atoms‘𝐾)
cdlemg4.h 𝐻 = (LHyp‘𝐾)
cdlemg4.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemg4.r 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemg4.j = (join‘𝐾)
cdlemg4b.v 𝑉 = (𝑅𝐺)
Assertion
Ref Expression
cdlemg6c (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → (((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉)) → (𝐹‘(𝐺𝑄)) = 𝑄))
Distinct variable groups:   𝐴,𝑟   𝐹,𝑟   𝐺,𝑟   𝐻,𝑟   ,𝑟   𝐾,𝑟   ,𝑟   𝑃,𝑟   𝑄,𝑟   𝑇,𝑟   𝑉,𝑟   𝑊,𝑟
Allowed substitution hint:   𝑅(𝑟)

Proof of Theorem cdlemg6c
StepHypRef Expression
1 simpl1 1188 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 simprl 769 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑟𝐴 ∧ ¬ 𝑟 𝑊))
3 simpl22 1249 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑄𝐴 ∧ ¬ 𝑄 𝑊))
4 simpl23 1250 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝐹𝑇)
5 simpl31 1251 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝐺𝑇)
6 simprr 771 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → ¬ 𝑟 (𝑃 𝑉))
7 simpl1l 1221 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝐾 ∈ HL)
8 simp22l 1289 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → 𝑄𝐴)
98adantr 479 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑄𝐴)
10 simprll 777 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑟𝐴)
11 cdlemg4b.v . . . . . . 7 𝑉 = (𝑅𝐺)
12 eqid 2726 . . . . . . . . 9 (Base‘𝐾) = (Base‘𝐾)
13 cdlemg4.h . . . . . . . . 9 𝐻 = (LHyp‘𝐾)
14 cdlemg4.t . . . . . . . . 9 𝑇 = ((LTrn‘𝐾)‘𝑊)
15 cdlemg4.r . . . . . . . . 9 𝑅 = ((trL‘𝐾)‘𝑊)
1612, 13, 14, 15trlcl 39865 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇) → (𝑅𝐺) ∈ (Base‘𝐾))
171, 5, 16syl2anc 582 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑅𝐺) ∈ (Base‘𝐾))
1811, 17eqeltrid 2830 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑉 ∈ (Base‘𝐾))
19 simp22r 1290 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → ¬ 𝑄 𝑊)
2019adantr 479 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → ¬ 𝑄 𝑊)
21 cdlemg4.l . . . . . . . . . . 11 = (le‘𝐾)
2221, 13, 14, 15trlle 39885 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇) → (𝑅𝐺) 𝑊)
231, 5, 22syl2anc 582 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑅𝐺) 𝑊)
2411, 23eqbrtrid 5190 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑉 𝑊)
25 simp1l 1194 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → 𝐾 ∈ HL)
2625hllatd 39064 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → 𝐾 ∈ Lat)
2726adantr 479 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝐾 ∈ Lat)
28 cdlemg4.a . . . . . . . . . . . 12 𝐴 = (Atoms‘𝐾)
2912, 28atbase 38989 . . . . . . . . . . 11 (𝑄𝐴𝑄 ∈ (Base‘𝐾))
308, 29syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → 𝑄 ∈ (Base‘𝐾))
3130adantr 479 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑄 ∈ (Base‘𝐾))
32 simp1r 1195 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → 𝑊𝐻)
3312, 13lhpbase 39699 . . . . . . . . . . 11 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3432, 33syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → 𝑊 ∈ (Base‘𝐾))
3534adantr 479 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑊 ∈ (Base‘𝐾))
3612, 21lattr 18471 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 𝑉𝑉 𝑊) → 𝑄 𝑊))
3727, 31, 18, 35, 36syl13anc 1369 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → ((𝑄 𝑉𝑉 𝑊) → 𝑄 𝑊))
3824, 37mpan2d 692 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑄 𝑉𝑄 𝑊))
3920, 38mtod 197 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → ¬ 𝑄 𝑉)
40 cdlemg4.j . . . . . . 7 = (join‘𝐾)
4112, 21, 40, 28hlexch2 39084 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑄𝐴𝑟𝐴𝑉 ∈ (Base‘𝐾)) ∧ ¬ 𝑄 𝑉) → (𝑄 (𝑟 𝑉) → 𝑟 (𝑄 𝑉)))
427, 9, 10, 18, 39, 41syl131anc 1380 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑄 (𝑟 𝑉) → 𝑟 (𝑄 𝑉)))
43 simpl32 1252 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑄 (𝑃 𝑉))
44 simp21l 1287 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → 𝑃𝐴)
4544adantr 479 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑃𝐴)
4612, 28atbase 38989 . . . . . . . . 9 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
4745, 46syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑃 ∈ (Base‘𝐾))
4812, 21, 40latlej2 18476 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾)) → 𝑉 (𝑃 𝑉))
4927, 47, 18, 48syl3anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑉 (𝑃 𝑉))
5012, 40latjcl 18466 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾)) → (𝑃 𝑉) ∈ (Base‘𝐾))
5127, 47, 18, 50syl3anc 1368 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑃 𝑉) ∈ (Base‘𝐾))
5212, 21, 40latjle12 18477 . . . . . . . 8 ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾) ∧ (𝑃 𝑉) ∈ (Base‘𝐾))) → ((𝑄 (𝑃 𝑉) ∧ 𝑉 (𝑃 𝑉)) ↔ (𝑄 𝑉) (𝑃 𝑉)))
5327, 31, 18, 51, 52syl13anc 1369 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → ((𝑄 (𝑃 𝑉) ∧ 𝑉 (𝑃 𝑉)) ↔ (𝑄 𝑉) (𝑃 𝑉)))
5443, 49, 53mpbi2and 710 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑄 𝑉) (𝑃 𝑉))
5512, 28atbase 38989 . . . . . . . 8 (𝑟𝐴𝑟 ∈ (Base‘𝐾))
5610, 55syl 17 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → 𝑟 ∈ (Base‘𝐾))
5712, 40latjcl 18466 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑄 ∈ (Base‘𝐾) ∧ 𝑉 ∈ (Base‘𝐾)) → (𝑄 𝑉) ∈ (Base‘𝐾))
5827, 31, 18, 57syl3anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑄 𝑉) ∈ (Base‘𝐾))
5912, 21lattr 18471 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑟 ∈ (Base‘𝐾) ∧ (𝑄 𝑉) ∈ (Base‘𝐾) ∧ (𝑃 𝑉) ∈ (Base‘𝐾))) → ((𝑟 (𝑄 𝑉) ∧ (𝑄 𝑉) (𝑃 𝑉)) → 𝑟 (𝑃 𝑉)))
6027, 56, 58, 51, 59syl13anc 1369 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → ((𝑟 (𝑄 𝑉) ∧ (𝑄 𝑉) (𝑃 𝑉)) → 𝑟 (𝑃 𝑉)))
6154, 60mpan2d 692 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑟 (𝑄 𝑉) → 𝑟 (𝑃 𝑉)))
6242, 61syld 47 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑄 (𝑟 𝑉) → 𝑟 (𝑃 𝑉)))
636, 62mtod 197 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → ¬ 𝑄 (𝑟 𝑉))
64 simpl21 1248 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝑃𝐴 ∧ ¬ 𝑃 𝑊))
65 simpl33 1253 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝐹‘(𝐺𝑃)) = 𝑃)
6621, 28, 13, 14, 15, 40, 11cdlemg6a 40319 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇 ∧ ¬ 𝑟 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → (𝐹‘(𝐺𝑟)) = 𝑟)
671, 64, 2, 4, 5, 6, 65, 66syl133anc 1390 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝐹‘(𝐺𝑟)) = 𝑟)
6821, 28, 13, 14, 15, 40, 11cdlemg6b 40320 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇 ∧ ¬ 𝑄 (𝑟 𝑉) ∧ (𝐹‘(𝐺𝑟)) = 𝑟)) → (𝐹‘(𝐺𝑄)) = 𝑄)
691, 2, 3, 4, 5, 63, 67, 68syl133anc 1390 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉))) → (𝐹‘(𝐺𝑄)) = 𝑄)
7069ex 411 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊) ∧ 𝐹𝑇) ∧ (𝐺𝑇𝑄 (𝑃 𝑉) ∧ (𝐹‘(𝐺𝑃)) = 𝑃)) → (((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ ¬ 𝑟 (𝑃 𝑉)) → (𝐹‘(𝐺𝑄)) = 𝑄))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099   class class class wbr 5155  cfv 6556  (class class class)co 7426  Basecbs 17215  lecple 17275  joincjn 18338  Latclat 18458  Atomscatm 38963  HLchlt 39050  LHypclh 39685  LTrncltrn 39802  trLctrl 39859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5292  ax-sep 5306  ax-nul 5313  ax-pow 5371  ax-pr 5435  ax-un 7748  ax-riotaBAD 38653
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4916  df-iun 5005  df-iin 5006  df-br 5156  df-opab 5218  df-mpt 5239  df-id 5582  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-1st 8005  df-2nd 8006  df-undef 8290  df-map 8859  df-proset 18322  df-poset 18340  df-plt 18357  df-lub 18373  df-glb 18374  df-join 18375  df-meet 18376  df-p0 18452  df-p1 18453  df-lat 18459  df-clat 18526  df-oposet 38876  df-ol 38878  df-oml 38879  df-covers 38966  df-ats 38967  df-atl 38998  df-cvlat 39022  df-hlat 39051  df-llines 39199  df-lplanes 39200  df-lvols 39201  df-lines 39202  df-psubsp 39204  df-pmap 39205  df-padd 39497  df-lhyp 39689  df-laut 39690  df-ldil 39805  df-ltrn 39806  df-trl 39860
This theorem is referenced by:  cdlemg6d  40322
  Copyright terms: Public domain W3C validator