Description: Closure of vector scalar multiplication in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | shmulcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | issh2 | |
|
2 | 1 | simprbi | |
3 | 2 | simprd | |
4 | oveq1 | |
|
5 | 4 | eleq1d | |
6 | oveq2 | |
|
7 | 6 | eleq1d | |
8 | 5 7 | rspc2v | |
9 | 3 8 | syl5com | |
10 | 9 | 3impib | |