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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
ip2eqi.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
ip2eqi.u ⊢ 𝑈 ∈ CPreHilOLD
Assertion ip2eqi ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 𝐴 ) = ( 𝑥 𝑃 𝐵 ) ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ip2eqi.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip2eqi.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3 ip2eqi.u ⊢ 𝑈 ∈ CPreHilOLD
4 3 phnvi ⊢ 𝑈 ∈ NrmCVec
5 eqid ⊢ ( −𝑣 ‘ 𝑈 ) = ( −𝑣 ‘ 𝑈 )
6 1 5 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 )
7 4 6 mp3an1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 )
8 oveq1 ⊢ ( 𝑥 = ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) → ( 𝑥 𝑃 𝐴 ) = ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) )
9 oveq1 ⊢ ( 𝑥 = ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) → ( 𝑥 𝑃 𝐵 ) = ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) )
10 8 9 eqeq12d ⊢ ( 𝑥 = ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) → ( ( 𝑥 𝑃 𝐴 ) = ( 𝑥 𝑃 𝐵 ) ↔ ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) = ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) )
11 10 rspcv ⊢ ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 𝐴 ) = ( 𝑥 𝑃 𝐵 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) = ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) )
12 7 11 syl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 𝐴 ) = ( 𝑥 𝑃 𝐵 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) = ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) )
13 simpl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
14 simpr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
15 1 5 2 dipsubdi ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) = ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) − ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) )
16 3 15 mpan ⊢ ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) = ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) − ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) )
17 7 13 14 16 syl3anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) = ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) − ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) )
18 17 eqeq1d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) = 0 ↔ ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) − ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) = 0 ) )
19 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
20 1 19 2 ipz ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ) → ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) = 0 ↔ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) = ( 0vec ‘ 𝑈 ) ) )
21 4 20 mpan ⊢ ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 → ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) = 0 ↔ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) = ( 0vec ‘ 𝑈 ) ) )
22 7 21 syl ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ) = 0 ↔ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) = ( 0vec ‘ 𝑈 ) ) )
23 18 22 bitr3d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) − ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) = 0 ↔ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) = ( 0vec ‘ 𝑈 ) ) )
24 1 2 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) ∈ ℂ )
25 4 24 mp3an1 ⊢ ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) ∈ ℂ )
26 7 13 25 syl2anc ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) ∈ ℂ )
27 1 2 dipcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ∈ ℂ )
28 4 27 mp3an1 ⊢ ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ∈ ℂ )
29 7 28 sylancom ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ∈ ℂ )
30 26 29 subeq0ad ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) − ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) = 0 ↔ ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) = ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ) )
31 1 5 19 nvmeq0 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) = ( 0vec ‘ 𝑈 ) ↔ 𝐴 = 𝐵 ) )
32 4 31 mp3an1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) = ( 0vec ‘ 𝑈 ) ↔ 𝐴 = 𝐵 ) )
33 23 30 32 3bitr3d ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐴 ) = ( ( 𝐴 ( −𝑣 ‘ 𝑈 ) 𝐵 ) 𝑃 𝐵 ) ↔ 𝐴 = 𝐵 ) )
34 12 33 sylibd ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 𝐴 ) = ( 𝑥 𝑃 𝐵 ) → 𝐴 = 𝐵 ) )
35 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑥 𝑃 𝐴 ) = ( 𝑥 𝑃 𝐵 ) )
36 35 ralrimivw ⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 𝐴 ) = ( 𝑥 𝑃 𝐵 ) )
37 34 36 impbid1 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 𝐴 ) = ( 𝑥 𝑃 𝐵 ) ↔ 𝐴 = 𝐵 ) )