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	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
	ip0l.z	$$⊢Z=0_F$$
	ip0l.o	$$⊢\underset{\dot{}}{0}=0_W$$
Assertion	ipeq0	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=Z\leftrightarrow A=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
4		ip0l.z	$$⊢Z=0_F$$
5		ip0l.o	$$⊢\underset{\dot{}}{0}=0_W$$
6		eqid	$$⊢{\mathrm{*}}_F={\mathrm{*}}_F$$
7	3 1 2 5 6 4	isphl	$$⊢W\in \mathrm{PreHil}\leftrightarrow \left(W\in \mathrm{LVec}\wedge F\in \mathrm{*-Ring}\wedge \forall x\in V\left(\left(y\in V⟼y\underset{\dot{}}{,}x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)\wedge \forall y\in V{\left(x\underset{\dot{}}{,}y\right)}^{{\mathrm{*}}_F}=y\underset{\dot{}}{,}x\right)\right)$$
8	7	simp3bi	$$⊢W\in \mathrm{PreHil}\to \forall x\in V\left(\left(y\in V⟼y\underset{\dot{}}{,}x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)\wedge \forall y\in V{\left(x\underset{\dot{}}{,}y\right)}^{{\mathrm{*}}_F}=y\underset{\dot{}}{,}x\right)$$
9		simp2	$$⊢\left(\left(y\in V⟼y\underset{\dot{}}{,}x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)\wedge \forall y\in V{\left(x\underset{\dot{}}{,}y\right)}^{{\mathrm{*}}_F}=y\underset{\dot{}}{,}x\right)\to \left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)$$
10	9	ralimi	$$⊢\forall x\in V\left(\left(y\in V⟼y\underset{\dot{}}{,}x\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\wedge \left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)\wedge \forall y\in V{\left(x\underset{\dot{}}{,}y\right)}^{{\mathrm{*}}_F}=y\underset{\dot{}}{,}x\right)\to \forall x\in V\left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)$$
11	8 10	syl	$$⊢W\in \mathrm{PreHil}\to \forall x\in V\left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)$$
12		oveq12	$$⊢\left(x=A\wedge x=A\right)\to x\underset{\dot{}}{,}x=A\underset{\dot{}}{,}A$$
13	12	anidms	$$⊢x=A\to x\underset{\dot{}}{,}x=A\underset{\dot{}}{,}A$$
14	13	eqeq1d	$$⊢x=A\to \left(x\underset{\dot{}}{,}x=Z\leftrightarrow A\underset{\dot{}}{,}A=Z\right)$$
15		eqeq1	$$⊢x=A\to \left(x=\underset{\dot{}}{0}\leftrightarrow A=\underset{\dot{}}{0}\right)$$
16	14 15	imbi12d	$$⊢x=A\to \left(\left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)\leftrightarrow \left(A\underset{\dot{}}{,}A=Z\to A=\underset{\dot{}}{0}\right)\right)$$
17	16	rspccva	$$⊢\left(\forall x\in V\left(x\underset{\dot{}}{,}x=Z\to x=\underset{\dot{}}{0}\right)\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=Z\to A=\underset{\dot{}}{0}\right)$$
18	11 17	sylan	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=Z\to A=\underset{\dot{}}{0}\right)$$
19	1 2 3 4 5	ip0l	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \underset{\dot{}}{0}\underset{\dot{}}{,}A=Z$$
20		oveq1	$$⊢A=\underset{\dot{}}{0}\to A\underset{\dot{}}{,}A=\underset{\dot{}}{0}\underset{\dot{}}{,}A$$
21	20	eqeq1d	$$⊢A=\underset{\dot{}}{0}\to \left(A\underset{\dot{}}{,}A=Z\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{,}A=Z\right)$$
22	19 21	syl5ibrcom	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \left(A=\underset{\dot{}}{0}\to A\underset{\dot{}}{,}A=Z\right)$$
23	18 22	impbid	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\right)\to \left(A\underset{\dot{}}{,}A=Z\leftrightarrow A=\underset{\dot{}}{0}\right)$$