Metamath Proof Explorer

Theorem ip2eqi

Description: Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses ip2eqi.1 
|- X = ( BaseSet ` U )
ip2eqi.7 
|- P = ( .iOLD ` U )
ip2eqi.u 
|- U e. CPreHilOLD
Assertion ip2eqi 
|- ( ( A e. X /\ B e. X ) -> ( A. x e. X ( x P A ) = ( x P B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 ip2eqi.1 
 |-  X = ( BaseSet ` U )
2 ip2eqi.7 
 |-  P = ( .iOLD ` U )
3 ip2eqi.u 
 |-  U e. CPreHilOLD
4 3 phnvi 
 |-  U e. NrmCVec
5 eqid 
 |-  ( -v ` U ) = ( -v ` U )
6 1 5 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A ( -v ` U ) B ) e. X )
7 4 6 mp3an1 
 |-  ( ( A e. X /\ B e. X ) -> ( A ( -v ` U ) B ) e. X )
8 oveq1 
 |-  ( x = ( A ( -v ` U ) B ) -> ( x P A ) = ( ( A ( -v ` U ) B ) P A ) )
9 oveq1 
 |-  ( x = ( A ( -v ` U ) B ) -> ( x P B ) = ( ( A ( -v ` U ) B ) P B ) )
10 8 9 eqeq12d 
 |-  ( x = ( A ( -v ` U ) B ) -> ( ( x P A ) = ( x P B ) <-> ( ( A ( -v ` U ) B ) P A ) = ( ( A ( -v ` U ) B ) P B ) ) )
11 10 rspcv 
 |-  ( ( A ( -v ` U ) B ) e. X -> ( A. x e. X ( x P A ) = ( x P B ) -> ( ( A ( -v ` U ) B ) P A ) = ( ( A ( -v ` U ) B ) P B ) ) )
12 7 11 syl 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X ( x P A ) = ( x P B ) -> ( ( A ( -v ` U ) B ) P A ) = ( ( A ( -v ` U ) B ) P B ) ) )
13 simpl 
 |-  ( ( A e. X /\ B e. X ) -> A e. X )
14 simpr 
 |-  ( ( A e. X /\ B e. X ) -> B e. X )
15 1 5 2 dipsubdi 
 |-  ( ( U e. CPreHilOLD /\ ( ( A ( -v ` U ) B ) e. X /\ A e. X /\ B e. X ) ) -> ( ( A ( -v ` U ) B ) P ( A ( -v ` U ) B ) ) = ( ( ( A ( -v ` U ) B ) P A ) - ( ( A ( -v ` U ) B ) P B ) ) )
16 3 15 mpan 
 |-  ( ( ( A ( -v ` U ) B ) e. X /\ A e. X /\ B e. X ) -> ( ( A ( -v ` U ) B ) P ( A ( -v ` U ) B ) ) = ( ( ( A ( -v ` U ) B ) P A ) - ( ( A ( -v ` U ) B ) P B ) ) )
17 7 13 14 16 syl3anc 
 |-  ( ( A e. X /\ B e. X ) -> ( ( A ( -v ` U ) B ) P ( A ( -v ` U ) B ) ) = ( ( ( A ( -v ` U ) B ) P A ) - ( ( A ( -v ` U ) B ) P B ) ) )
18 17 eqeq1d 
 |-  ( ( A e. X /\ B e. X ) -> ( ( ( A ( -v ` U ) B ) P ( A ( -v ` U ) B ) ) = 0 <-> ( ( ( A ( -v ` U ) B ) P A ) - ( ( A ( -v ` U ) B ) P B ) ) = 0 ) )
19 eqid 
 |-  ( 0vec ` U ) = ( 0vec ` U )
20 1 19 2 ipz 
 |-  ( ( U e. NrmCVec /\ ( A ( -v ` U ) B ) e. X ) -> ( ( ( A ( -v ` U ) B ) P ( A ( -v ` U ) B ) ) = 0 <-> ( A ( -v ` U ) B ) = ( 0vec ` U ) ) )
21 4 20 mpan 
 |-  ( ( A ( -v ` U ) B ) e. X -> ( ( ( A ( -v ` U ) B ) P ( A ( -v ` U ) B ) ) = 0 <-> ( A ( -v ` U ) B ) = ( 0vec ` U ) ) )
22 7 21 syl 
 |-  ( ( A e. X /\ B e. X ) -> ( ( ( A ( -v ` U ) B ) P ( A ( -v ` U ) B ) ) = 0 <-> ( A ( -v ` U ) B ) = ( 0vec ` U ) ) )
23 18 22 bitr3d 
 |-  ( ( A e. X /\ B e. X ) -> ( ( ( ( A ( -v ` U ) B ) P A ) - ( ( A ( -v ` U ) B ) P B ) ) = 0 <-> ( A ( -v ` U ) B ) = ( 0vec ` U ) ) )
24 1 2 dipcl 
 |-  ( ( U e. NrmCVec /\ ( A ( -v ` U ) B ) e. X /\ A e. X ) -> ( ( A ( -v ` U ) B ) P A ) e. CC )
25 4 24 mp3an1 
 |-  ( ( ( A ( -v ` U ) B ) e. X /\ A e. X ) -> ( ( A ( -v ` U ) B ) P A ) e. CC )
26 7 13 25 syl2anc 
 |-  ( ( A e. X /\ B e. X ) -> ( ( A ( -v ` U ) B ) P A ) e. CC )
27 1 2 dipcl 
 |-  ( ( U e. NrmCVec /\ ( A ( -v ` U ) B ) e. X /\ B e. X ) -> ( ( A ( -v ` U ) B ) P B ) e. CC )
28 4 27 mp3an1 
 |-  ( ( ( A ( -v ` U ) B ) e. X /\ B e. X ) -> ( ( A ( -v ` U ) B ) P B ) e. CC )
29 7 28 sylancom 
 |-  ( ( A e. X /\ B e. X ) -> ( ( A ( -v ` U ) B ) P B ) e. CC )
30 26 29 subeq0ad 
 |-  ( ( A e. X /\ B e. X ) -> ( ( ( ( A ( -v ` U ) B ) P A ) - ( ( A ( -v ` U ) B ) P B ) ) = 0 <-> ( ( A ( -v ` U ) B ) P A ) = ( ( A ( -v ` U ) B ) P B ) ) )
31 1 5 19 nvmeq0 
 |-  ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( ( A ( -v ` U ) B ) = ( 0vec ` U ) <-> A = B ) )
32 4 31 mp3an1 
 |-  ( ( A e. X /\ B e. X ) -> ( ( A ( -v ` U ) B ) = ( 0vec ` U ) <-> A = B ) )
33 23 30 32 3bitr3d 
 |-  ( ( A e. X /\ B e. X ) -> ( ( ( A ( -v ` U ) B ) P A ) = ( ( A ( -v ` U ) B ) P B ) <-> A = B ) )
34 12 33 sylibd 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X ( x P A ) = ( x P B ) -> A = B ) )
35 oveq2 
 |-  ( A = B -> ( x P A ) = ( x P B ) )
36 35 ralrimivw 
 |-  ( A = B -> A. x e. X ( x P A ) = ( x P B ) )
37 34 36 impbid1 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X ( x P A ) = ( x P B ) <-> A = B ) )