Theorem cphipeq0

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. Complex version of ipeq0 . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	cphipcj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	cphip0l.z	⊢ 0 = ( 0g ‘ 𝑊 )
Assertion	cphipeq0	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = 0 ↔ 𝐴 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
2		cphipcj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
3		cphip0l.z	⊢ 0 = ( 0g ‘ 𝑊 )
4		cphclm	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
5		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6	5	clm0	⊢ ( 𝑊 ∈ ℂMod → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
7	4 6	syl	⊢ ( 𝑊 ∈ ℂPreHil → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
8	7	adantr	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
9	8	eqeq2d	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = 0 ↔ ( 𝐴 , 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
10		cphphl	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
11		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
12	5 1 2 11 3	ipeq0	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝐴 = 0 ) )
13	10 12	sylan	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ 𝐴 = 0 ) )
14	9 13	bitrd	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 , 𝐴 ) = 0 ↔ 𝐴 = 0 ) )