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 56 57 58 mulgnn0cld 
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( y .^ X ) e. V )
67 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 ) ) )
68 64 65 66 58 67 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 ) ) )
69 62 68 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 ) ) )
70 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 ) ) )
71 69 70 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 ) ) )
72 2 lmodfgrp 
 |-  ( W e. LMod -> F e. Grp )
73 72 grpmndd 
 |-  ( W e. LMod -> F e. Mnd )
74 73 ad2antll 
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> F e. Mnd )
75 4 6 74 57 65 mulgnn0cld 
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( y E R ) e. K )
76 eqid 
 |-  ( +g ` F ) = ( +g ` F )
77 1 59 2 3 4 76 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 ) ) )
78 64 75 65 58 77 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 ) ) )
79 4 6 76 mulgnn0p1 
 |-  ( ( F e. Mnd /\ y e. NN0 /\ R e. K ) -> ( ( y + 1 ) E R ) = ( ( y E R ) ( +g ` F ) R ) )
80 74 57 65 79 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y + 1 ) E R ) = ( ( y E R ) ( +g ` F ) R ) )
81 80 eqcomd 
 |-  ( ( y e. NN0 /\ ( ( R e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y E R ) ( +g ` F ) R ) = ( ( y + 1 ) E R ) )
82 81 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 ) )
83 78 82 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 ) )
84 83 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 ) )
85 71 84 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 ) )
86 85 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 ) ) ) )
87 86 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 ) ) ) )
88 12 18 24 30 53 87 nn0ind 
 |-  ( N e. NN0 -> ( ( ( R e. K /\ X e. V ) /\ W e. LMod ) -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) )
89 88 exp4c 
 |-  ( N e. NN0 -> ( R e. K -> ( X e. V -> ( W e. LMod -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) ) ) )
90 89 com12 
 |-  ( R e. K -> ( N e. NN0 -> ( X e. V -> ( W e. LMod -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) ) ) )
91 90 3imp 
 |-  ( ( R e. K /\ N e. NN0 /\ X e. V ) -> ( W e. LMod -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) ) )
92 91 impcom 
 |-  ( ( W e. LMod /\ ( R e. K /\ N e. NN0 /\ X e. V ) ) -> ( R .x. ( N .^ X ) ) = ( ( N E R ) .x. X ) )