Metamath Proof Explorer


Theorem lmodvsmdi

Description: Multiple distributive law for scalar product (left-distributivity). (Contributed by AV, 5-Sep-2019)

Ref Expression
Hypotheses lmodvsmdi.v
|- V = ( Base ` W )
lmodvsmdi.f
|- F = ( Scalar ` W )
lmodvsmdi.s
|- .x. = ( .s ` W )
lmodvsmdi.k
|- K = ( Base ` F )
lmodvsmdi.p
|- .^ = ( .g ` W )
lmodvsmdi.e
|- E = ( .g ` F )
Assertion lmodvsmdi
|- ( ( W e. LMod /\ ( R e. K /\ N e. NN0 /\ X e. V ) ) -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) )

Proof

Step Hyp Ref Expression
1 lmodvsmdi.v
 |-  V = ( Base ` W )
2 lmodvsmdi.f
 |-  F = ( Scalar ` W )
3 lmodvsmdi.s
 |-  .x. = ( .s ` W )
4 lmodvsmdi.k
 |-  K = ( Base ` F )
5 lmodvsmdi.p
 |-  .^ = ( .g ` W )
6 lmodvsmdi.e
 |-  E = ( .g ` F )
7 oveq1
 |-  ( x = 0 -> ( x .^ X ) = ( 0 .^ X ) )
8 7 oveq2d
 |-  ( x = 0 -> ( R .x. ( x .^ X ) ) = ( R .x. ( 0 .^ X ) ) )
9 oveq1
 |-  ( x = 0 -> ( x E R ) = ( 0 E R ) )
10 9 oveq1d
 |-  ( x = 0 -> ( ( x E R ) .x. X ) = ( ( 0 E R ) .x. X ) )
11 8 10 eqeq12d
 |-  ( x = 0 -> ( ( R .x. ( x .^ X ) ) = ( ( x E R ) .x. X ) <-> ( R .x. ( 0 .^ X ) ) = ( ( 0 E R ) .x. X ) ) )
12 11 imbi2d
 |-  ( x = 0 -> ( ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( x .^ X ) ) = ( ( x E R ) .x. X ) ) <-> ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( 0 .^ X ) ) = ( ( 0 E R ) .x. X ) ) ) )
13 oveq1
 |-  ( x = y -> ( x .^ X ) = ( y .^ X ) )
14 13 oveq2d
 |-  ( x = y -> ( R .x. ( x .^ X ) ) = ( R .x. ( y .^ X ) ) )
15 oveq1
 |-  ( x = y -> ( x E R ) = ( y E R ) )
16 15 oveq1d
 |-  ( x = y -> ( ( x E R ) .x. X ) = ( ( y E R ) .x. X ) )
17 14 16 eqeq12d
 |-  ( x = y -> ( ( R .x. ( x .^ X ) ) = ( ( x E R ) .x. X ) <-> ( R .x. ( y .^ X ) ) = ( ( y E R ) .x. X ) ) )
18 17 imbi2d
 |-  ( x = y -> ( ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( x .^ X ) ) = ( ( x E R ) .x. X ) ) <-> ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( y .^ X ) ) = ( ( y E R ) .x. X ) ) ) )
19 oveq1
 |-  ( x = ( y + 1 ) -> ( x .^ X ) = ( ( y + 1 ) .^ X ) )
20 19 oveq2d
 |-  ( x = ( y + 1 ) -> ( R .x. ( x .^ X ) ) = ( R .x. ( ( y + 1 ) .^ X ) ) )
21 oveq1
 |-  ( x = ( y + 1 ) -> ( x E R ) = ( ( y + 1 ) E R ) )
22 21 oveq1d
 |-  ( x = ( y + 1 ) -> ( ( x E R ) .x. X ) = ( ( ( y + 1 ) E R ) .x. X ) )
23 20 22 eqeq12d
 |-  ( x = ( y + 1 ) -> ( ( R .x. ( x .^ X ) ) = ( ( x E R ) .x. X ) <-> ( R .x. ( ( y + 1 ) .^ X ) ) = ( ( ( y + 1 ) E R ) .x. X ) ) )
24 23 imbi2d
 |-  ( x = ( y + 1 ) -> ( ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( x .^ X ) ) = ( ( x E R ) .x. X ) ) <-> ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( ( y + 1 ) .^ X ) ) = ( ( ( y + 1 ) E R ) .x. X ) ) ) )
25 oveq1
 |-  ( x = N -> ( x .^ X ) = ( N .^ X ) )
