Theorem ip2eq

Description: Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	ip2eq.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	ip2eq.v	$$⊢V={\mathrm{Base}}_W$$
Assertion	ip2eq	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A=B\leftrightarrow \forall x\in Vx\underset{\dot{}}{,}A=x\underset{\dot{}}{,}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ip2eq.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
2		ip2eq.v	$$⊢V={\mathrm{Base}}_W$$
3		oveq2	$$⊢A=B\to x\underset{\dot{}}{,}A=x\underset{\dot{}}{,}B$$
4	3	ralrimivw	$$⊢A=B\to \forall x\in Vx\underset{\dot{}}{,}A=x\underset{\dot{}}{,}B$$
5		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
6		eqid	$$⊢{-}_W={-}_W$$
7	2 6	lmodvsubcl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in V\wedge B\in V\right)\to A{-}_{W}B\in V$$
8	5 7	syl3an1	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A{-}_{W}B\in V$$
9		oveq1	$$⊢x=A{-}_{W}B\to x\underset{\dot{}}{,}A=\left(A{-}_{W}B\right)\underset{\dot{}}{,}A$$
10		oveq1	$$⊢x=A{-}_{W}B\to x\underset{\dot{}}{,}B=\left(A{-}_{W}B\right)\underset{\dot{}}{,}B$$
11	9 10	eqeq12d	$$⊢x=A{-}_{W}B\to \left(x\underset{\dot{}}{,}A=x\underset{\dot{}}{,}B\leftrightarrow \left(A{-}_{W}B\right)\underset{\dot{}}{,}A=\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)$$
12	11	rspcv	$$⊢A{-}_{W}B\in V\to \left(\forall x\in Vx\underset{\dot{}}{,}A=x\underset{\dot{}}{,}B\to \left(A{-}_{W}B\right)\underset{\dot{}}{,}A=\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)$$
13	8 12	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(\forall x\in Vx\underset{\dot{}}{,}A=x\underset{\dot{}}{,}B\to \left(A{-}_{W}B\right)\underset{\dot{}}{,}A=\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)$$
14		simp1	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to W\in \mathrm{PreHil}$$
15		simp2	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A\in V$$
16		simp3	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to B\in V$$
17		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
18		eqid	$$⊢{-}_{\mathrm{Scalar}\left(W\right)}={-}_{\mathrm{Scalar}\left(W\right)}$$
19	17 1 2 6 18	ipsubdi	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A{-}_{W}B\in V\wedge A\in V\wedge B\in V\right)\right)\to \left(A{-}_{W}B\right)\underset{\dot{}}{,}\left(A{-}_{W}B\right)=\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}A\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)$$
20	14 8 15 16 19	syl13anc	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A{-}_{W}B\right)\underset{\dot{}}{,}\left(A{-}_{W}B\right)=\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}A\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)$$
21	20	eqeq1d	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}\left(A{-}_{W}B\right)=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow \left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}A\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)=0_{\mathrm{Scalar}\left(W\right)}\right)$$
22		eqid	$$⊢0_{\mathrm{Scalar}\left(W\right)}=0_{\mathrm{Scalar}\left(W\right)}$$
23		eqid	$$⊢0_W=0_W$$
24	17 1 2 22 23	ipeq0	$$⊢\left(W\in \mathrm{PreHil}\wedge A{-}_{W}B\in V\right)\to \left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}\left(A{-}_{W}B\right)=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow A{-}_{W}B=0_W\right)$$
25	14 8 24	syl2anc	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}\left(A{-}_{W}B\right)=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow A{-}_{W}B=0_W\right)$$
26	21 25	bitr3d	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}A\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow A{-}_{W}B=0_W\right)$$
27	5	3ad2ant1	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to W\in \mathrm{LMod}$$
28	17	lmodfgrp	$$⊢W\in \mathrm{LMod}\to \mathrm{Scalar}\left(W\right)\in \mathrm{Grp}$$
29	27 28	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \mathrm{Scalar}\left(W\right)\in \mathrm{Grp}$$
30		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
31	17 1 2 30	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A{-}_{W}B\in V\wedge A\in V\right)\to \left(A{-}_{W}B\right)\underset{\dot{}}{,}A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
32	14 8 15 31	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A{-}_{W}B\right)\underset{\dot{}}{,}A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
33	17 1 2 30	ipcl	$$⊢\left(W\in \mathrm{PreHil}\wedge A{-}_{W}B\in V\wedge B\in V\right)\to \left(A{-}_{W}B\right)\underset{\dot{}}{,}B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
34	14 8 16 33	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A{-}_{W}B\right)\underset{\dot{}}{,}B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
35	30 22 18	grpsubeq0	$$⊢\left(\mathrm{Scalar}\left(W\right)\in \mathrm{Grp}\wedge \left(A{-}_{W}B\right)\underset{\dot{}}{,}A\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\wedge \left(A{-}_{W}B\right)\underset{\dot{}}{,}B\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\right)\to \left(\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}A\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow \left(A{-}_{W}B\right)\underset{\dot{}}{,}A=\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)$$
36	29 32 34 35	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}A\right){-}_{\mathrm{Scalar}\left(W\right)}\left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)=0_{\mathrm{Scalar}\left(W\right)}\leftrightarrow \left(A{-}_{W}B\right)\underset{\dot{}}{,}A=\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\right)$$
37		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
38	5 37	syl	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{Grp}$$
39	2 23 6	grpsubeq0	$$⊢\left(W\in \mathrm{Grp}\wedge A\in V\wedge B\in V\right)\to \left(A{-}_{W}B=0_W\leftrightarrow A=B\right)$$
40	38 39	syl3an1	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A{-}_{W}B=0_W\leftrightarrow A=B\right)$$
41	26 36 40	3bitr3d	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(\left(A{-}_{W}B\right)\underset{\dot{}}{,}A=\left(A{-}_{W}B\right)\underset{\dot{}}{,}B\leftrightarrow A=B\right)$$
42	13 41	sylibd	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(\forall x\in Vx\underset{\dot{}}{,}A=x\underset{\dot{}}{,}B\to A=B\right)$$
43	4 42	impbid2	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to \left(A=B\leftrightarrow \forall x\in Vx\underset{\dot{}}{,}A=x\underset{\dot{}}{,}B\right)$$