This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )