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	|- ( ( H e. SH /\ A e. CC /\ B e. H ) -> ( A .h B ) e. H )

Proof

Step	Hyp	Ref	Expression
1		issh2	|- ( H e. SH <-> ( ( H C_ ~H /\ 0h e. H ) /\ ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) ) )
2	1	simprbi	|- ( H e. SH -> ( A. x e. H A. y e. H ( x +h y ) e. H /\ A. x e. CC A. y e. H ( x .h y ) e. H ) )
3	2	simprd	|- ( H e. SH -> A. x e. CC A. y e. H ( x .h y ) e. H )
4		oveq1	|- ( x = A -> ( x .h y ) = ( A .h y ) )
5	4	eleq1d	|- ( x = A -> ( ( x .h y ) e. H <-> ( A .h y ) e. H ) )
6		oveq2	|- ( y = B -> ( A .h y ) = ( A .h B ) )
7	6	eleq1d	|- ( y = B -> ( ( A .h y ) e. H <-> ( A .h B ) e. H ) )
8	5 7	rspc2v	|- ( ( A e. CC /\ B e. H ) -> ( A. x e. CC A. y e. H ( x .h y ) e. H -> ( A .h B ) e. H ) )
9	3 8	syl5com	|- ( H e. SH -> ( ( A e. CC /\ B e. H ) -> ( A .h B ) e. H ) )
10	9	3impib	|- ( ( H e. SH /\ A e. CC /\ B e. H ) -> ( A .h B ) e. H )