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	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
	cphip0l.z	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	cphipeq0	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=0\leftrightarrow A=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		cphipcj.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
2		cphipcj.v	$$⊢V={\mathrm{Base}}_W$$
3		cphip0l.z	$$⊢\underset{\dot{}}{0}=0_W$$
4		cphclm	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{CMod}$$
5		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
6	5	clm0	$$⊢W\in \mathrm{CMod}\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
7	4 6	syl	$$⊢W\in \mathrm{CPreHil}\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
8	7	adantr	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to 0=0_{\mathrm{Scalar}\left(W\right)}$$
9	8	eqeq2d	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=0\leftrightarrow A\underset{\dot{}}{,}A=0_{\mathrm{Scalar}\left(W\right)}\right)$$
10		cphphl	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{PreHil}$$
11		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
12	5 1 2 11 3	ipeq0	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow A=\underset{\dot{}}{0}\right)$$
13	10 12	sylan	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow A=\underset{\dot{}}{0}\right)$$
14	9 13	bitrd	$$⊢\left(W\in \mathrm{CPreHil}\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=0\leftrightarrow A=\underset{\dot{}}{0}\right)$$