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 
|- ., = ( .i ` W )
ip2eq.v 
|- V = ( Base ` W )
Assertion ip2eq 
|- ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( A = B <-> A. x e. V ( x ., A ) = ( x ., B ) ) )

Proof

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