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{˙}{,} = \cdot_{𝑖} (W)$
	ip2eq.v	$⊢ V = {Base}_{W}$
Assertion	ip2eq	$⊢ (W \in PreHil \land A \in V \land B \in V) \to (A = B \leftrightarrow \forall x \in V x \underset{˙}{,} A = x \underset{˙}{,} B)$

Proof

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

Metamath Proof Explorer

Theorem ip2eq

Proof