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 ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
sspn.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
sspn.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
sspn.h ⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspn ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑁 ↾ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 sspn.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
2 sspn.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
3 sspn.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
4 sspn.h ⊢ 𝐻 = ( SubSp ‘ 𝑈 )
5 4 sspnv ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )
6 1 3 nvf ⊢ ( 𝑊 ∈ NrmCVec → 𝑀 : 𝑌 ⟶ ℝ )
7 5 6 syl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 : 𝑌 ⟶ ℝ )
8 7 ffnd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 Fn 𝑌 )
9 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
10 9 2 nvf ⊢ ( 𝑈 ∈ NrmCVec → 𝑁 : ( BaseSet ‘ 𝑈 ) ⟶ ℝ )
11 10 ffnd ⊢ ( 𝑈 ∈ NrmCVec → 𝑁 Fn ( BaseSet ‘ 𝑈 ) )
12 11 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑁 Fn ( BaseSet ‘ 𝑈 ) )
13 9 1 4 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) )
14 fnssres ⊢ ( ( 𝑁 Fn ( BaseSet ‘ 𝑈 ) ∧ 𝑌 ⊆ ( BaseSet ‘ 𝑈 ) ) → ( 𝑁 ↾ 𝑌 ) Fn 𝑌 )
15 12 13 14 syl2anc ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑁 ↾ 𝑌 ) Fn 𝑌 )
16 10 ffund ⊢ ( 𝑈 ∈ NrmCVec → Fun 𝑁 )
17 funres ⊢ ( Fun 𝑁 → Fun ( 𝑁 ↾ 𝑌 ) )
18 16 17 syl ⊢ ( 𝑈 ∈ NrmCVec → Fun ( 𝑁 ↾ 𝑌 ) )
19 18 ad2antrr ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → Fun ( 𝑁 ↾ 𝑌 ) )
20 fnresdm ⊢ ( 𝑀 Fn 𝑌 → ( 𝑀 ↾ 𝑌 ) = 𝑀 )
21 8 20 syl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑀 ↾ 𝑌 ) = 𝑀 )
22 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
23 eqid ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
24 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
25 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
26 22 23 24 25 2 3 4 isssp ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ 𝑀 ⊆ 𝑁 ) ) ) )
27 26 simplbda ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ 𝑀 ⊆ 𝑁 ) )
28 27 simp3d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 ⊆ 𝑁 )
29 ssres ⊢ ( 𝑀 ⊆ 𝑁 → ( 𝑀 ↾ 𝑌 ) ⊆ ( 𝑁 ↾ 𝑌 ) )
30 28 29 syl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑀 ↾ 𝑌 ) ⊆ ( 𝑁 ↾ 𝑌 ) )
31 21 30 eqsstrrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 ⊆ ( 𝑁 ↾ 𝑌 ) )
32 31 adantr ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑀 ⊆ ( 𝑁 ↾ 𝑌 ) )
33 6 fdmd ⊢ ( 𝑊 ∈ NrmCVec → dom 𝑀 = 𝑌 )
34 33 eleq2d ⊢ ( 𝑊 ∈ NrmCVec → ( 𝑥 ∈ dom 𝑀 ↔ 𝑥 ∈ 𝑌 ) )
35 34 biimpar ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ dom 𝑀 )
36 5 35 sylan ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ dom 𝑀 )
37 funssfv ⊢ ( ( Fun ( 𝑁 ↾ 𝑌 ) ∧ 𝑀 ⊆ ( 𝑁 ↾ 𝑌 ) ∧ 𝑥 ∈ dom 𝑀 ) → ( ( 𝑁 ↾ 𝑌 ) ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
38 19 32 36 37 syl3anc ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ↾ 𝑌 ) ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
39 38 eqcomd ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑀 ‘ 𝑥 ) = ( ( 𝑁 ↾ 𝑌 ) ‘ 𝑥 ) )
40 8 15 39 eqfnfvd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑁 ↾ 𝑌 ) )