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 ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 𝐺 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )