Theorem sspnval

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

	Ref	Expression
Hypotheses	sspn.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
	sspn.n	$$⊢N={norm}_{CV}\left(U\right)$$
	sspn.m	$$⊢M={norm}_{CV}\left(W\right)$$
	sspn.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
Assertion	sspnval	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\wedge A\in Y\right)\to M\left(A\right)=N\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		sspn.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
2		sspn.n	$$⊢N={norm}_{CV}\left(U\right)$$
3		sspn.m	$$⊢M={norm}_{CV}\left(W\right)$$
4		sspn.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
5	1 2 3 4	sspn	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to M={N\upharpoonright }_Y$$
6	5	fveq1d	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to M\left(A\right)=\left({N\upharpoonright }_Y\right)\left(A\right)$$
7		fvres	$$⊢A\in Y\to \left({N\upharpoonright }_Y\right)\left(A\right)=N\left(A\right)$$
8	6 7	sylan9eq	$$⊢\left(\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\wedge A\in Y\right)\to M\left(A\right)=N\left(A\right)$$
9	8	3impa	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\wedge A\in Y\right)\to M\left(A\right)=N\left(A\right)$$