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 16 funresd ⊢ ( 𝑈 ∈ NrmCVec → Fun ( 𝑁 ↾ 𝑌 ) )
18 17 ad2antrr ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → Fun ( 𝑁 ↾ 𝑌 ) )
19 fnresdm ⊢ ( 𝑀 Fn 𝑌 → ( 𝑀 ↾ 𝑌 ) = 𝑀 )
20 8 19 syl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑀 ↾ 𝑌 ) = 𝑀 )
21 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
22 eqid ⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
23 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
24 eqid ⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
25 21 22 23 24 2 3 4 isssp ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ 𝑀 ⊆ 𝑁 ) ) ) )
26 25 simplbda ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ 𝑀 ⊆ 𝑁 ) )
27 26 simp3d ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 ⊆ 𝑁 )
28 ssres ⊢ ( 𝑀 ⊆ 𝑁 → ( 𝑀 ↾ 𝑌 ) ⊆ ( 𝑁 ↾ 𝑌 ) )
29 27 28 syl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑀 ↾ 𝑌 ) ⊆ ( 𝑁 ↾ 𝑌 ) )
30 20 29 eqsstrrd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 ⊆ ( 𝑁 ↾ 𝑌 ) )
31 30 adantr ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑀 ⊆ ( 𝑁 ↾ 𝑌 ) )
32 6 fdmd ⊢ ( 𝑊 ∈ NrmCVec → dom 𝑀 = 𝑌 )
33 32 eleq2d ⊢ ( 𝑊 ∈ NrmCVec → ( 𝑥 ∈ dom 𝑀 ↔ 𝑥 ∈ 𝑌 ) )
34 33 biimpar ⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ dom 𝑀 )
35 5 34 sylan ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ dom 𝑀 )
36 funssfv ⊢ ( ( Fun ( 𝑁 ↾ 𝑌 ) ∧ 𝑀 ⊆ ( 𝑁 ↾ 𝑌 ) ∧ 𝑥 ∈ dom 𝑀 ) → ( ( 𝑁 ↾ 𝑌 ) ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
37 18 31 35 36 syl3anc ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑁 ↾ 𝑌 ) ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
38 37 eqcomd ⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑀 ‘ 𝑥 ) = ( ( 𝑁 ↾ 𝑌 ) ‘ 𝑥 ) )
39 8 15 38 eqfnfvd ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑁 ↾ 𝑌 ) )