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

Metamath Proof Explorer

Theorem nvvc

Description: The vector space component of a normed complex vector space. (Contributed by NM, 28-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis nvvc.1 ⊢ W = 1 st ⁡ U
Assertion nvvc ⊢ U ∈ NrmCVec → W ∈ CVec OLD

Proof

Step Hyp Ref Expression
1 nvvc.1 ⊢ W = 1 st ⁡ U
2 eqid ⊢ + v ⁡ U = + v ⁡ U
3 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
4 1 2 3 nvvop ⊢ U ∈ NrmCVec → W = + v ⁡ U ⋅ 𝑠OLD ⁡ U
5 eqid ⊢ BaseSet ⁡ U = BaseSet ⁡ U
6 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
7 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
8 5 2 3 6 7 nvi ⊢ U ∈ NrmCVec → + v ⁡ U ⋅ 𝑠OLD ⁡ U ∈ CVec OLD ∧ norm CV ⁡ U : BaseSet ⁡ U ⟶ ℝ ∧ ∀ x ∈ BaseSet ⁡ U norm CV ⁡ U ⁡ x = 0 → x = 0 vec ⁡ U ∧ ∀ y ∈ ℂ norm CV ⁡ U ⁡ y ⋅ 𝑠OLD ⁡ U x = y ⁢ norm CV ⁡ U ⁡ x ∧ ∀ y ∈ BaseSet ⁡ U norm CV ⁡ U ⁡ x + v ⁡ U y ≤ norm CV ⁡ U ⁡ x + norm CV ⁡ U ⁡ y
9 8 simp1d ⊢ U ∈ NrmCVec → + v ⁡ U ⋅ 𝑠OLD ⁡ U ∈ CVec OLD
10 4 9 eqeltrd ⊢ U ∈ NrmCVec → W ∈ CVec OLD