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=⋅𝑖OLD⁡U
ip2eqi.u ⊢U∈CPreHilOLD
Assertion ip2eqi ⊢A∈X∧B∈X→∀x∈XxPA=xPB↔A=B

Proof

Step Hyp Ref Expression
1 ip2eqi.1 ⊢X=BaseSet⁡U
2 ip2eqi.7 ⊢P=⋅𝑖OLD⁡U
3 ip2eqi.u ⊢U∈CPreHilOLD
4 3 phnvi ⊢U∈NrmCVec
5 eqid ⊢-v⁡U=-v⁡U
6 1 5 nvmcl ⊢U∈NrmCVec∧A∈X∧B∈X→A-v⁡UB∈X
7 4 6 mp3an1 ⊢A∈X∧B∈X→A-v⁡UB∈X
8 oveq1 ⊢x=A-v⁡UB→xPA=A-v⁡UBPA
9 oveq1 ⊢x=A-v⁡UB→xPB=A-v⁡UBPB
10 8 9 eqeq12d ⊢x=A-v⁡UB→xPA=xPB↔A-v⁡UBPA=A-v⁡UBPB
11 10 rspcv ⊢A-v⁡UB∈X→∀x∈XxPA=xPB→A-v⁡UBPA=A-v⁡UBPB
12 7 11 syl ⊢A∈X∧B∈X→∀x∈XxPA=xPB→A-v⁡UBPA=A-v⁡UBPB
13 simpl ⊢A∈X∧B∈X→A∈X
14 simpr ⊢A∈X∧B∈X→B∈X
15 1 5 2 dipsubdi ⊢U∈CPreHilOLD∧A-v⁡UB∈X∧A∈X∧B∈X→A-v⁡UBPA-v⁡UB=A-v⁡UBPA−A-v⁡UBPB
16 3 15 mpan ⊢A-v⁡UB∈X∧A∈X∧B∈X→A-v⁡UBPA-v⁡UB=A-v⁡UBPA−A-v⁡UBPB
17 7 13 14 16 syl3anc ⊢A∈X∧B∈X→A-v⁡UBPA-v⁡UB=A-v⁡UBPA−A-v⁡UBPB
18 17 eqeq1d ⊢A∈X∧B∈X→A-v⁡UBPA-v⁡UB=0↔A-v⁡UBPA−A-v⁡UBPB=0
19 eqid ⊢0vec⁡U=0vec⁡U
20 1 19 2 ipz ⊢U∈NrmCVec∧A-v⁡UB∈X→A-v⁡UBPA-v⁡UB=0↔A-v⁡UB=0vec⁡U
21 4 20 mpan ⊢A-v⁡UB∈X→A-v⁡UBPA-v⁡UB=0↔A-v⁡UB=0vec⁡U
22 7 21 syl ⊢A∈X∧B∈X→A-v⁡UBPA-v⁡UB=0↔A-v⁡UB=0vec⁡U
23 18 22 bitr3d ⊢A∈X∧B∈X→A-v⁡UBPA−A-v⁡UBPB=0↔A-v⁡UB=0vec⁡U
24 1 2 dipcl ⊢U∈NrmCVec∧A-v⁡UB∈X∧A∈X→A-v⁡UBPA∈ℂ
25 4 24 mp3an1 ⊢A-v⁡UB∈X∧A∈X→A-v⁡UBPA∈ℂ
26 7 13 25 syl2anc ⊢A∈X∧B∈X→A-v⁡UBPA∈ℂ
27 1 2 dipcl ⊢U∈NrmCVec∧A-v⁡UB∈X∧B∈X→A-v⁡UBPB∈ℂ
28 4 27 mp3an1 ⊢A-v⁡UB∈X∧B∈X→A-v⁡UBPB∈ℂ
29 7 28 sylancom ⊢A∈X∧B∈X→A-v⁡UBPB∈ℂ
30 26 29 subeq0ad ⊢A∈X∧B∈X→A-v⁡UBPA−A-v⁡UBPB=0↔A-v⁡UBPA=A-v⁡UBPB
31 1 5 19 nvmeq0 ⊢U∈NrmCVec∧A∈X∧B∈X→A-v⁡UB=0vec⁡U↔A=B
32 4 31 mp3an1 ⊢A∈X∧B∈X→A-v⁡UB=0vec⁡U↔A=B
33 23 30 32 3bitr3d ⊢A∈X∧B∈X→A-v⁡UBPA=A-v⁡UBPB↔A=B
34 12 33 sylibd ⊢A∈X∧B∈X→∀x∈XxPA=xPB→A=B
35 oveq2 ⊢A=B→xPA=xPB
36 35 ralrimivw ⊢A=B→∀x∈XxPA=xPB
37 34 36 impbid1 ⊢A∈X∧B∈X→∀x∈XxPA=xPB↔A=B