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

Metamath Proof Explorer

Theorem lvecinv

Description: Invert coefficient of scalar product. (Contributed by NM, 11-Apr-2015)

Ref Expression
Hypotheses lvecinv.v 
|- V = ( Base ` W )
lvecinv.t 
|- .x. = ( .s ` W )
lvecinv.f 
|- F = ( Scalar ` W )
lvecinv.k 
|- K = ( Base ` F )
lvecinv.o 
|- .0. = ( 0g ` F )
lvecinv.i 
|- I = ( invr ` F )
lvecinv.w 
|- ( ph -> W e. LVec )
lvecinv.a 
|- ( ph -> A e. ( K \ { .0. } ) )
lvecinv.x 
|- ( ph -> X e. V )
lvecinv.y 
|- ( ph -> Y e. V )
Assertion lvecinv 
|- ( ph -> ( X = ( A .x. Y ) <-> Y = ( ( I ` A ) .x. X ) ) )

Proof

Step Hyp Ref Expression
1 lvecinv.v 
 |-  V = ( Base ` W )
2 lvecinv.t 
 |-  .x. = ( .s ` W )
3 lvecinv.f 
 |-  F = ( Scalar ` W )
4 lvecinv.k 
 |-  K = ( Base ` F )
5 lvecinv.o 
 |-  .0. = ( 0g ` F )
6 lvecinv.i 
 |-  I = ( invr ` F )
7 lvecinv.w 
 |-  ( ph -> W e. LVec )
8 lvecinv.a 
 |-  ( ph -> A e. ( K \ { .0. } ) )
9 lvecinv.x 
 |-  ( ph -> X e. V )
10 lvecinv.y 
 |-  ( ph -> Y e. V )
11 oveq2 
 |-  ( X = ( A .x. Y ) -> ( ( I ` A ) .x. X ) = ( ( I ` A ) .x. ( A .x. Y ) ) )
12 3 lvecdrng 
 |-  ( W e. LVec -> F e. DivRing )
13 7 12 syl 
 |-  ( ph -> F e. DivRing )
14 8 eldifad 
 |-  ( ph -> A e. K )
15 eldifsni 
 |-  ( A e. ( K \ { .0. } ) -> A =/= .0. )
16 8 15 syl 
 |-  ( ph -> A =/= .0. )
17 eqid 
 |-  ( .r ` F ) = ( .r ` F )
18 eqid 
 |-  ( 1r ` F ) = ( 1r ` F )
19 4 5 17 18 6 drnginvrl 
 |-  ( ( F e. DivRing /\ A e. K /\ A =/= .0. ) -> ( ( I ` A ) ( .r ` F ) A ) = ( 1r ` F ) )
20 13 14 16 19 syl3anc 
 |-  ( ph -> ( ( I ` A ) ( .r ` F ) A ) = ( 1r ` F ) )
21 20 oveq1d 
 |-  ( ph -> ( ( ( I ` A ) ( .r ` F ) A ) .x. Y ) = ( ( 1r ` F ) .x. Y ) )
22 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
23 7 22 syl 
 |-  ( ph -> W e. LMod )
24 4 5 6 drnginvrcl 
 |-  ( ( F e. DivRing /\ A e. K /\ A =/= .0. ) -> ( I ` A ) e. K )
25 13 14 16 24 syl3anc 
 |-  ( ph -> ( I ` A ) e. K )
26 1 3 2 4 17 lmodvsass 
 |-  ( ( W e. LMod /\ ( ( I ` A ) e. K /\ A e. K /\ Y e. V ) ) -> ( ( ( I ` A ) ( .r ` F ) A ) .x. Y ) = ( ( I ` A ) .x. ( A .x. Y ) ) )
27 23 25 14 10 26 syl13anc 
 |-  ( ph -> ( ( ( I ` A ) ( .r ` F ) A ) .x. Y ) = ( ( I ` A ) .x. ( A .x. Y ) ) )
28 1 3 2 18 lmodvs1 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( ( 1r ` F ) .x. Y ) = Y )
29 23 10 28 syl2anc 
 |-  ( ph -> ( ( 1r ` F ) .x. Y ) = Y )
30 21 27 29 3eqtr3d 
 |-  ( ph -> ( ( I ` A ) .x. ( A .x. Y ) ) = Y )
31 11 30 sylan9eqr 
 |-  ( ( ph /\ X = ( A .x. Y ) ) -> ( ( I ` A ) .x. X ) = Y )
32 4 5 17 18 6 drnginvrr 
 |-  ( ( F e. DivRing /\ A e. K /\ A =/= .0. ) -> ( A ( .r ` F ) ( I ` A ) ) = ( 1r ` F ) )
33 13 14 16 32 syl3anc 
 |-  ( ph -> ( A ( .r ` F ) ( I ` A ) ) = ( 1r ` F ) )
34 33 oveq1d 
 |-  ( ph -> ( ( A ( .r ` F ) ( I ` A ) ) .x. X ) = ( ( 1r ` F ) .x. X ) )
35 1 3 2 4 17 lmodvsass 
 |-  ( ( W e. LMod /\ ( A e. K /\ ( I ` A ) e. K /\ X e. V ) ) -> ( ( A ( .r ` F ) ( I ` A ) ) .x. X ) = ( A .x. ( ( I ` A ) .x. X ) ) )
36 23 14 25 9 35 syl13anc 
 |-  ( ph -> ( ( A ( .r ` F ) ( I ` A ) ) .x. X ) = ( A .x. ( ( I ` A ) .x. X ) ) )
37 1 3 2 18 lmodvs1 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 1r ` F ) .x. X ) = X )
38 23 9 37 syl2anc 
 |-  ( ph -> ( ( 1r ` F ) .x. X ) = X )
39 34 36 38 3eqtr3rd 
 |-  ( ph -> X = ( A .x. ( ( I ` A ) .x. X ) ) )
40 oveq2 
 |-  ( ( ( I ` A ) .x. X ) = Y -> ( A .x. ( ( I ` A ) .x. X ) ) = ( A .x. Y ) )
41 39 40 sylan9eq 
 |-  ( ( ph /\ ( ( I ` A ) .x. X ) = Y ) -> X = ( A .x. Y ) )
42 31 41 impbida 
 |-  ( ph -> ( X = ( A .x. Y ) <-> ( ( I ` A ) .x. X ) = Y ) )
43 eqcom 
 |-  ( ( ( I ` A ) .x. X ) = Y <-> Y = ( ( I ` A ) .x. X ) )
44 42 43 bitrdi 
 |-  ( ph -> ( X = ( A .x. Y ) <-> Y = ( ( I ` A ) .x. X ) ) )