This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ , = ( ·𝑖 ‘ 𝑊 )
ip2eq.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
Assertion ip2eq ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐴 ) = ( 𝑥 , 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ip2eq.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
2 ip2eq.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑥 , 𝐴 ) = ( 𝑥 , 𝐵 ) )
4 3 ralrimivw ⊢ ( 𝐴 = 𝐵 → ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐴 ) = ( 𝑥 , 𝐵 ) )
5 phllmod ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
6 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
7 2 6 lmodvsubcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 )
8 5 7 syl3an1 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 )
9 oveq1 ⊢ ( 𝑥 = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) → ( 𝑥 , 𝐴 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) )
10 oveq1 ⊢ ( 𝑥 = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) → ( 𝑥 , 𝐵 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) )
11 9 10 eqeq12d ⊢ ( 𝑥 = ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) → ( ( 𝑥 , 𝐴 ) = ( 𝑥 , 𝐵 ) ↔ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) )
12 11 rspcv ⊢ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 → ( ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐴 ) = ( 𝑥 , 𝐵 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) )
13 8 12 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐴 ) = ( 𝑥 , 𝐵 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) )
14 simp1 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑊 ∈ PreHil )
15 simp2 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
16 simp3 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
17 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
18 eqid ⊢ ( -g ‘ ( Scalar ‘ 𝑊 ) ) = ( -g ‘ ( Scalar ‘ 𝑊 ) )
19 17 1 2 6 18 ipsubdi ⊢ ( ( 𝑊 ∈ PreHil ∧ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) )
20 14 8 15 16 19 syl13anc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) )
21 20 eqeq1d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
22 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
23 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
24 17 1 2 22 23 ipeq0 ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ) → ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) = ( 0g ‘ 𝑊 ) ) )
25 14 8 24 syl2anc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) = ( 0g ‘ 𝑊 ) ) )
26 21 25 bitr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) = ( 0g ‘ 𝑊 ) ) )
27 5 3ad2ant1 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑊 ∈ LMod )
28 17 lmodfgrp ⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Grp )
29 27 28 syl ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( Scalar ‘ 𝑊 ) ∈ Grp )
30 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
31 17 1 2 30 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
32 14 8 15 31 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
33 17 1 2 30 ipcl ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
34 14 8 16 33 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
35 30 22 18 grpsubeq0 ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) )
36 29 32 34 35 syl3anc ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) ( -g ‘ ( Scalar ‘ 𝑊 ) ) ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ↔ ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ) )
37 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
38 5 37 syl ⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ Grp )
39 2 23 6 grpsubeq0 ⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) = ( 0g ‘ 𝑊 ) ↔ 𝐴 = 𝐵 ) )
40 38 39 syl3an1 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) = ( 0g ‘ 𝑊 ) ↔ 𝐴 = 𝐵 ) )
41 26 36 40 3bitr3d ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐴 ) = ( ( 𝐴 ( -g ‘ 𝑊 ) 𝐵 ) , 𝐵 ) ↔ 𝐴 = 𝐵 ) )
42 13 41 sylibd ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐴 ) = ( 𝑥 , 𝐵 ) → 𝐴 = 𝐵 ) )
43 4 42 impbid2 ⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑥 , 𝐴 ) = ( 𝑥 , 𝐵 ) ) )