Metamath Proof Explorer


Theorem tendospcl

Description: Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013)

Ref Expression
Hypotheses tendosp.h H = LHyp K
tendosp.t T = LTrn K W
tendosp.e E = TEndo K W
Assertion tendospcl K V W H U E F T U F T

Proof

Step Hyp Ref Expression
1 tendosp.h H = LHyp K
2 tendosp.t T = LTrn K W
3 tendosp.e E = TEndo K W
4 1 2 3 tendocl K V W H U E F T U F T