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 ) ) )