# Metamath Proof Explorer

## Theorem tendococl

Description: The composition of two trace-preserving endomorphisms (multiplication in the endormorphism ring) is a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013)

Ref Expression
Hypotheses tendoco.h 𝐻 = ( LHyp ‘ 𝐾 )
tendoco.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
Assertion tendococl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) → ( 𝑆𝑇 ) ∈ 𝐸 )

### Proof

Step Hyp Ref Expression
1 tendoco.h 𝐻 = ( LHyp ‘ 𝐾 )
2 tendoco.e 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
3 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 eqid ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
7 simp2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) → 𝑆𝐸 )
8 1 4 2 tendof ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸 ) → 𝑆 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
9 6 7 8 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) → 𝑆 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
10 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) → 𝑇𝐸 )
11 1 4 2 tendof ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑇𝐸 ) → 𝑇 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
12 6 10 11 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) → 𝑇 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
13 fco ( ( 𝑆 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑇 : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑆𝑇 ) : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
14 9 12 13 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) → ( 𝑆𝑇 ) : ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ⟶ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
15 simp11l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝐾 ∈ HL )
16 simp11r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑊𝐻 )
17 simp13 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑇𝐸 )
18 simp2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
19 simp3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
20 1 4 2 tendovalco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻𝑇𝐸 ) ∧ ( 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑇 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑇𝑓 ) ∘ ( 𝑇𝑔 ) ) )
21 15 16 17 18 19 20 syl32anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑇 ‘ ( 𝑓𝑔 ) ) = ( ( 𝑇𝑓 ) ∘ ( 𝑇𝑔 ) ) )
22 21 fveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑆 ‘ ( 𝑇 ‘ ( 𝑓𝑔 ) ) ) = ( 𝑆 ‘ ( ( 𝑇𝑓 ) ∘ ( 𝑇𝑔 ) ) ) )
23 simp12 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑆𝐸 )
24 simp11 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
25 1 4 2 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑇𝐸𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑇𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
26 24 17 18 25 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑇𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
27 1 4 2 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑇𝐸𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑇𝑔 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
28 24 17 19 27 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑇𝑔 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
29 1 4 2 tendovalco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻𝑆𝐸 ) ∧ ( ( 𝑇𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑇𝑔 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑆 ‘ ( ( 𝑇𝑓 ) ∘ ( 𝑇𝑔 ) ) ) = ( ( 𝑆 ‘ ( 𝑇𝑓 ) ) ∘ ( 𝑆 ‘ ( 𝑇𝑔 ) ) ) )
30 15 16 23 26 28 29 syl32anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑆 ‘ ( ( 𝑇𝑓 ) ∘ ( 𝑇𝑔 ) ) ) = ( ( 𝑆 ‘ ( 𝑇𝑓 ) ) ∘ ( 𝑆 ‘ ( 𝑇𝑔 ) ) ) )
31 22 30 eqtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑆 ‘ ( 𝑇 ‘ ( 𝑓𝑔 ) ) ) = ( ( 𝑆 ‘ ( 𝑇𝑓 ) ) ∘ ( 𝑆 ‘ ( 𝑇𝑔 ) ) ) )
32 1 4 ltrnco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑓𝑔 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
33 24 18 19 32 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑓𝑔 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
34 1 4 2 tendocoval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐸𝑇𝐸 ) ∧ ( 𝑓𝑔 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ ( 𝑓𝑔 ) ) = ( 𝑆 ‘ ( 𝑇 ‘ ( 𝑓𝑔 ) ) ) )
35 24 23 17 33 34 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ ( 𝑓𝑔 ) ) = ( 𝑆 ‘ ( 𝑇 ‘ ( 𝑓𝑔 ) ) ) )
36 1 4 2 tendocoval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ 𝑓 ) = ( 𝑆 ‘ ( 𝑇𝑓 ) ) )
37 15 16 23 17 18 36 syl221anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ 𝑓 ) = ( 𝑆 ‘ ( 𝑇𝑓 ) ) )
38 1 4 2 tendocoval ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑆𝐸𝑇𝐸 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ 𝑔 ) = ( 𝑆 ‘ ( 𝑇𝑔 ) ) )
39 15 16 23 17 19 38 syl221anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ 𝑔 ) = ( 𝑆 ‘ ( 𝑇𝑔 ) ) )
40 37 39 coeq12d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( 𝑆𝑇 ) ‘ 𝑓 ) ∘ ( ( 𝑆𝑇 ) ‘ 𝑔 ) ) = ( ( 𝑆 ‘ ( 𝑇𝑓 ) ) ∘ ( 𝑆 ‘ ( 𝑇𝑔 ) ) ) )
41 31 35 40 3eqtr4d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑔 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ ( 𝑓𝑔 ) ) = ( ( ( 𝑆𝑇 ) ‘ 𝑓 ) ∘ ( ( 𝑆𝑇 ) ‘ 𝑔 ) ) )
42 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
43 simpl1l ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝐾 ∈ HL )
44 43 hllatd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝐾 ∈ Lat )
45 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
46 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑆𝐸 )
47 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑇𝐸 )
48 simpr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
49 45 46 47 48 36 syl121anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ 𝑓 ) = ( 𝑆 ‘ ( 𝑇𝑓 ) ) )
50 45 47 48 25 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑇𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
51 1 4 2 tendocl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸 ∧ ( 𝑇𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑆 ‘ ( 𝑇𝑓 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
52 45 46 50 51 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑆 ‘ ( 𝑇𝑓 ) ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
53 49 52 eqeltrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ 𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
54 42 1 4 5 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑆𝑇 ) ‘ 𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑆𝑇 ) ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐾 ) )
55 45 53 54 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑆𝑇 ) ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐾 ) )
56 42 1 4 5 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑇𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑇𝑓 ) ) ∈ ( Base ‘ 𝐾 ) )
57 45 50 56 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑇𝑓 ) ) ∈ ( Base ‘ 𝐾 ) )
58 42 1 4 5 trlcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐾 ) )
59 45 48 58 syl2anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ∈ ( Base ‘ 𝐾 ) )
60 simpl1r ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑊𝐻 )
61 43 60 46 47 48 36 syl221anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑆𝑇 ) ‘ 𝑓 ) = ( 𝑆 ‘ ( 𝑇𝑓 ) ) )
62 61 fveq2d ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑆𝑇 ) ‘ 𝑓 ) ) = ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( 𝑇𝑓 ) ) ) )
63 3 1 4 5 2 tendotp ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸 ∧ ( 𝑇𝑓 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( 𝑇𝑓 ) ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑇𝑓 ) ) )
64 45 46 50 63 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑆 ‘ ( 𝑇𝑓 ) ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑇𝑓 ) ) )
65 62 64 eqbrtrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑆𝑇 ) ‘ 𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑇𝑓 ) ) )
66 3 1 4 5 2 tendotp ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑇𝐸𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑇𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) )
67 45 47 48 66 syl3anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑇𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) )
68 42 3 44 55 57 59 65 67 lattrd ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) ∧ 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑆𝑇 ) ‘ 𝑓 ) ) ( le ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) )
69 3 1 4 5 2 6 14 41 68 istendod ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑆𝐸𝑇𝐸 ) → ( 𝑆𝑇 ) ∈ 𝐸 )