This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( 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 )