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

Metamath Proof Explorer

Theorem nvi

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

Ref Expression
Hypotheses nvi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvi.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
nvi.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
nvi.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
nvi.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvi ( 𝑈 ∈ NrmCVec → ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nvi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvi.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 nvi.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 nvi.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
5 nvi.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
6 eqid ⊢ ( 1st ‘ 𝑈 ) = ( 1st ‘ 𝑈 )
7 6 5 nvop2 ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ( 1st ‘ 𝑈 ) , 𝑁 ⟩ )
8 6 2 3 nvvop ⊢ ( 𝑈 ∈ NrmCVec → ( 1st ‘ 𝑈 ) = ⟨ 𝐺 , 𝑆 ⟩ )
9 8 opeq1d ⊢ ( 𝑈 ∈ NrmCVec → ⟨ ( 1st ‘ 𝑈 ) , 𝑁 ⟩ = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
10 7 9 eqtrd ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ )
11 id ⊢ ( 𝑈 ∈ NrmCVec → 𝑈 ∈ NrmCVec )
12 10 11 eqeltrrd ⊢ ( 𝑈 ∈ NrmCVec → ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec )
13 1 2 bafval ⊢ 𝑋 = ran 𝐺
14 eqid ⊢ ( GId ‘ 𝐺 ) = ( GId ‘ 𝐺 )
15 13 14 isnv ⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
16 12 15 sylib ⊢ ( 𝑈 ∈ NrmCVec → ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
17 2 4 0vfval ⊢ ( 𝑈 ∈ NrmCVec → 𝑍 = ( GId ‘ 𝐺 ) )
18 17 eqeq2d ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑥 = 𝑍 ↔ 𝑥 = ( GId ‘ 𝐺 ) ) )
19 18 imbi2d ⊢ ( 𝑈 ∈ NrmCVec → ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ↔ ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝐺 ) ) ) )
20 19 3anbi1d ⊢ ( 𝑈 ∈ NrmCVec → ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ↔ ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
21 20 ralbidv ⊢ ( 𝑈 ∈ NrmCVec → ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
22 21 3anbi3d ⊢ ( 𝑈 ∈ NrmCVec → ( ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = ( GId ‘ 𝐺 ) ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )
23 16 22 mpbird ⊢ ( 𝑈 ∈ NrmCVec → ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )