Theorem sspnv

Description: A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sspnv.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion	sspnv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )

Proof

Step	Hyp	Ref	Expression
1		sspnv.h	⊢ 𝐻 = ( SubSp ‘ 𝑈 )
2		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
3		eqid	⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
4		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
5		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
6		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
7		eqid	⊢ ( normCV ‘ 𝑊 ) = ( normCV ‘ 𝑊 )
8	2 3 4 5 6 7 1	isssp	⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( ( +𝑣 ‘ 𝑊 ) ⊆ ( +𝑣 ‘ 𝑈 ) ∧ ( ·𝑠OLD ‘ 𝑊 ) ⊆ ( ·𝑠OLD ‘ 𝑈 ) ∧ ( normCV ‘ 𝑊 ) ⊆ ( normCV ‘ 𝑈 ) ) ) ) )
9	8	simprbda	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ∈ NrmCVec )