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 | |
|
sspn.n | |
||
sspn.m | |
||
sspn.h | |
||
Assertion | sspn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sspn.y | |
|
2 | sspn.n | |
|
3 | sspn.m | |
|
4 | sspn.h | |
|
5 | 4 | sspnv | |
6 | 1 3 | nvf | |
7 | 5 6 | syl | |
8 | 7 | ffnd | |
9 | eqid | |
|
10 | 9 2 | nvf | |
11 | 10 | ffnd | |
12 | 11 | adantr | |
13 | 9 1 4 | sspba | |
14 | fnssres | |
|
15 | 12 13 14 | syl2anc | |
16 | 10 | ffund | |
17 | 16 | funresd | |
18 | 17 | ad2antrr | |
19 | fnresdm | |
|
20 | 8 19 | syl | |
21 | eqid | |
|
22 | eqid | |
|
23 | eqid | |
|
24 | eqid | |
|
25 | 21 22 23 24 2 3 4 | isssp | |
26 | 25 | simplbda | |
27 | 26 | simp3d | |
28 | ssres | |
|
29 | 27 28 | syl | |
30 | 20 29 | eqsstrrd | |
31 | 30 | adantr | |
32 | 6 | fdmd | |
33 | 32 | eleq2d | |
34 | 33 | biimpar | |
35 | 5 34 | sylan | |
36 | funssfv | |
|
37 | 18 31 35 36 | syl3anc | |
38 | 37 | eqcomd | |
39 | 8 15 38 | eqfnfvd | |