Metamath Proof Explorer

Theorem ipeq0

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) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
ip0l.z ⊢ 𝑍 = ( 0g ‘ 𝐹 )
ip0l.o ⊢ 0 = ( 0g ‘ 𝑊 )
Assertion ipeq0 ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = 𝑍 ↔ 𝐴 = 0 ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 phllmhm.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 phllmhm.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 ip0l.z ⊢ 𝑍 = ( 0g ‘ 𝐹 )
5 ip0l.o ⊢ 0 = ( 0g ‘ 𝑊 )
6 eqid ⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 )
7 3 1 2 5 6 4 isphl ⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) )
8 7 simp3bi ⊢ ( 𝑊 ∈ PreHil → ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) )
9 simp2 ⊢ ( ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) → ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) )
10 9 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) → ∀ 𝑥 ∈ 𝑉 ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) )
11 8 10 syl ⊢ ( 𝑊 ∈ PreHil → ∀ 𝑥 ∈ 𝑉 ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) )
12 oveq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑥 = 𝐴 ) → ( 𝑥 , 𝑥 ) = ( 𝐴 , 𝐴 ) )
13 12 anidms ⊢ ( 𝑥 = 𝐴 → ( 𝑥 , 𝑥 ) = ( 𝐴 , 𝐴 ) )
14 13 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 , 𝑥 ) = 𝑍 ↔ ( 𝐴 , 𝐴 ) = 𝑍 ) )
15 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 0 ↔ 𝐴 = 0 ) )
16 14 15 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ↔ ( ( 𝐴 , 𝐴 ) = 𝑍 → 𝐴 = 0 ) ) )
17 16 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑉 ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = 𝑍 → 𝐴 = 0 ) )
18 11 17 sylan ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = 𝑍 → 𝐴 = 0 ) )
19 1 2 3 4 5 ip0l ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( 0 , 𝐴 ) = 𝑍 )
20 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 , 𝐴 ) = ( 0 , 𝐴 ) )
21 20 eqeq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 , 𝐴 ) = 𝑍 ↔ ( 0 , 𝐴 ) = 𝑍 ) )
22 19 21 syl5ibrcom ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( 𝐴 = 0 → ( 𝐴 , 𝐴 ) = 𝑍 ) )
23 18 22 impbid ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = 𝑍 ↔ 𝐴 = 0 ) )