Metamath Proof Explorer

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
ip2eq.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
Assertion ip2eq

Proof

Step Hyp Ref Expression
1 ip2eq.h
2 ip2eq.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
3 oveq2
4 3 ralrimivw
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
10 oveq1
11 9 10 eqeq12d
12 11 rspcv
13 8 12 syl
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
20 14 8 15 16 19 syl13anc
21 20 eqeq1d
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
25 14 8 24 syl2anc
26 21 25 bitr3d
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
32 14 8 15 31 syl3anc
33 17 1 2 30 ipcl
34 14 8 16 33 syl3anc
35 30 22 18 grpsubeq0
36 29 32 34 35 syl3anc
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}}↔{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}}↔{A}={B}\right)$
41 26 36 40 3bitr3d
42 13 41 sylibd
43 4 42 impbid2