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

Theorem trlcolem 38021
Description: Lemma for trlco 38022. (Contributed by NM, 1-Jun-2013.)
Hypotheses
Ref Expression
trlco.l = (le‘𝐾)
trlco.j = (join‘𝐾)
trlco.h 𝐻 = (LHyp‘𝐾)
trlco.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlco.r 𝑅 = ((trL‘𝐾)‘𝑊)
trlcolem.m = (meet‘𝐾)
trlcolem.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
trlcolem (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝐹𝐺)) ((𝑅𝐹) (𝑅𝐺)))

Proof of Theorem trlcolem
StepHypRef Expression
1 simp1l 1194 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ HL)
21hllatd 36659 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ Lat)
3 simp3l 1198 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
4 eqid 2801 . . . . . . 7 (Base‘𝐾) = (Base‘𝐾)
5 trlcolem.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
64, 5atbase 36584 . . . . . 6 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
73, 6syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 ∈ (Base‘𝐾))
8 simp1 1133 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
9 simp2r 1197 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐺𝑇)
10 trlco.l . . . . . . . 8 = (le‘𝐾)
11 trlco.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
12 trlco.t . . . . . . . 8 𝑇 = ((LTrn‘𝐾)‘𝑊)
1310, 5, 11, 12ltrnat 37435 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇𝑃𝐴) → (𝐺𝑃) ∈ 𝐴)
148, 9, 3, 13syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐺𝑃) ∈ 𝐴)
154, 5atbase 36584 . . . . . 6 ((𝐺𝑃) ∈ 𝐴 → (𝐺𝑃) ∈ (Base‘𝐾))
1614, 15syl 17 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐺𝑃) ∈ (Base‘𝐾))
17 trlco.j . . . . . 6 = (join‘𝐾)
184, 10, 17latlej1 17666 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐺𝑃) ∈ (Base‘𝐾)) → 𝑃 (𝑃 (𝐺𝑃)))
192, 7, 16, 18syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃 (𝑃 (𝐺𝑃)))
204, 17, 5hlatjcl 36662 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑃𝐴 ∧ (𝐺𝑃) ∈ 𝐴) → (𝑃 (𝐺𝑃)) ∈ (Base‘𝐾))
211, 3, 14, 20syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝐺𝑃)) ∈ (Base‘𝐾))
22 simp2l 1196 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐹𝑇)
234, 11, 12ltrncl 37420 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝐺𝑃) ∈ (Base‘𝐾)) → (𝐹‘(𝐺𝑃)) ∈ (Base‘𝐾))
248, 22, 16, 23syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹‘(𝐺𝑃)) ∈ (Base‘𝐾))
254, 10, 17latjlej1 17671 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ (𝑃 (𝐺𝑃)) ∈ (Base‘𝐾) ∧ (𝐹‘(𝐺𝑃)) ∈ (Base‘𝐾))) → (𝑃 (𝑃 (𝐺𝑃)) → (𝑃 (𝐹‘(𝐺𝑃))) ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃)))))
262, 7, 21, 24, 25syl13anc 1369 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝑃 (𝐺𝑃)) → (𝑃 (𝐹‘(𝐺𝑃))) ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃)))))
2719, 26mpd 15 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝐹‘(𝐺𝑃))) ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))))
284, 17latjcl 17657 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐹‘(𝐺𝑃)) ∈ (Base‘𝐾)) → (𝑃 (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾))
292, 7, 24, 28syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾))
304, 17latjcl 17657 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 (𝐺𝑃)) ∈ (Base‘𝐾) ∧ (𝐹‘(𝐺𝑃)) ∈ (Base‘𝐾)) → ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾))
312, 21, 24, 30syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾))
32 simp1r 1195 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊𝐻)
334, 11lhpbase 37293 . . . . 5 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
3432, 33syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑊 ∈ (Base‘𝐾))
35 trlcolem.m . . . . 5 = (meet‘𝐾)
364, 10, 35latmlem1 17687 . . . 4 ((𝐾 ∈ Lat ∧ ((𝑃 (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾) ∧ ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 (𝐹‘(𝐺𝑃))) ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) (((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) 𝑊)))
372, 29, 31, 34, 36syl13anc 1369 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐹‘(𝐺𝑃))) ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) (((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) 𝑊)))
3827, 37mpd 15 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊) (((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) 𝑊))
3911, 12ltrnco 38014 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐺𝑇) → (𝐹𝐺) ∈ 𝑇)
408, 22, 9, 39syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹𝐺) ∈ 𝑇)
41 trlco.r . . . . 5 𝑅 = ((trL‘𝐾)‘𝑊)
4210, 17, 35, 5, 11, 12, 41trlval2 37458 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝐺) ∈ 𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝐹𝐺)) = ((𝑃 ((𝐹𝐺)‘𝑃)) 𝑊))
4340, 42syld3an2 1408 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝐹𝐺)) = ((𝑃 ((𝐹𝐺)‘𝑃)) 𝑊))
4410, 5, 11, 12ltrncoval 37440 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ 𝑃𝐴) → ((𝐹𝐺)‘𝑃) = (𝐹‘(𝐺𝑃)))
45443adant3r 1178 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐹𝐺)‘𝑃) = (𝐹‘(𝐺𝑃)))
4645oveq2d 7155 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑃 ((𝐹𝐺)‘𝑃)) = (𝑃 (𝐹‘(𝐺𝑃))))
4746oveq1d 7154 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 ((𝐹𝐺)‘𝑃)) 𝑊) = ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊))
4843, 47eqtrd 2836 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝐹𝐺)) = ((𝑃 (𝐹‘(𝐺𝑃))) 𝑊))
4910, 5, 11, 12ltrnel 37434 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐺𝑃) ∈ 𝐴 ∧ ¬ (𝐺𝑃) 𝑊))
509, 49syld3an2 1408 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐺𝑃) ∈ 𝐴 ∧ ¬ (𝐺𝑃) 𝑊))
5110, 17, 35, 5, 11, 12, 41trlval2 37458 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ ((𝐺𝑃) ∈ 𝐴 ∧ ¬ (𝐺𝑃) 𝑊)) → (𝑅𝐹) = (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊))
528, 22, 50, 51syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐹) = (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊))
5310, 17, 35, 5, 11, 12, 41trlval2 37458 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇 ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐺) = ((𝑃 (𝐺𝑃)) 𝑊))
549, 53syld3an2 1408 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅𝐺) = ((𝑃 (𝐺𝑃)) 𝑊))
5552, 54oveq12d 7157 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑅𝐹) (𝑅𝐺)) = ((((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊) ((𝑃 (𝐺𝑃)) 𝑊)))
5610, 5, 11, 12ltrnat 37435 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇 ∧ (𝐺𝑃) ∈ 𝐴) → (𝐹‘(𝐺𝑃)) ∈ 𝐴)
578, 22, 14, 56syl3anc 1368 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐹‘(𝐺𝑃)) ∈ 𝐴)
584, 17, 5hlatjcl 36662 . . . . . 6 ((𝐾 ∈ HL ∧ (𝐺𝑃) ∈ 𝐴 ∧ (𝐹‘(𝐺𝑃)) ∈ 𝐴) → ((𝐺𝑃) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾))
591, 14, 57, 58syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐺𝑃) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾))
604, 35latmcl 17658 . . . . 5 ((𝐾 ∈ Lat ∧ ((𝐺𝑃) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊) ∈ (Base‘𝐾))
612, 59, 34, 60syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊) ∈ (Base‘𝐾))
624, 35latmcl 17658 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑃 (𝐺𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 (𝐺𝑃)) 𝑊) ∈ (Base‘𝐾))
632, 21, 34, 62syl3anc 1368 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐺𝑃)) 𝑊) ∈ (Base‘𝐾))
644, 17latjcom 17665 . . . 4 ((𝐾 ∈ Lat ∧ (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊) ∈ (Base‘𝐾) ∧ ((𝑃 (𝐺𝑃)) 𝑊) ∈ (Base‘𝐾)) → ((((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊) ((𝑃 (𝐺𝑃)) 𝑊)) = (((𝑃 (𝐺𝑃)) 𝑊) (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊)))
652, 61, 63, 64syl3anc 1368 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊) ((𝑃 (𝐺𝑃)) 𝑊)) = (((𝑃 (𝐺𝑃)) 𝑊) (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊)))
664, 17latjcl 17657 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝐺𝑃) ∈ (Base‘𝐾) ∧ (𝐹‘(𝐺𝑃)) ∈ (Base‘𝐾)) → ((𝐺𝑃) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾))
672, 16, 24, 66syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝐺𝑃) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾))
684, 10, 35latmle2 17683 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑃 (𝐺𝑃)) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 (𝐺𝑃)) 𝑊) 𝑊)
692, 21, 34, 68syl3anc 1368 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐺𝑃)) 𝑊) 𝑊)
704, 10, 17, 35, 11lhpmod6i1 37334 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (((𝑃 (𝐺𝑃)) 𝑊) ∈ (Base‘𝐾) ∧ ((𝐺𝑃) (𝐹‘(𝐺𝑃))) ∈ (Base‘𝐾)) ∧ ((𝑃 (𝐺𝑃)) 𝑊) 𝑊) → (((𝑃 (𝐺𝑃)) 𝑊) (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊)) = ((((𝑃 (𝐺𝑃)) 𝑊) ((𝐺𝑃) (𝐹‘(𝐺𝑃)))) 𝑊))
718, 63, 67, 69, 70syl121anc 1372 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑃 (𝐺𝑃)) 𝑊) (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊)) = ((((𝑃 (𝐺𝑃)) 𝑊) ((𝐺𝑃) (𝐹‘(𝐺𝑃)))) 𝑊))
724, 17latjass 17701 . . . . . . 7 ((𝐾 ∈ Lat ∧ (((𝑃 (𝐺𝑃)) 𝑊) ∈ (Base‘𝐾) ∧ (𝐺𝑃) ∈ (Base‘𝐾) ∧ (𝐹‘(𝐺𝑃)) ∈ (Base‘𝐾))) → ((((𝑃 (𝐺𝑃)) 𝑊) (𝐺𝑃)) (𝐹‘(𝐺𝑃))) = (((𝑃 (𝐺𝑃)) 𝑊) ((𝐺𝑃) (𝐹‘(𝐺𝑃)))))
732, 63, 16, 24, 72syl13anc 1369 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((((𝑃 (𝐺𝑃)) 𝑊) (𝐺𝑃)) (𝐹‘(𝐺𝑃))) = (((𝑃 (𝐺𝑃)) 𝑊) ((𝐺𝑃) (𝐹‘(𝐺𝑃)))))
744, 10, 17latlej2 17667 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ (𝐺𝑃) ∈ (Base‘𝐾)) → (𝐺𝑃) (𝑃 (𝐺𝑃)))
752, 7, 16, 74syl3anc 1368 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝐺𝑃) (𝑃 (𝐺𝑃)))
764, 10, 17, 35, 11lhpmod2i2 37333 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑃 (𝐺𝑃)) ∈ (Base‘𝐾) ∧ (𝐺𝑃) ∈ (Base‘𝐾)) ∧ (𝐺𝑃) (𝑃 (𝐺𝑃))) → (((𝑃 (𝐺𝑃)) 𝑊) (𝐺𝑃)) = ((𝑃 (𝐺𝑃)) (𝑊 (𝐺𝑃))))
778, 21, 16, 75, 76syl121anc 1372 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑃 (𝐺𝑃)) 𝑊) (𝐺𝑃)) = ((𝑃 (𝐺𝑃)) (𝑊 (𝐺𝑃))))
78 eqid 2801 . . . . . . . . . . 11 (1.‘𝐾) = (1.‘𝐾)
7910, 17, 78, 5, 11lhpjat1 37315 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐺𝑃) ∈ 𝐴 ∧ ¬ (𝐺𝑃) 𝑊)) → (𝑊 (𝐺𝑃)) = (1.‘𝐾))
808, 50, 79syl2anc 587 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑊 (𝐺𝑃)) = (1.‘𝐾))
8180oveq2d 7155 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐺𝑃)) (𝑊 (𝐺𝑃))) = ((𝑃 (𝐺𝑃)) (1.‘𝐾)))
82 hlol 36656 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ OL)
831, 82syl 17 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ OL)
844, 35, 78olm11 36522 . . . . . . . . 9 ((𝐾 ∈ OL ∧ (𝑃 (𝐺𝑃)) ∈ (Base‘𝐾)) → ((𝑃 (𝐺𝑃)) (1.‘𝐾)) = (𝑃 (𝐺𝑃)))
8583, 21, 84syl2anc 587 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑃 (𝐺𝑃)) (1.‘𝐾)) = (𝑃 (𝐺𝑃)))
8677, 81, 853eqtrd 2840 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑃 (𝐺𝑃)) 𝑊) (𝐺𝑃)) = (𝑃 (𝐺𝑃)))
8786oveq1d 7154 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((((𝑃 (𝐺𝑃)) 𝑊) (𝐺𝑃)) (𝐹‘(𝐺𝑃))) = ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))))
8873, 87eqtr3d 2838 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑃 (𝐺𝑃)) 𝑊) ((𝐺𝑃) (𝐹‘(𝐺𝑃)))) = ((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))))
8988oveq1d 7154 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((((𝑃 (𝐺𝑃)) 𝑊) ((𝐺𝑃) (𝐹‘(𝐺𝑃)))) 𝑊) = (((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) 𝑊))
9071, 89eqtrd 2836 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (((𝑃 (𝐺𝑃)) 𝑊) (((𝐺𝑃) (𝐹‘(𝐺𝑃))) 𝑊)) = (((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) 𝑊))
9155, 65, 903eqtrd 2840 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ((𝑅𝐹) (𝑅𝐺)) = (((𝑃 (𝐺𝑃)) (𝐹‘(𝐺𝑃))) 𝑊))
9238, 48, 913brtr4d 5065 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝐺𝑇) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑅‘(𝐹𝐺)) ((𝑅𝐹) (𝑅𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2112   class class class wbr 5033  ccom 5527  cfv 6328  (class class class)co 7139  Basecbs 16479  lecple 16568  joincjn 17550  meetcmee 17551  1.cp1 17644  Latclat 17651  OLcol 36469  Atomscatm 36558  HLchlt 36645  LHypclh 37279  LTrncltrn 37396  trLctrl 37453
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-riotaBAD 36248
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 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  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 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-1st 7675  df-2nd 7676  df-undef 7926  df-map 8395  df-proset 17534  df-poset 17552  df-plt 17564  df-lub 17580  df-glb 17581  df-join 17582  df-meet 17583  df-p0 17645  df-p1 17646  df-lat 17652  df-clat 17714  df-oposet 36471  df-ol 36473  df-oml 36474  df-covers 36561  df-ats 36562  df-atl 36593  df-cvlat 36617  df-hlat 36646  df-llines 36793  df-lplanes 36794  df-lvols 36795  df-lines 36796  df-psubsp 36798  df-pmap 36799  df-padd 37091  df-lhyp 37283  df-laut 37284  df-ldil 37399  df-ltrn 37400  df-trl 37454
This theorem is referenced by:  trlco  38022
  Copyright terms: Public domain W3C validator