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 e. V /\ W e. H ) /\ U e. E /\ F e. T ) -> ( U ` F ) e. T ) |
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 e. V /\ W e. H ) /\ U e. E /\ F e. T ) -> ( U ` F ) e. T ) |