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

Metamath Proof Explorer

Theorem isnvi

Description: Properties that determine a normed complex vector space. (Contributed by NM, 15-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses isnvi.5 ⊢ 𝑋 = ran 𝐺
isnvi.6 ⊢ 𝑍 = ( GId ‘ 𝐺 )
isnvi.7 ⊢ ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD
isnvi.8 ⊢ 𝑁 : 𝑋 ⟶ ℝ
isnvi.9 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) = 0 ) → 𝑥 = 𝑍 )
isnvi.10 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) )
isnvi.11 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
isnvi.12 ⊢ 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩
Assertion isnvi 𝑈 ∈ NrmCVec

Proof

Step Hyp Ref Expression
1 isnvi.5 ⊢ 𝑋 = ran 𝐺
2 isnvi.6 ⊢ 𝑍 = ( GId ‘ 𝐺 )
3 isnvi.7 ⊢ ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD
4 isnvi.8 ⊢ 𝑁 : 𝑋 ⟶ ℝ
5 isnvi.9 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑁 ‘ 𝑥 ) = 0 ) → 𝑥 = 𝑍 )
6 isnvi.10 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) )
7 isnvi.11 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
8 isnvi.12 ⊢ 𝑈 = ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩
9 5 ex ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) )
10 6 ancoms ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) )
11 10 ralrimiva ⊢ ( 𝑥 ∈ 𝑋 → ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) )
12 7 ralrimiva ⊢ ( 𝑥 ∈ 𝑋 → ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
13 9 11 12 3jca ⊢ ( 𝑥 ∈ 𝑋 → ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
14 13 rgen ⊢ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) )
15 1 2 isnv ⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
16 3 4 14 15 mpbir3an ⊢ ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec
17 8 16 eqeltri ⊢ 𝑈 ∈ NrmCVec