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