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 = ( BaseSet ` W )
	sspn.n	|- N = ( normCV ` U )
	sspn.m	|- M = ( normCV ` W )
	sspn.h	|- H = ( SubSp ` U )
Assertion	sspnval	|- ( ( U e. NrmCVec /\ W e. H /\ A e. Y ) -> ( M ` A ) = ( N ` A ) )

Proof

Step	Hyp	Ref	Expression
1		sspn.y	|- Y = ( BaseSet ` W )
2		sspn.n	|- N = ( normCV ` U )
3		sspn.m	|- M = ( normCV ` W )
4		sspn.h	|- H = ( SubSp ` U )
5	1 2 3 4	sspn	|- ( ( U e. NrmCVec /\ W e. H ) -> M = ( N |` Y ) )
6	5	fveq1d	|- ( ( U e. NrmCVec /\ W e. H ) -> ( M ` A ) = ( ( N |` Y ) ` A ) )
7		fvres	|- ( A e. Y -> ( ( N |` Y ) ` A ) = ( N ` A ) )
8	6 7	sylan9eq	|- ( ( ( U e. NrmCVec /\ W e. H ) /\ A e. Y ) -> ( M ` A ) = ( N ` A ) )
9	8	3impa	|- ( ( U e. NrmCVec /\ W e. H /\ A e. Y ) -> ( M ` A ) = ( N ` A ) )