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 𝑌 = ( BaseSet ‘ 𝑊 )
ssps.s 𝑆 = ( ·𝑠OLD𝑈 )
ssps.r 𝑅 = ( ·𝑠OLD𝑊 )
ssps.h 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspsval ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵𝑌 ) ) → ( 𝐴 𝑅 𝐵 ) = ( 𝐴 𝑆 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ssps.y 𝑌 = ( BaseSet ‘ 𝑊 )
2 ssps.s 𝑆 = ( ·𝑠OLD𝑈 )
3 ssps.r 𝑅 = ( ·𝑠OLD𝑊 )
4 ssps.h 𝐻 = ( SubSp ‘ 𝑈 )
5 1 2 3 4 ssps ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → 𝑅 = ( 𝑆 ↾ ( ℂ × 𝑌 ) ) )
6 5 oveqd ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) → ( 𝐴 𝑅 𝐵 ) = ( 𝐴 ( 𝑆 ↾ ( ℂ × 𝑌 ) ) 𝐵 ) )
7 ovres ( ( 𝐴 ∈ ℂ ∧ 𝐵𝑌 ) → ( 𝐴 ( 𝑆 ↾ ( ℂ × 𝑌 ) ) 𝐵 ) = ( 𝐴 𝑆 𝐵 ) )
8 6 7 sylan9eq ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊𝐻 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵𝑌 ) ) → ( 𝐴 𝑅 𝐵 ) = ( 𝐴 𝑆 𝐵 ) )