This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑆 ∈ 𝐸 ∧ 𝑇 ∈ 𝐸 ) → ( 𝑆 ∘ 𝑇 ) ∈ 𝐸 )