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

Metamath Proof Explorer

Theorem isnv

Description: The predicate "is a normed complex vector space." (Contributed by NM, 5-Jun-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isnv.1 ⊢ 𝑋 = ran 𝐺
isnv.2 ⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion isnv ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isnv.1 ⊢ 𝑋 = ran 𝐺
2 isnv.2 ⊢ 𝑍 = ( GId ‘ 𝐺 )
3 nvex ⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) )
4 vcex ⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
5 4 adantr ⊢ ( ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
6 4 simpld ⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD → 𝐺 ∈ V )
7 rnexg ⊢ ( 𝐺 ∈ V → ran 𝐺 ∈ V )
8 6 7 syl ⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD → ran 𝐺 ∈ V )
9 1 8 eqeltrid ⊢ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD → 𝑋 ∈ V )
10 fex ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ 𝑋 ∈ V ) → 𝑁 ∈ V )
11 9 10 sylan2 ⊢ ( ( 𝑁 : 𝑋 ⟶ ℝ ∧ ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ) → 𝑁 ∈ V )
12 11 ancoms ⊢ ( ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ) → 𝑁 ∈ V )
13 df-3an ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) ↔ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) ∧ 𝑁 ∈ V ) )
14 5 12 13 sylanbrc ⊢ ( ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) )
15 14 3adant3 ⊢ ( ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) )
16 1 2 isnvlem ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ∧ 𝑁 ∈ V ) → ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) ) )
17 3 15 16 pm5.21nii ⊢ ( ⟨ ⟨ 𝐺 , 𝑆 ⟩ , 𝑁 ⟩ ∈ NrmCVec ↔ ( ⟨ 𝐺 , 𝑆 ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 𝑆 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )