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