Metamath Proof Explorer

Theorem nvz

Description: The norm of a vector is zero iff the vector is zero. First part of Problem 2 of Kreyszig p. 64. (Contributed by NM, 24-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvz.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvz.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
nvz.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
Assertion nvz ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 0 ↔ 𝐴 = 𝑍 ) )

Proof

Step Hyp Ref Expression
1 nvz.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvz.5 ⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3 nvz.6 ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 eqid ⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
5 eqid ⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
6 1 4 5 2 3 nvi ⊢ ( 𝑈 ∈ NrmCVec → ( ⟨ ( +𝑣 ‘ 𝑈 ) , ( ·𝑠OLD ‘ 𝑈 ) ⟩ ∈ CVecOLD ∧ 𝑁 : 𝑋 ⟶ ℝ ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) ) )
7 6 simp3d ⊢ ( 𝑈 ∈ NrmCVec → ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) )
8 simp1 ⊢ ( ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) )
9 8 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ∧ ∀ 𝑦 ∈ ℂ ( 𝑁 ‘ ( 𝑦 ( ·𝑠OLD ‘ 𝑈 ) 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( 𝑁 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑥 ( +𝑣 ‘ 𝑈 ) 𝑦 ) ) ≤ ( ( 𝑁 ‘ 𝑥 ) + ( 𝑁 ‘ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) )
10 fveqeq2 ⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ 𝑥 ) = 0 ↔ ( 𝑁 ‘ 𝐴 ) = 0 ) )
11 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝑍 ↔ 𝐴 = 𝑍 ) )
12 10 11 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) ↔ ( ( 𝑁 ‘ 𝐴 ) = 0 → 𝐴 = 𝑍 ) ) )
13 12 rspccv ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑁 ‘ 𝑥 ) = 0 → 𝑥 = 𝑍 ) → ( 𝐴 ∈ 𝑋 → ( ( 𝑁 ‘ 𝐴 ) = 0 → 𝐴 = 𝑍 ) ) )
14 7 9 13 3syl ⊢ ( 𝑈 ∈ NrmCVec → ( 𝐴 ∈ 𝑋 → ( ( 𝑁 ‘ 𝐴 ) = 0 → 𝐴 = 𝑍 ) ) )
15 14 imp ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 0 → 𝐴 = 𝑍 ) )
16 fveq2 ⊢ ( 𝐴 = 𝑍 → ( 𝑁 ‘ 𝐴 ) = ( 𝑁 ‘ 𝑍 ) )
17 2 3 nvz0 ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑁 ‘ 𝑍 ) = 0 )
18 16 17 sylan9eqr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 = 𝑍 ) → ( 𝑁 ‘ 𝐴 ) = 0 )
19 18 ex ⊢ ( 𝑈 ∈ NrmCVec → ( 𝐴 = 𝑍 → ( 𝑁 ‘ 𝐴 ) = 0 ) )
20 19 adantr ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 = 𝑍 → ( 𝑁 ‘ 𝐴 ) = 0 ) )
21 15 20 impbid ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) = 0 ↔ 𝐴 = 𝑍 ) )