Theorem sspgval

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

	Ref	Expression
Hypotheses	sspg.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
	sspg.g	$$⊢G={+}_v\left(U\right)$$
	sspg.f	$$⊢F={+}_v\left(W\right)$$
	sspg.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
Assertion	sspgval	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\wedge \left(A\in Y\wedge B\in Y\right)\right)\to AFB=AGB$$

Proof

Step	Hyp	Ref	Expression
1		sspg.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
2		sspg.g	$$⊢G={+}_v\left(U\right)$$
3		sspg.f	$$⊢F={+}_v\left(W\right)$$
4		sspg.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
5	1 2 3 4	sspg	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to F={G\upharpoonright }_{\left(Y\times Y\right)}$$
6	5	oveqd	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to AFB=A\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)B$$
7		ovres	$$⊢\left(A\in Y\wedge B\in Y\right)\to A\left({G\upharpoonright }_{\left(Y\times Y\right)}\right)B=AGB$$
8	6 7	sylan9eq	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\wedge \left(A\in Y\wedge B\in Y\right)\right)\to AFB=AGB$$