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=BaseSetW
sspn.n N=normCVU
sspn.m M=normCVW
sspn.h H=SubSpU
Assertion sspn UNrmCVecWHM=NY

Proof

Step Hyp Ref Expression
1 sspn.y Y=BaseSetW
2 sspn.n N=normCVU
3 sspn.m M=normCVW
4 sspn.h H=SubSpU
5 4 sspnv UNrmCVecWHWNrmCVec
6 1 3 nvf WNrmCVecM:Y
7 5 6 syl UNrmCVecWHM:Y
8 7 ffnd UNrmCVecWHMFnY
9 eqid BaseSetU=BaseSetU
10 9 2 nvf UNrmCVecN:BaseSetU
11 10 ffnd UNrmCVecNFnBaseSetU
12 11 adantr UNrmCVecWHNFnBaseSetU
13 9 1 4 sspba UNrmCVecWHYBaseSetU
14 fnssres NFnBaseSetUYBaseSetUNYFnY
15 12 13 14 syl2anc UNrmCVecWHNYFnY
16 10 ffund UNrmCVecFunN
17 16 funresd UNrmCVecFunNY
18 17 ad2antrr UNrmCVecWHxYFunNY
19 fnresdm MFnYMY=M
20 8 19 syl UNrmCVecWHMY=M
21 eqid +vU=+vU
22 eqid +vW=+vW
23 eqid 𝑠OLDU=𝑠OLDU
24 eqid 𝑠OLDW=𝑠OLDW
25 21 22 23 24 2 3 4 isssp UNrmCVecWHWNrmCVec+vW+vU𝑠OLDW𝑠OLDUMN
26 25 simplbda UNrmCVecWH+vW+vU𝑠OLDW𝑠OLDUMN
27 26 simp3d UNrmCVecWHMN
28 ssres MNMYNY
29 27 28 syl UNrmCVecWHMYNY
30 20 29 eqsstrrd UNrmCVecWHMNY
31 30 adantr UNrmCVecWHxYMNY
32 6 fdmd WNrmCVecdomM=Y
33 32 eleq2d WNrmCVecxdomMxY
34 33 biimpar WNrmCVecxYxdomM
35 5 34 sylan UNrmCVecWHxYxdomM
36 funssfv FunNYMNYxdomMNYx=Mx
37 18 31 35 36 syl3anc UNrmCVecWHxYNYx=Mx
38 37 eqcomd UNrmCVecWHxYMx=NYx
39 8 15 38 eqfnfvd UNrmCVecWHM=NY