Theorem sspnval

Description: The norm on a subspace in terms 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	sspnval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ 𝐴 ∈ 𝑌 ) → ( 𝑀 ‘ 𝐴 ) = ( 𝑁 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sspn.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
2		sspn.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
3		sspn.m	⊢ 𝑀 = ( normCV ‘ 𝑊 )
4		sspn.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
5	1 2 3 4	sspn	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑁 ↾ 𝑌 ) )
6	5	fveq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → ( 𝑀 ‘ 𝐴 ) = ( ( 𝑁 ↾ 𝑌 ) ‘ 𝐴 ) )
7		fvres	⊢ ( 𝐴 ∈ 𝑌 → ( ( 𝑁 ↾ 𝑌 ) ‘ 𝐴 ) = ( 𝑁 ‘ 𝐴 ) )
8	6 7	sylan9eq	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐴 ∈ 𝑌 ) → ( 𝑀 ‘ 𝐴 ) = ( 𝑁 ‘ 𝐴 ) )
9	8	3impa	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ∧ 𝐴 ∈ 𝑌 ) → ( 𝑀 ‘ 𝐴 ) = ( 𝑁 ‘ 𝐴 ) )