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 · ˙ = W
lmodvsmmulgdi.k K = Base F
lmodvsmmulgdi.p × ˙ = W
lmodvsmmulgdi.e E = F
Assertion lmodvsmmulgdi W LMod C K N 0 X V N × ˙ C · ˙ X = N E C · ˙ X

Proof

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