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