Description: Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tendosp.h | ||
tendosp.t | |||
tendosp.e | |||
Assertion | tendospcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tendosp.h | ||
2 | tendosp.t | ||
3 | tendosp.e | ||
4 | 1 2 3 | tendocl |