26 25 oveq2d
 |-  ( x = N -> ( R .x. ( x .^ X ) ) = ( R .x. ( N .^ X ) ) )
27 oveq1
 |-  ( x = N -> ( x E R ) = ( N E R ) )
28 27 oveq1d
 |-  ( x = N -> ( ( x E R ) .x. X ) = ( ( N E R ) .x. X ) )
29 26 28 eqeq12d
 |-  ( x = N -> ( ( R .x. ( x .^ X ) ) = ( ( x E R ) .x. X ) <-> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) )
30 29 imbi2d
 |-  ( x = N -> ( ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( x .^ X ) ) = ( ( x E R ) .x. X ) ) <-> ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) ) )
31 simpr
 |-  ( ( R e. K /\ X e. V ) -> X e. V )
32 31 adantr
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> X e. V )
33 eqid
 |-  ( 0g ` W ) = ( 0g ` W )
34 1 33 5 mulg0
 |-  ( X e. V -> ( 0 .^ X ) = ( 0g ` W ) )
35 32 34 syl
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( 0 .^ X ) = ( 0g ` W ) )
36 35 oveq2d
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( 0 .^ X ) ) = ( R .x. ( 0g ` W ) ) )
37 simpl
 |-  ( ( R e. K /\ X e. V ) -> R e. K )
38 37 anim1i
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R e. K /\ W e. LMod ) )
39 38 ancomd
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( W e. LMod /\ R e. K ) )
40 2 3 4 33 lmodvs0
 |-  ( ( W e. LMod /\ R e. K ) -> ( R .x. ( 0g ` W ) ) = ( 0g ` W ) )
41 39 40 syl
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( 0g ` W ) ) = ( 0g ` W ) )
42 31 anim1i
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( X e. V /\ W e. LMod ) )
43 42 ancomd
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( W e. LMod /\ X e. V ) )
44 eqid
 |-  ( 0g ` F ) = ( 0g ` F )
45 1 2 3 44 33 lmod0vs
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 0g ` F ) .x. X ) = ( 0g ` W ) )
46 43 45 syl
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( ( 0g ` F ) .x. X ) = ( 0g ` W ) )
47 37 adantr
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> R e. K )
48 4 44 6 mulg0
 |-  ( R e. K -> ( 0 E R ) = ( 0g ` F ) )
49 48 eqcomd
 |-  ( R e. K -> ( 0g ` F ) = ( 0 E R ) )
50 47 49 syl
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( 0g ` F ) = ( 0 E R ) )
51 50 oveq1d
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( ( 0g ` F ) .x. X ) = ( ( 0 E R ) .x. X ) )
52 41 46 51 3eqtr2d
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( 0g ` W ) ) = ( ( 0 E R ) .x. X ) )
53 36 52 eqtrd
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( 0 .^ X ) ) = ( ( 0 E R ) .x. X ) )
54 lmodgrp
 |-  ( W e. LMod -> W e. Grp )
55 54 grpmndd
 |-  ( W e. LMod -> W e. Mnd )
56 55 ad2antll
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> W e. Mnd )
57 simpl
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> y e. NN0 )
58 32 adantl
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> X e. V )
59 eqid
 |-  ( +g ` W ) = ( +g ` W )
60 1 5 59 mulgnn0p1
 |-  ( ( W e. Mnd /\ y e. NN0 /\ X e. V ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( +g ` W ) X ) )
61 56 57 58 60 syl3anc
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y + 1 ) .^ X ) = ( ( y .^ X ) ( +g ` W ) X ) )
62 61 oveq2d
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( R .x. ( ( y + 1 ) .^ X ) ) = ( R .x. ( ( y .^ X ) ( +g ` W ) X ) ) )
63 simpr
 |-  ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> W e. LMod )
64 63 adantl
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> W e. LMod )
65 simprll
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> R e. K )
66 1 5 mulgnn0cl
 |-  ( ( W e. Mnd /\ y e. NN0 /\ X e. V ) -> ( y .^ X ) e. V )
67 56 57 58 66 syl3anc
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( y .^ X ) e. V )
68 1 59 2 3 4 lmodvsdi
 |-  ( ( W e. LMod /\ ( R e. K /\ ( y .^ X ) e. V /\ X e. V ) ) -> ( R .x. ( ( y .^ X ) ( +g ` W ) X ) ) = ( ( R .x. ( y .^ X ) ) ( +g ` W ) ( R .x. X ) ) )
69 64 65 67 58 68 syl13anc
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( R .x. ( ( y .^ X ) ( +g ` W ) X ) ) = ( ( R .x. ( y .^ X ) ) ( +g ` W ) ( R .x. X ) ) )
70 62 69 eqtrd
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( R .x. ( ( y + 1 ) .^ X ) ) = ( ( R .x. ( y .^ X ) ) ( +g ` W ) ( R .x. X ) ) )
71 oveq1
 |-  ( ( R .x. ( y .^ X ) ) = ( ( y E R ) .x. X ) -> ( ( R .x. ( y .^ X ) ) ( +g ` W ) ( R .x. X ) ) = ( ( ( y E R ) .x. X ) ( +g ` W ) ( R .x. X ) ) )
