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 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 𝑅 𝐵 ) = ( 𝐴 𝑆 𝐵 ) )