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 grpmnd 
 |-  ( W e. Grp -> W e. Mnd )
46 44 45 syl 
 |-  ( W e. LMod -> W e. Mnd )
47 46 ad2antll 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> W e. Mnd )
48 simpl 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> y e. NN0 )
49 40 adantl 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( C .x. X ) e. V )
50 eqid 
 |-  ( +g ` W ) = ( +g ` W )
51 1 5 50 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 ) ) )
52 47 48 49 51 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 ) ) )
53 52 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 ) ) )
54 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 ) ) )
55 27 adantl 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> W e. LMod )
56 2 lmodring 
 |-  ( W e. LMod -> F e. Ring )
57 ringmnd 
 |-  ( F e. Ring -> F e. Mnd )
58 56 57 syl 
 |-  ( W e. LMod -> F e. Mnd )
59 58 ad2antll 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> F e. Mnd )
60 simprll 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> C e. K )
61 4 6 mulgnn0cl 
 |-  ( ( F e. Mnd /\ y e. NN0 /\ C e. K ) -> ( y E C ) e. K )
62 59 48 60 61 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( y E C ) e. K )
63 29 adantl 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> X e. V )
64 eqid 
 |-  ( +g ` F ) = ( +g ` F )
65 1 50 2 3 4 64 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 ) ) )
66 55 62 60 63 65 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 ) ) )
67 4 6 64 mulgnn0p1 
 |-  ( ( F e. Mnd /\ y e. NN0 /\ C e. K ) -> ( ( y + 1 ) E C ) = ( ( y E C ) ( +g ` F ) C ) )
68 59 48 60 67 syl3anc 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y + 1 ) E C ) = ( ( y E C ) ( +g ` F ) C ) )
69 68 eqcomd 
 |-  ( ( y e. NN0 /\ ( ( C e. K /\ X e. V ) /\ W e. LMod ) ) -> ( ( y E C ) ( +g ` F ) C ) = ( ( y + 1 ) E C ) )
70 69 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 ) )
71 66 70 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 ) )
72 54 71 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 ) )
73 53 72 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 ) )
74 73 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 ) ) ) )
75 74 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 ) ) ) )
76 11 16 21 26 43 75 nn0ind 
 |-  ( N e. NN0 -> ( ( ( C e. K /\ X e. V ) /\ W e. LMod ) -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) ) )
77 76 exp4c 
 |-  ( N e. NN0 -> ( C e. K -> ( X e. V -> ( W e. LMod -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) ) ) ) )
78 77 3imp21 
 |-  ( ( C e. K /\ N e. NN0 /\ X e. V ) -> ( W e. LMod -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) ) )
79 78 impcom 
 |-  ( ( W e. LMod /\ ( C e. K /\ N e. NN0 /\ X e. V ) ) -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) )