Metamath Proof Explorer

Theorem ipz

Description: The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of Kreyszig p. 129. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses dip0r.1 ⊢ X = BaseSet ⁡ U
dip0r.5 ⊢ Z = 0 vec ⁡ U
dip0r.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
Assertion ipz ⊢ U ∈ NrmCVec ∧ A ∈ X → A P A = 0 ↔ A = Z

Proof

Step Hyp Ref Expression
1 dip0r.1 ⊢ X = BaseSet ⁡ U
2 dip0r.5 ⊢ Z = 0 vec ⁡ U
3 dip0r.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
4 eqid ⊢ norm CV ⁡ U = norm CV ⁡ U
5 1 4 3 ipidsq ⊢ U ∈ NrmCVec ∧ A ∈ X → A P A = norm CV ⁡ U ⁡ A 2
6 5 eqeq1d ⊢ U ∈ NrmCVec ∧ A ∈ X → A P A = 0 ↔ norm CV ⁡ U ⁡ A 2 = 0
7 1 4 nvcl ⊢ U ∈ NrmCVec ∧ A ∈ X → norm CV ⁡ U ⁡ A ∈ ℝ
8 7 recnd ⊢ U ∈ NrmCVec ∧ A ∈ X → norm CV ⁡ U ⁡ A ∈ ℂ
9 sqeq0 ⊢ norm CV ⁡ U ⁡ A ∈ ℂ → norm CV ⁡ U ⁡ A 2 = 0 ↔ norm CV ⁡ U ⁡ A = 0
10 8 9 syl ⊢ U ∈ NrmCVec ∧ A ∈ X → norm CV ⁡ U ⁡ A 2 = 0 ↔ norm CV ⁡ U ⁡ A = 0
11 1 2 4 nvz ⊢ U ∈ NrmCVec ∧ A ∈ X → norm CV ⁡ U ⁡ A = 0 ↔ A = Z
12 6 10 11 3bitrd ⊢ U ∈ NrmCVec ∧ A ∈ X → A P A = 0 ↔ A = Z