72 70 71 sylan9eq
 |-  ( ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) /\ ( R .x. ( y .^ X ) ) = ( ( y E R ) .x. X ) ) -> ( R .x. ( ( y + 1 ) .^ X ) ) = ( ( ( y E R ) .x. X ) ( +g ` W ) ( R .x. X ) ) )
73 2 lmodfgrp
 |-  ( W e. LMod -> F e. Grp )
74 73 grpmndd
 |-  ( W e. LMod -> F e. Mnd )
75 74 ad2antll
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> F e. Mnd )
76 4 6 mulgnn0cl
 |-  ( ( F e. Mnd /\ y e. NN0 /\ R e. K ) -> ( y E R ) e. K )
77 75 57 65 76 syl3anc
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( y E R ) e. K )
78 eqid
 |-  ( +g ` F ) = ( +g ` F )
79 1 59 2 3 4 78 lmodvsdir
 |-  ( ( W e. LMod /\ ( ( y E R ) e. K /\ R e. K /\ X e. V ) ) -> ( ( ( y E R ) ( +g ` F ) R ) .x. X ) = ( ( ( y E R ) .x. X ) ( +g ` W ) ( R .x. X ) ) )
80 64 77 65 58 79 syl13anc
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( ( y E R ) ( +g ` F ) R ) .x. X ) = ( ( ( y E R ) .x. X ) ( +g ` W ) ( R .x. X ) ) )
81 4 6 78 mulgnn0p1
 |-  ( ( F e. Mnd /\ y e. NN0 /\ R e. K ) -> ( ( y + 1 ) E R ) = ( ( y E R ) ( +g ` F ) R ) )
82 75 57 65 81 syl3anc
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y + 1 ) E R ) = ( ( y E R ) ( +g ` F ) R ) )
83 82 eqcomd
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y E R ) ( +g ` F ) R ) = ( ( y + 1 ) E R ) )
84 83 oveq1d
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( ( y E R ) ( +g ` F ) R ) .x. X ) = ( ( ( y + 1 ) E R ) .x. X ) )
85 80 84 eqtr3d
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( ( y E R ) .x. X ) ( +g ` W ) ( R .x. X ) ) = ( ( ( y + 1 ) E R ) .x. X ) )
86 85 adantr
 |-  ( ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) /\ ( R .x. ( y .^ X ) ) = ( ( y E R ) .x. X ) ) -> ( ( ( y E R ) .x. X ) ( +g ` W ) ( R .x. X ) ) = ( ( ( y + 1 ) E R ) .x. X ) )
87 72 86 eqtrd
 |-  ( ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) /\ ( R .x. ( y .^ X ) ) = ( ( y E R ) .x. X ) ) -> ( R .x. ( ( y + 1 ) .^ X ) ) = ( ( ( y + 1 ) E R ) .x. X ) )
88 87 exp31
 |-  ( y e. NN0 -> ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( ( R .x. ( y .^ X ) ) = ( ( y E R ) .x. X ) -> ( R .x. ( ( y + 1 ) .^ X ) ) = ( ( ( y + 1 ) E R ) .x. X ) ) ) )
89 88 a2d
 |-  ( y e. NN0 -> ( ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( y .^ X ) ) = ( ( y E R ) .x. X ) ) -> ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( ( y + 1 ) .^ X ) ) = ( ( ( y + 1 ) E R ) .x. X ) ) ) )
90 12 18 24 30 53 89 nn0ind
 |-  ( N e. NN0 -> ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) )
91 90 exp4c
 |-  ( N e. NN0 -> ( R e. K -> ( X e. V -> ( W e. LMod -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) ) ) )
92 91 com12
 |-  ( R e. K -> ( N e. NN0 -> ( X e. V -> ( W e. LMod -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) ) ) )
93 92 3imp
 |-  ( ( R e. K /\ N e. NN0 /\ X e. V ) -> ( W e. LMod -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) )
94 93 impcom
 |-  ( ( W e. LMod /\ ( R e. K /\ N e. NN0 /\ X e. V ) ) -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) )