# 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 ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
tendoco.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
Assertion tendococl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\to {S}\circ {T}\in {E}$

### Proof

Step Hyp Ref Expression
1 tendoco.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 tendoco.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
3 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
4 eqid ${⊢}\mathrm{LTrn}\left({K}\right)\left({W}\right)=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
5 eqid ${⊢}\mathrm{trL}\left({K}\right)\left({W}\right)=\mathrm{trL}\left({K}\right)\left({W}\right)$
6 simp1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 simp2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\to {S}\in {E}$
8 1 4 2 tendof ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\right)\to {S}:\mathrm{LTrn}\left({K}\right)\left({W}\right)⟶\mathrm{LTrn}\left({K}\right)\left({W}\right)$
9 6 7 8 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\to {S}:\mathrm{LTrn}\left({K}\right)\left({W}\right)⟶\mathrm{LTrn}\left({K}\right)\left({W}\right)$
10 simp3 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\to {T}\in {E}$
11 1 4 2 tendof ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {T}\in {E}\right)\to {T}:\mathrm{LTrn}\left({K}\right)\left({W}\right)⟶\mathrm{LTrn}\left({K}\right)\left({W}\right)$
12 6 10 11 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\to {T}:\mathrm{LTrn}\left({K}\right)\left({W}\right)⟶\mathrm{LTrn}\left({K}\right)\left({W}\right)$
13 fco ${⊢}\left({S}:\mathrm{LTrn}\left({K}\right)\left({W}\right)⟶\mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {T}:\mathrm{LTrn}\left({K}\right)\left({W}\right)⟶\mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right):\mathrm{LTrn}\left({K}\right)\left({W}\right)⟶\mathrm{LTrn}\left({K}\right)\left({W}\right)$
14 9 12 13 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\to \left({S}\circ {T}\right):\mathrm{LTrn}\left({K}\right)\left({W}\right)⟶\mathrm{LTrn}\left({K}\right)\left({W}\right)$
15 simp11l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {K}\in \mathrm{HL}$
16 simp11r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {W}\in {H}$
17 simp13 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {T}\in {E}$
18 simp2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
19 simp3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
20 1 4 2 tendovalco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\wedge {T}\in {E}\right)\wedge \left({f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\right)\to {T}\left({f}\circ {g}\right)={T}\left({f}\right)\circ {T}\left({g}\right)$
21 15 16 17 18 19 20 syl32anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {T}\left({f}\circ {g}\right)={T}\left({f}\right)\circ {T}\left({g}\right)$
22 21 fveq2d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {S}\left({T}\left({f}\circ {g}\right)\right)={S}\left({T}\left({f}\right)\circ {T}\left({g}\right)\right)$
23 simp12 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {S}\in {E}$
24 simp11 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
25 1 4 2 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {T}\in {E}\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {T}\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
26 24 17 18 25 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {T}\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
27 1 4 2 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {T}\in {E}\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {T}\left({g}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
28 24 17 19 27 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {T}\left({g}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
29 1 4 2 tendovalco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\wedge {S}\in {E}\right)\wedge \left({T}\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {T}\left({g}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\right)\to {S}\left({T}\left({f}\right)\circ {T}\left({g}\right)\right)={S}\left({T}\left({f}\right)\right)\circ {S}\left({T}\left({g}\right)\right)$
30 15 16 23 26 28 29 syl32anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {S}\left({T}\left({f}\right)\circ {T}\left({g}\right)\right)={S}\left({T}\left({f}\right)\right)\circ {S}\left({T}\left({g}\right)\right)$
31 22 30 eqtrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {S}\left({T}\left({f}\circ {g}\right)\right)={S}\left({T}\left({f}\right)\right)\circ {S}\left({T}\left({g}\right)\right)$
32 1 4 ltrnco ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {f}\circ {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
33 24 18 19 32 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {f}\circ {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
34 1 4 2 tendocoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\circ {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\circ {g}\right)={S}\left({T}\left({f}\circ {g}\right)\right)$
35 24 23 17 33 34 syl121anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\circ {g}\right)={S}\left({T}\left({f}\circ {g}\right)\right)$
36 1 4 2 tendocoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\right)={S}\left({T}\left({f}\right)\right)$
37 15 16 23 17 18 36 syl221anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\right)={S}\left({T}\left({f}\right)\right)$
38 1 4 2 tendocoval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\in {E}\wedge {T}\in {E}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({g}\right)={S}\left({T}\left({g}\right)\right)$
39 15 16 23 17 19 38 syl221anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({g}\right)={S}\left({T}\left({g}\right)\right)$
40 37 39 coeq12d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\right)\circ \left({S}\circ {T}\right)\left({g}\right)={S}\left({T}\left({f}\right)\right)\circ {S}\left({T}\left({g}\right)\right)$
41 31 35 40 3eqtr4d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\wedge {g}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\circ {g}\right)=\left({S}\circ {T}\right)\left({f}\right)\circ \left({S}\circ {T}\right)\left({g}\right)$
42 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
43 simpl1l ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {K}\in \mathrm{HL}$
44 43 hllatd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {K}\in \mathrm{Lat}$
45 simpl1 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
46 simpl2 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {S}\in {E}$
47 simpl3 ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {T}\in {E}$
48 simpr ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
49 45 46 47 48 36 syl121anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\right)={S}\left({T}\left({f}\right)\right)$
50 45 47 48 25 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {T}\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
51 1 4 2 tendocl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {S}\left({T}\left({f}\right)\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
52 45 46 50 51 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {S}\left({T}\left({f}\right)\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
53 49 52 eqeltrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)$
54 42 1 4 5 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({S}\circ {T}\right)\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left(\left({S}\circ {T}\right)\left({f}\right)\right)\in {\mathrm{Base}}_{{K}}$
55 45 53 54 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left(\left({S}\circ {T}\right)\left({f}\right)\right)\in {\mathrm{Base}}_{{K}}$
56 42 1 4 5 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {T}\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({T}\left({f}\right)\right)\in {\mathrm{Base}}_{{K}}$
57 45 50 56 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({T}\left({f}\right)\right)\in {\mathrm{Base}}_{{K}}$
58 42 1 4 5 trlcl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)\in {\mathrm{Base}}_{{K}}$
59 45 48 58 syl2anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)\in {\mathrm{Base}}_{{K}}$
60 simpl1r ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to {W}\in {H}$
61 43 60 46 47 48 36 syl221anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \left({S}\circ {T}\right)\left({f}\right)={S}\left({T}\left({f}\right)\right)$
62 61 fveq2d ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left(\left({S}\circ {T}\right)\left({f}\right)\right)=\mathrm{trL}\left({K}\right)\left({W}\right)\left({S}\left({T}\left({f}\right)\right)\right)$
63 3 1 4 5 2 tendotp ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\left({f}\right)\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({S}\left({T}\left({f}\right)\right)\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({T}\left({f}\right)\right)$
64 45 46 50 63 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({S}\left({T}\left({f}\right)\right)\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({T}\left({f}\right)\right)$
65 62 64 eqbrtrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left(\left({S}\circ {T}\right)\left({f}\right)\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({T}\left({f}\right)\right)$
66 3 1 4 5 2 tendotp ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {T}\in {E}\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({T}\left({f}\right)\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)$
67 45 47 48 66 syl3anc ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left({T}\left({f}\right)\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)$
68 42 3 44 55 57 59 65 67 lattrd ${⊢}\left(\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\wedge {f}\in \mathrm{LTrn}\left({K}\right)\left({W}\right)\right)\to \mathrm{trL}\left({K}\right)\left({W}\right)\left(\left({S}\circ {T}\right)\left({f}\right)\right){\le }_{{K}}\mathrm{trL}\left({K}\right)\left({W}\right)\left({f}\right)$
69 3 1 4 5 2 6 14 41 68 istendod ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {S}\in {E}\wedge {T}\in {E}\right)\to {S}\circ {T}\in {E}$