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 = norm CV U
sspn.m M = norm CV W
sspn.h H = SubSp U
Assertion sspn U NrmCVec W H M = N Y

Proof

Step Hyp Ref Expression
1 sspn.y Y = BaseSet W
2 sspn.n N = norm CV U
3 sspn.m M = norm CV W
4 sspn.h H = SubSp U
5 4 sspnv U NrmCVec W H W NrmCVec
6 1 3 nvf W NrmCVec M : Y
7 5 6 syl U NrmCVec W H M : Y
8 7 ffnd U NrmCVec W H M Fn Y
9 eqid BaseSet U = BaseSet U
10 9 2 nvf U NrmCVec N : BaseSet U
11 10 ffnd U NrmCVec N Fn BaseSet U
12 11 adantr U NrmCVec W H N Fn BaseSet U
13 9 1 4 sspba U NrmCVec W H Y BaseSet U
14 fnssres N Fn BaseSet U Y BaseSet U N Y Fn Y
15 12 13 14 syl2anc U NrmCVec W H N Y Fn Y
16 10 ffund U NrmCVec Fun N
17 funres Fun N Fun N Y
18 16 17 syl U NrmCVec Fun N Y
19 18 ad2antrr U NrmCVec W H x Y Fun N Y
20 fnresdm M Fn Y M Y = M
21 8 20 syl U NrmCVec W H M Y = M
22 eqid + v U = + v U
23 eqid + v W = + v W
24 eqid 𝑠OLD U = 𝑠OLD U
25 eqid 𝑠OLD W = 𝑠OLD W
26 22 23 24 25 2 3 4 isssp U NrmCVec W H W NrmCVec + v W + v U 𝑠OLD W 𝑠OLD U M N
27 26 simplbda U NrmCVec W H + v W + v U 𝑠OLD W 𝑠OLD U M N
28 27 simp3d U NrmCVec W H M N
29 ssres M N M Y N Y
30 28 29 syl U NrmCVec W H M Y N Y
31 21 30 eqsstrrd U NrmCVec W H M N Y
32 31 adantr U NrmCVec W H x Y M N Y
33 6 fdmd W NrmCVec dom M = Y
34 33 eleq2d W NrmCVec x dom M x Y
35 34 biimpar W NrmCVec x Y x dom M
36 5 35 sylan U NrmCVec W H x Y x dom M
37 funssfv Fun N Y M N Y x dom M N Y x = M x
38 19 32 36 37 syl3anc U NrmCVec W H x Y N Y x = M x
39 38 eqcomd U NrmCVec W H x Y M x = N Y x
40 8 15 39 eqfnfvd U NrmCVec W H M = N Y