# 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$