This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )