Metamath Proof Explorer


Theorem shmulcl

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 HSABHABH

Proof

Step Hyp Ref Expression
1 issh2 HSH0HxHyHx+yHxyHxyH
2 1 simprbi HSxHyHx+yHxyHxyH
3 2 simprd HSxyHxyH
4 oveq1 x=Axy=Ay
5 4 eleq1d x=AxyHAyH
6 oveq2 y=BAy=AB
7 6 eleq1d y=BAyHABH
8 5 7 rspc2v ABHxyHxyHABH
9 3 8 syl5com HSABHABH
10 9 3impib HSABHABH