Metamath Proof Explorer

Theorem lmodvsmmulgdi

Description: Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019)

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

Proof

Step Hyp Ref Expression
1 lmodvsmmulgdi.v 
 |-  V = ( Base ` W )
2 lmodvsmmulgdi.f 
 |-  F = ( Scalar ` W )
3 lmodvsmmulgdi.s 
 |-  .x. = ( .s ` W )
4 lmodvsmmulgdi.k 
 |-  K = ( Base ` F )
5 lmodvsmmulgdi.p 
 |-  .^ = ( .g ` W )
6 lmodvsmmulgdi.e 
 |-  E = ( .g ` F )
7 oveq1 
 |-  ( x = 0 -> ( x .^ ( C .x. X ) ) = ( 0 .^ ( C .x. X ) ) )
8 oveq1 
 |-  ( x = 0 -> ( x E C ) = ( 0 E C ) )
9 8 oveq1d 
 |-  ( x = 0 -> ( ( x E C ) .x. X ) = ( ( 0 E C ) .x. X ) )
10 7 9 eqeq12d 
 |-  ( x = 0 -> ( ( x .^ ( C .x. X ) ) = ( ( x E C ) .x. X ) <-> ( 0 .^ ( C .x. X ) ) = ( ( 0 E C ) .x. X ) ) )
11 10 imbi2d 
 |-  ( x = 0 -> ( ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( x .^ ( C .x. X ) ) = ( ( x E C ) .x. X ) ) <-> ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( 0 .^ ( C .x. X ) ) = ( ( 0 E C ) .x. X ) ) ) )
12 oveq1 
 |-  ( x = y -> ( x .^ ( C .x. X ) ) = ( y .^ ( C .x. X ) ) )
13 oveq1 
 |-  ( x = y -> ( x E C ) = ( y E C ) )
14 13 oveq1d 
 |-  ( x = y -> ( ( x E C ) .x. X ) = ( ( y E C ) .x. X ) )
15 12 14 eqeq12d 
 |-  ( x = y -> ( ( x .^ ( C .x. X ) ) = ( ( x E C ) .x. X ) <-> ( y .^ ( C .x. X ) ) = ( ( y E C ) .x. X ) ) )
16 15 imbi2d 
 |-  ( x = y -> ( ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( x .^ ( C .x. X ) ) = ( ( x E C ) .x. X ) ) <-> ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( y .^ ( C .x. X ) ) = ( ( y E C ) .x. X ) ) ) )
17 oveq1 
 |-  ( x = ( y + 1 ) -> ( x .^ ( C .x. X ) ) = ( ( y + 1 ) .^ ( C .x. X ) ) )
18 oveq1 
 |-  ( x = ( y + 1 ) -> ( x E C ) = ( ( y + 1 ) E C ) )
19 18 oveq1d 
 |-  ( x = ( y + 1 ) -> ( ( x E C ) .x. X ) = ( ( ( y + 1 ) E C ) .x. X ) )
20 17 19 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( x .^ ( C .x. X ) ) = ( ( x E C ) .x. X ) <-> ( ( y + 1 ) .^ ( C .x. X ) ) = ( ( ( y + 1 ) E C ) .x. X ) ) )
21 20 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( x .^ ( C .x. X ) ) = ( ( x E C ) .x. X ) ) <-> ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( ( y + 1 ) .^ ( C .x. X ) ) = ( ( ( y + 1 ) E C ) .x. X ) ) ) )
22 oveq1 
 |-  ( x = N -> ( x .^ ( C .x. X ) ) = ( N .^ ( C .x. X ) ) )
23 oveq1 
 |-  ( x = N -> ( x E C ) = ( N E C ) )
24 23 oveq1d 
 |-  ( x = N -> ( ( x E C ) .x. X ) = ( ( N E C ) .x. X ) )
25 22 24 eqeq12d 
 |-  ( x = N -> ( ( x .^ ( C .x. X ) ) = ( ( x E C ) .x. X ) <-> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) ) )
26 25 imbi2d 
 |-  ( x = N -> ( ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( x .^ ( C .x. X ) ) = ( ( x E C ) .x. X ) ) <-> ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) ) ) )
27 simpr 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> W e. LMod )
28 simpr 
 |-  ( ( C e. K /\ X e. V ) -> X e. V )
29 28 adantr 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> X e. V )
30 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
31 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
32 1 2 3 30 31 lmod0vs 
 |-  ( ( W e. LMod /\ X e. V ) -> ( ( 0g ` F ) .x. X ) = ( 0g ` W ) )
33 27 29 32 syl2anc 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( ( 0g ` F ) .x. X ) = ( 0g ` W ) )
34 simpl 
 |-  ( ( C e. K /\ X e. V ) -> C e. K )
35 34 adantr 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> C e. K )
36 4 30 6 mulg0 
 |-  ( C e. K -> ( 0 E C ) = ( 0g ` F ) )
37 35 36 syl 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( 0 E C ) = ( 0g ` F ) )
38 37 oveq1d 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( ( 0 E C ) .x. X ) = ( ( 0g ` F ) .x. X ) )
39 1 2 3 4 lmodvscl 
 |-  ( ( W e. LMod /\ C e. K /\ X e. V ) -> ( C .x. X ) e. V )
40 27 35 29 39 syl3anc 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( C .x. X ) e. V )
41 1 31 5 mulg0 
 |-  ( ( C .x. X ) e. V -> ( 0 .^ ( C .x. X ) ) = ( 0g ` W ) )
