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 funres 
 |-  ( Fun N -> Fun ( N |` Y ) )
18 16 17 syl 
 |-  ( U e. NrmCVec -> Fun ( N |` Y ) )
19 18 ad2antrr 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> Fun ( N |` Y ) )
20 fnresdm 
 |-  ( M Fn Y -> ( M |` Y ) = M )
21 8 20 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( M |` Y ) = M )
22 eqid 
 |-  ( +v ` U ) = ( +v ` U )
23 eqid 
 |-  ( +v ` W ) = ( +v ` W )
24 eqid 
 |-  ( .sOLD ` U ) = ( .sOLD ` U )
25 eqid 
 |-  ( .sOLD ` W ) = ( .sOLD ` W )
26 22 23 24 25 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 ) ) ) )
27 26 simplbda 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( ( +v ` W ) C_ ( +v ` U ) /\ ( .sOLD ` W ) C_ ( .sOLD ` U ) /\ M C_ N ) )
28 27 simp3d 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> M C_ N )
29 ssres 
 |-  ( M C_ N -> ( M |` Y ) C_ ( N |` Y ) )
30 28 29 syl 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( M |` Y ) C_ ( N |` Y ) )
31 21 30 eqsstrrd 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> M C_ ( N |` Y ) )
32 31 adantr 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> M C_ ( N |` Y ) )
33 6 fdmd 
 |-  ( W e. NrmCVec -> dom M = Y )
34 33 eleq2d 
 |-  ( W e. NrmCVec -> ( x e. dom M <-> x e. Y ) )
35 34 biimpar 
 |-  ( ( W e. NrmCVec /\ x e. Y ) -> x e. dom M )
36 5 35 sylan 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> x e. dom M )
37 funssfv 
 |-  ( ( Fun ( N |` Y ) /\ M C_ ( N |` Y ) /\ x e. dom M ) -> ( ( N |` Y ) ` x ) = ( M ` x ) )
38 19 32 36 37 syl3anc 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> ( ( N |` Y ) ` x ) = ( M ` x ) )
39 38 eqcomd 
 |-  ( ( ( U e. NrmCVec /\ W e. H ) /\ x e. Y ) -> ( M ` x ) = ( ( N |` Y ) ` x ) )
40 8 15 39 eqfnfvd 
 |-  ( ( U e. NrmCVec /\ W e. H ) -> M = ( N |` Y ) )