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 ∈ CPreHil OLD
Assertion ip2eqi ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X x P A = x P B ↔ A = B

Proof

Step Hyp Ref Expression
1 ip2eqi.1 ⊢ X = BaseSet ⁡ U
2 ip2eqi.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
3 ip2eqi.u ⊢ U ∈ CPreHil OLD
4 3 phnvi ⊢ U ∈ NrmCVec
5 eqid ⊢ - v ⁡ U = - v ⁡ U
6 1 5 nvmcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A - v ⁡ U B ∈ X
7 4 6 mp3an1 ⊢ A ∈ X ∧ B ∈ X → A - v ⁡ U B ∈ 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 ∈ X → ∀ x ∈ X x P A = x P B → A - v ⁡ U B P A = A - v ⁡ U B P B
12 7 11 syl ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X x P A = x P B → A - v ⁡ U B P A = A - v ⁡ U B P B
13 simpl ⊢ A ∈ X ∧ B ∈ X → A ∈ X
14 simpr ⊢ A ∈ X ∧ B ∈ X → B ∈ X
15 1 5 2 dipsubdi ⊢ U ∈ CPreHil OLD ∧ A - v ⁡ U B ∈ X ∧ A ∈ X ∧ B ∈ 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 ∈ X ∧ A ∈ X ∧ B ∈ 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 ∈ X ∧ B ∈ 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 ∈ X ∧ B ∈ 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 ⊢ 0 vec ⁡ U = 0 vec ⁡ U
20 1 19 2 ipz ⊢ U ∈ NrmCVec ∧ A - v ⁡ U B ∈ X → A - v ⁡ U B P A - v ⁡ U B = 0 ↔ A - v ⁡ U B = 0 vec ⁡ U
21 4 20 mpan ⊢ A - v ⁡ U B ∈ X → A - v ⁡ U B P A - v ⁡ U B = 0 ↔ A - v ⁡ U B = 0 vec ⁡ U
22 7 21 syl ⊢ A ∈ X ∧ B ∈ X → A - v ⁡ U B P A - v ⁡ U B = 0 ↔ A - v ⁡ U B = 0 vec ⁡ U
23 18 22 bitr3d ⊢ A ∈ X ∧ B ∈ X → A - v ⁡ U B P A − A - v ⁡ U B P B = 0 ↔ A - v ⁡ U B = 0 vec ⁡ U
24 1 2 dipcl ⊢ U ∈ NrmCVec ∧ A - v ⁡ U B ∈ X ∧ A ∈ X → A - v ⁡ U B P A ∈ ℂ
25 4 24 mp3an1 ⊢ A - v ⁡ U B ∈ X ∧ A ∈ X → A - v ⁡ U B P A ∈ ℂ
26 7 13 25 syl2anc ⊢ A ∈ X ∧ B ∈ X → A - v ⁡ U B P A ∈ ℂ
27 1 2 dipcl ⊢ U ∈ NrmCVec ∧ A - v ⁡ U B ∈ X ∧ B ∈ X → A - v ⁡ U B P B ∈ ℂ
28 4 27 mp3an1 ⊢ A - v ⁡ U B ∈ X ∧ B ∈ X → A - v ⁡ U B P B ∈ ℂ
29 7 28 sylancom ⊢ A ∈ X ∧ B ∈ X → A - v ⁡ U B P B ∈ ℂ
30 26 29 subeq0ad ⊢ A ∈ X ∧ B ∈ 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 ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A - v ⁡ U B = 0 vec ⁡ U ↔ A = B
32 4 31 mp3an1 ⊢ A ∈ X ∧ B ∈ X → A - v ⁡ U B = 0 vec ⁡ U ↔ A = B
33 23 30 32 3bitr3d ⊢ A ∈ X ∧ B ∈ X → A - v ⁡ U B P A = A - v ⁡ U B P B ↔ A = B
34 12 33 sylibd ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X x P A = x P B → A = B
35 oveq2 ⊢ A = B → x P A = x P B
36 35 ralrimivw ⊢ A = B → ∀ x ∈ X x P A = x P B
37 34 36 impbid1 ⊢ A ∈ X ∧ B ∈ X → ∀ x ∈ X x P A = x P B ↔ A = B