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 ⊢ 𝑊 = ( 1st ‘ 𝑈 )
Assertion nvvc ( 𝑈 ∈ NrmCVec → 𝑊 ∈ CVecOLD )

Proof

Step Hyp Ref Expression
1 nvvc.1 ⊢ 𝑊 = ( 1st ‘ 𝑈 )
2 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
3 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
4 1 2 3 nvvop ⊢ ( 𝑈 ∈ NrmCVec → 𝑊 = ⟨ ( +𝑣 ‘ 𝑈 ) , ( ·𝑠OLD ‘ 𝑈 ) ⟩ )
5 eqid ⊢ ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
6 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
7 eqid ⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
8 5 2 3 6 7 nvi ⊢ ( 𝑈 ∈ NrmCVec → ( ⟨ ( +𝑣 ‘ 𝑈 ) , ( ·𝑠OLD ‘ 𝑈 ) ⟩ ∈ CVecOLD ∧ ( normCV ‘ 𝑈 ) : ( BaseSet ‘ 𝑈 ) ⟶ ℝ ∧ ∀ 𝑥 ∈ ( BaseSet ‘ 𝑈 ) ( ( ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) = 0 → 𝑥 = ( 0vec ‘ 𝑈 ) ) ∧ ∀ 𝑦 ∈ ℂ ( ( normCV ‘ 𝑈 ) ‘ ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( BaseSet ‘ 𝑈 ) ( ( normCV ‘ 𝑈 ) ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( ( normCV ‘ 𝑈 ) ‘ 𝑥 ) + ( ( normCV ‘ 𝑈 ) ‘ 𝑦 ) ) ) ) )
9 8 simp1d ⊢ ( 𝑈 ∈ NrmCVec → ⟨ ( +𝑣 ‘ 𝑈 ) , ( ·𝑠OLD ‘ 𝑈 ) ⟩ ∈ CVecOLD )
10 4 9 eqeltrd ⊢ ( 𝑈 ∈ NrmCVec → 𝑊 ∈ CVecOLD )