42 40 41 syl 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( 0 .^ ( C .x. X ) ) = ( 0g ` W ) )
43 33 38 42 3eqtr4rd 
 |-  ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( 0 .^ ( C .x. X ) ) = ( ( 0 E C ) .x. X ) )
44 lmodgrp 
 |-  ( W e. LMod -> W e. Grp )
45 44 grpmndd 
 |-  ( W e. LMod -> W e. Mnd )
46 45 ad2antll 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> W e. Mnd )
47 simpl 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> y e. NN0 )
48 40 adantl 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( C .x. X ) e. V )
49 eqid 
 |-  ( +g ` W ) = ( +g ` W )
50 1 5 49 mulgnn0p1 
 |-  ( ( W e. Mnd /\ y e. NN0 /\ ( C .x. X ) e. V ) -> ( ( y + 1 ) .^ ( C .x. X ) ) = ( ( y .^ ( C .x. X ) ) ( +g ` W ) ( C .x. X ) ) )
51 46 47 48 50 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y + 1 ) .^ ( C .x. X ) ) = ( ( y .^ ( C .x. X ) ) ( +g ` W ) ( C .x. X ) ) )
52 51 adantr 
 |-  ( ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) /\ ( y .^ ( C .x. X ) ) = ( ( y E C ) .x. X ) ) -> ( ( y + 1 ) .^ ( C .x. X ) ) = ( ( y .^ ( C .x. X ) ) ( +g ` W ) ( C .x. X ) ) )
53 oveq1 
 |-  ( ( y .^ ( C .x. X ) ) = ( ( y E C ) .x. X ) -> ( ( y .^ ( C .x. X ) ) ( +g ` W ) ( C .x. X ) ) = ( ( ( y E C ) .x. X ) ( +g ` W ) ( C .x. X ) ) )
54 27 adantl 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> W e. LMod )
55 2 lmodring 
 |-  ( W e. LMod -> F e. Ring )
56 ringmnd 
 |-  ( F e. Ring -> F e. Mnd )
57 55 56 syl 
 |-  ( W e. LMod -> F e. Mnd )
58 57 ad2antll 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> F e. Mnd )
59 simprll 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> C e. K )
60 4 6 58 47 59 mulgnn0cld 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( y E C ) e. K )
61 29 adantl 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> X e. V )
62 eqid 
 |-  ( +g ` F ) = ( +g ` F )
63 1 49 2 3 4 62 lmodvsdir 
 |-  ( ( W e. LMod /\ ( ( y E C ) e. K /\ C e. K /\ X e. V ) ) -> ( ( ( y E C ) ( +g ` F ) C ) .x. X ) = ( ( ( y E C ) .x. X ) ( +g ` W ) ( C .x. X ) ) )
64 54 60 59 61 63 syl13anc 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( ( y E C ) ( +g ` F ) C ) .x. X ) = ( ( ( y E C ) .x. X ) ( +g ` W ) ( C .x. X ) ) )
65 4 6 62 mulgnn0p1 
 |-  ( ( F e. Mnd /\ y e. NN0 /\ C e. K ) -> ( ( y + 1 ) E C ) = ( ( y E C ) ( +g ` F ) C ) )
66 58 47 59 65 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y + 1 ) E C ) = ( ( y E C ) ( +g ` F ) C ) )
67 66 eqcomd 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y E C ) ( +g ` F ) C ) = ( ( y + 1 ) E C ) )
68 67 oveq1d 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( ( y E C ) ( +g ` F ) C ) .x. X ) = ( ( ( y + 1 ) E C ) .x. X ) )
69 64 68 eqtr3d 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( ( y E C ) .x. X ) ( +g ` W ) ( C .x. X ) ) = ( ( ( y + 1 ) E C ) .x. X ) )
70 53 69 sylan9eqr 
 |-  ( ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) /\ ( y .^ ( C .x. X ) ) = ( ( y E C ) .x. X ) ) -> ( ( y .^ ( C .x. X ) ) ( +g ` W ) ( C .x. X ) ) = ( ( ( y + 1 ) E C ) .x. X ) )
71 52 70 eqtrd 
 |-  ( ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) /\ ( y .^ ( C .x. X ) ) = ( ( y E C ) .x. X ) ) -> ( ( y + 1 ) .^ ( C .x. X ) ) = ( ( ( y + 1 ) E C ) .x. X ) )
72 71 exp31 
 |-  ( y e. NN0 -> ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( ( y .^ ( C .x. X ) ) = ( ( y E C ) .x. X ) -> ( ( y + 1 ) .^ ( C .x. X ) ) = ( ( ( y + 1 ) E C ) .x. X ) ) ) )
73 72 a2d 
 |-  ( y e. NN0 -> ( ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( y .^ ( C .x. X ) ) = ( ( y E C ) .x. X ) ) -> ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( ( y + 1 ) .^ ( C .x. X ) ) = ( ( ( y + 1 ) E C ) .x. X ) ) ) )
74 11 16 21 26 43 73 nn0ind 
 |-  ( N e. NN0 -> ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) ) )
75 74 exp4c 
 |-  ( N e. NN0 -> ( C e. K -> ( X e. V -> ( W e. LMod -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) ) ) ) )
76 75 3imp21 
 |-  ( ( C e. K /\ N e. NN0 /\ X e. V ) -> ( W e. LMod -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) ) )
77 76 impcom 
 |-  ( ( W e. LMod /\ ( C e. K /\ N e. NN0 /\ X e. V ) ) -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) )