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 ⊢ X = BaseSet ⁡ U
nvz.5 ⊢ Z = 0 vec ⁡ U
nvz.6 ⊢ N = norm CV ⁡ U
Assertion nvz ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A = 0 ↔ A = Z

Proof

Step Hyp Ref Expression
1 nvz.1 ⊢ X = BaseSet ⁡ U
2 nvz.5 ⊢ Z = 0 vec ⁡ U
3 nvz.6 ⊢ N = norm CV ⁡ U
4 eqid ⊢ + v ⁡ U = + v ⁡ U
5 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
6 1 4 5 2 3 nvi ⊢ U ∈ NrmCVec → + v ⁡ U ⋅ 𝑠OLD ⁡ U ∈ CVec OLD ∧ N : X ⟶ ℝ ∧ ∀ x ∈ X N ⁡ x = 0 → x = Z ∧ ∀ y ∈ ℂ N ⁡ y ⋅ 𝑠OLD ⁡ U x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x + v ⁡ U y ≤ N ⁡ x + N ⁡ y
7 6 simp3d ⊢ U ∈ NrmCVec → ∀ x ∈ X N ⁡ x = 0 → x = Z ∧ ∀ y ∈ ℂ N ⁡ y ⋅ 𝑠OLD ⁡ U x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x + v ⁡ U y ≤ N ⁡ x + N ⁡ y
8 simp1 ⊢ N ⁡ x = 0 → x = Z ∧ ∀ y ∈ ℂ N ⁡ y ⋅ 𝑠OLD ⁡ U x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x + v ⁡ U y ≤ N ⁡ x + N ⁡ y → N ⁡ x = 0 → x = Z
9 8 ralimi ⊢ ∀ x ∈ X N ⁡ x = 0 → x = Z ∧ ∀ y ∈ ℂ N ⁡ y ⋅ 𝑠OLD ⁡ U x = y ⁢ N ⁡ x ∧ ∀ y ∈ X N ⁡ x + v ⁡ U y ≤ N ⁡ x + N ⁡ y → ∀ x ∈ X N ⁡ x = 0 → x = Z
10 fveqeq2 ⊢ x = A → N ⁡ x = 0 ↔ N ⁡ A = 0
11 eqeq1 ⊢ x = A → x = Z ↔ A = Z
12 10 11 imbi12d ⊢ x = A → N ⁡ x = 0 → x = Z ↔ N ⁡ A = 0 → A = Z
13 12 rspccv ⊢ ∀ x ∈ X N ⁡ x = 0 → x = Z → A ∈ X → N ⁡ A = 0 → A = Z
14 7 9 13 3syl ⊢ U ∈ NrmCVec → A ∈ X → N ⁡ A = 0 → A = Z
15 14 imp ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A = 0 → A = Z
16 fveq2 ⊢ A = Z → N ⁡ A = N ⁡ Z
17 2 3 nvz0 ⊢ U ∈ NrmCVec → N ⁡ Z = 0
18 16 17 sylan9eqr ⊢ U ∈ NrmCVec ∧ A = Z → N ⁡ A = 0
19 18 ex ⊢ U ∈ NrmCVec → A = Z → N ⁡ A = 0
20 19 adantr ⊢ U ∈ NrmCVec ∧ A ∈ X → A = Z → N ⁡ A = 0
21 15 20 impbid ⊢ U ∈ NrmCVec ∧ A ∈ X → N ⁡ A = 0 ↔ A = Z