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

Metamath Proof Explorer

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 ⊢ H = SubSp ⁡ U
Assertion sspnv ⊢ U ∈ NrmCVec ∧ W ∈ H → W ∈ NrmCVec

Proof

Step Hyp Ref Expression
1 sspnv.h ⊢ H = SubSp ⁡ U
2 eqid ⊢ + v ⁡ U = + v ⁡ U
3 eqid ⊢ + v ⁡ W = + v ⁡ W
4 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
5 eqid ⊢ ⋅ 𝑠OLD ⁡ W = ⋅ 𝑠OLD ⁡ W
6 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
7 eqid ⊢ norm CV ⁡ W = norm CV ⁡ W
8 2 3 4 5 6 7 1 isssp ⊢ U ∈ NrmCVec → W ∈ H ↔ W ∈ NrmCVec ∧ + v ⁡ W ⊆ + v ⁡ U ∧ ⋅ 𝑠OLD ⁡ W ⊆ ⋅ 𝑠OLD ⁡ U ∧ norm CV ⁡ W ⊆ norm CV ⁡ U
9 8 simprbda ⊢ U ∈ NrmCVec ∧ W ∈ H → W ∈ NrmCVec