Theorem lssnvc

Description: A subspace of a normed vector space is a normed vector space. (Contributed by Mario Carneiro, 4-Oct-2015)

	Ref	Expression
Hypotheses	lssnlm.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
	lssnlm.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lssnvc	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmVec )

Proof

Step	Hyp	Ref	Expression
1		lssnlm.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2		lssnlm.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		nvcnlm	⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ NrmMod )
4	1 2	lssnlm	⊢ ( ( 𝑊 ∈ NrmMod ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmMod )
5	3 4	sylan	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmMod )
6		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
7	1 6	resssca	⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
8	7	adantl	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
9		nvclvec	⊢ ( 𝑊 ∈ NrmVec → 𝑊 ∈ LVec )
10	6	lvecdrng	⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
11	9 10	syl	⊢ ( 𝑊 ∈ NrmVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
12	11	adantr	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) ∈ DivRing )
13	8 12	eqeltrrd	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑋 ) ∈ DivRing )
14		eqid	⊢ ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑋 )
15	14	isnvc2	⊢ ( 𝑋 ∈ NrmVec ↔ ( 𝑋 ∈ NrmMod ∧ ( Scalar ‘ 𝑋 ) ∈ DivRing ) )
16	5 13 15	sylanbrc	⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmVec )