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=\mathrm{BaseSet}\left(W\right)$$
	ssps.s	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	ssps.r	$$⊢R={\cdot }_{\mathrm{𝑠OLD}}\left(W\right)$$
	ssps.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
Assertion	sspsval	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\wedge \left(A\in ℂ\wedge B\in Y\right)\right)\to ARB=ASB$$

Proof

Step	Hyp	Ref	Expression
1		ssps.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
2		ssps.s	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
3		ssps.r	$$⊢R={\cdot }_{\mathrm{𝑠OLD}}\left(W\right)$$
4		ssps.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
5	1 2 3 4	ssps	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to R={S\upharpoonright }_{\left(ℂ\times Y\right)}$$
6	5	oveqd	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to ARB=A\left({S\upharpoonright }_{\left(ℂ\times Y\right)}\right)B$$
7		ovres	$$⊢\left(A\in ℂ\wedge B\in Y\right)\to A\left({S\upharpoonright }_{\left(ℂ\times Y\right)}\right)B=ASB$$
8	6 7	sylan9eq	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\wedge \left(A\in ℂ\wedge B\in Y\right)\right)\to ARB=ASB$$