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 โˆง ๐ด โˆˆ ๐‘‰ โˆง ๐ต โˆˆ ๐‘‰ ) โ†’ ( ๐ด = ๐ต โ†” โˆ€ ๐‘ฅ โˆˆ ๐‘‰ ( ๐‘ฅ , ๐ด ) = ( ๐‘ฅ , ๐ต ) ) )