Metamath Proof Explorer

Theorem sspn

Description: The norm on a subspace is a restriction 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 sspn 
|- ( ( U e. NrmCVec /\ W e. H ) -> M = ( N |` Y ) )

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 4 sspnv 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )
6 1 3 nvf 
 |-  ( W e. NrmCVec -> M : Y --> RR )
7 5 6 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> M : Y --> RR )
8 7 ffnd 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> M Fn Y )
9 eqid 
 |-  ( BaseSet ` U ) = ( BaseSet ` U )
10 9 2 nvf 
 |-  ( U e. NrmCVec -> N : ( BaseSet ` U ) --> RR )
11 10 ffnd 
 |-  ( U e. NrmCVec -> N Fn ( BaseSet ` U ) )
12 11 adantr 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> N Fn ( BaseSet ` U ) )
13 9 1 4 sspba 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> Y C_ ( BaseSet ` U ) )
14 fnssres 
 |-  ( ( N Fn ( BaseSet ` U ) /\ Y C_ ( BaseSet ` U ) ) -> ( N |` Y ) Fn Y )
15 12 13 14 syl2anc 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( N |` Y ) Fn Y )
16 10 ffund 
 |-  ( U e. NrmCVec -> Fun N )
17 16 funresd 
 |-  ( U e. NrmCVec -> Fun ( N |` Y ) )
18 17 ad2antrr 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> Fun ( N |` Y ) )
19 fnresdm 
 |-  ( M Fn Y -> ( M |` Y ) = M )
20 8 19 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( M |` Y ) = M )
21 eqid 
 |-  ( +v ` U ) = ( +v ` U )
22 eqid 
 |-  ( +v ` W ) = ( +v ` W )
23 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
24 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
25 21 22 23 24 2 3 4 isssp 
 |-  ( U e. NrmCVec -> ( W e. H <-> ( W e. NrmCVec /\ ( ( +v ` W ) C_ ( +v ` U ) /\ ( .sOLD ` W ) C_ ( .sOLD ` U ) /\ M C_ N ) ) ) )
26 25 simplbda 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( ( +v ` W ) C_ ( +v ` U ) /\ ( .sOLD ` W ) C_ ( .sOLD ` U ) /\ M C_ N ) )
27 26 simp3d 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> M C_ N )
28 ssres 
 |-  ( M C_ N -> ( M |` Y ) C_ ( N |` Y ) )
29 27 28 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( M |` Y ) C_ ( N |` Y ) )
30 20 29 eqsstrrd 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> M C_ ( N |` Y ) )
31 30 adantr 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> M C_ ( N |` Y ) )
32 6 fdmd 
 |-  ( W e. NrmCVec -> dom M = Y )
33 32 eleq2d 
 |-  ( W e. NrmCVec -> ( x e. dom M <-> x e. Y ) )
34 33 biimpar 
 |-  ( ( W e. NrmCVec /\ x e. Y ) -> x e. dom M )
35 5 34 sylan 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> x e. dom M )
36 funssfv 
 |-  ( ( Fun ( N |` Y ) /\ M C_ ( N |` Y ) /\ x e. dom M ) -> ( ( N |` Y ) ` x ) = ( M ` x ) )
37 18 31 35 36 syl3anc 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> ( ( N |` Y ) ` x ) = ( M ` x ) )
38 37 eqcomd 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> ( M ` x ) = ( ( N |` Y ) ` x ) )
39 8 15 38 eqfnfvd 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> M = ( N |` Y ) )