Metamath Proof Explorer


Theorem sspsval

Description: Scalar multiplication on a subspace in terms of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ssps.y
|- Y = ( BaseSet ` W )
ssps.s
|- S = ( .sOLD ` U )
ssps.r
|- R = ( .sOLD ` W )
ssps.h
|- H = ( SubSp ` U )
Assertion sspsval
|- ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. CC /\ B e. Y ) ) -> ( A R B ) = ( A S B ) )

Proof

Step Hyp Ref Expression
1 ssps.y
 |-  Y = ( BaseSet ` W )
2 ssps.s
 |-  S = ( .sOLD ` U )
3 ssps.r
 |-  R = ( .sOLD ` W )
4 ssps.h
 |-  H = ( SubSp ` U )
5 1 2 3 4 ssps
 |-  ( ( U e. NrmCVec /\ W e. H ) -> R = ( S |` ( CC X. Y ) ) )
6 5 oveqd
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( A R B ) = ( A ( S |` ( CC X. Y ) ) B ) )
7 ovres
 |-  ( ( A e. CC /\ B e. Y ) -> ( A ( S |` ( CC X. Y ) ) B ) = ( A S B ) )
8 6 7 sylan9eq
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ ( A e. CC /\ B e. Y ) ) -> ( A R B ) = ( A S B ) )