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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lmodvsmdi.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lmodvsmdi.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lmodvsmdi.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lmodvsmdi.p ⊢ ↑ = ( .g ‘ 𝑊 )
lmodvsmdi.e ⊢ 𝐸 = ( .g ‘ 𝐹 )
Assertion lmodvsmdi ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) )

Proof

Step Hyp Ref Expression
1 lmodvsmdi.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodvsmdi.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 lmodvsmdi.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 lmodvsmdi.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lmodvsmdi.p ⊢ ↑ = ( .g ‘ 𝑊 )
6 lmodvsmdi.e ⊢ 𝐸 = ( .g ‘ 𝐹 )
7 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 𝑋 ) = ( 0 ↑ 𝑋 ) )
8 7 oveq2d ⊢ ( 𝑥 = 0 → ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( 𝑅 · ( 0 ↑ 𝑋 ) ) )
9 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 𝐸 𝑅 ) = ( 0 𝐸 𝑅 ) )
10 9 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) = ( ( 0 𝐸 𝑅 ) · 𝑋 ) )
11 8 10 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) ↔ ( 𝑅 · ( 0 ↑ 𝑋 ) ) = ( ( 0 𝐸 𝑅 ) · 𝑋 ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 0 → ( ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) ) ↔ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 0 ↑ 𝑋 ) ) = ( ( 0 𝐸 𝑅 ) · 𝑋 ) ) ) )
13 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 𝑋 ) = ( 𝑦 ↑ 𝑋 ) )
14 13 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) )
15 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐸 𝑅 ) = ( 𝑦 𝐸 𝑅 ) )
16 15 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) )
17 14 16 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) ↔ ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ) )
18 17 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) ) ↔ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ) ) )
19 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ 𝑋 ) = ( ( 𝑦 + 1 ) ↑ 𝑋 ) )
20 19 oveq2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) )
21 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 𝐸 𝑅 ) = ( ( 𝑦 + 1 ) 𝐸 𝑅 ) )
22 21 oveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) )
23 20 22 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) ↔ ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) ) )
24 23 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) ) ↔ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) ) ) )
25 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) )
26 25 oveq2d ⊢ ( 𝑥 = 𝑁 → ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) )
27 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 𝐸 𝑅 ) = ( 𝑁 𝐸 𝑅 ) )
28 27 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) )
29 26 28 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) ↔ ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) ) )
30 29 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 𝑥 ↑ 𝑋 ) ) = ( ( 𝑥 𝐸 𝑅 ) · 𝑋 ) ) ↔ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) ) ) )
31 simpr ⊢ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
32 31 adantr ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝑋 ∈ 𝑉 )
33 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
34 1 33 5 mulg0 ⊢ ( 𝑋 ∈ 𝑉 → ( 0 ↑ 𝑋 ) = ( 0g ‘ 𝑊 ) )
35 32 34 syl ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 ↑ 𝑋 ) = ( 0g ‘ 𝑊 ) )
36 35 oveq2d ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 0 ↑ 𝑋 ) ) = ( 𝑅 · ( 0g ‘ 𝑊 ) ) )
37 simpl ⊢ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑅 ∈ 𝐾 )
38 37 anim1i ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 ∈ 𝐾 ∧ 𝑊 ∈ LMod ) )
39 38 ancomd ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) )
40 2 3 4 33 lmodvs0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑅 ∈ 𝐾 ) → ( 𝑅 · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
41 39 40 syl ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 0g ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
42 31 anim1i ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑋 ∈ 𝑉 ∧ 𝑊 ∈ LMod ) )
43 42 ancomd ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) )
44 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
45 1 2 3 44 33 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) )
46 43 45 syl ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) )
47 37 adantr ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝑅 ∈ 𝐾 )
48 4 44 6 mulg0 ⊢ ( 𝑅 ∈ 𝐾 → ( 0 𝐸 𝑅 ) = ( 0g ‘ 𝐹 ) )
49 48 eqcomd ⊢ ( 𝑅 ∈ 𝐾 → ( 0g ‘ 𝐹 ) = ( 0 𝐸 𝑅 ) )
50 47 49 syl ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0g ‘ 𝐹 ) = ( 0 𝐸 𝑅 ) )
51 50 oveq1d ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( ( 0 𝐸 𝑅 ) · 𝑋 ) )
52 41 46 51 3eqtr2d ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 0g ‘ 𝑊 ) ) = ( ( 0 𝐸 𝑅 ) · 𝑋 ) )
53 36 52 eqtrd ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 0 ↑ 𝑋 ) ) = ( ( 0 𝐸 𝑅 ) · 𝑋 ) )
54 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
55 54 grpmndd ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Mnd )
56 55 ad2antll ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑊 ∈ Mnd )
57 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑦 ∈ ℕ0 )
58 32 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑋 ∈ 𝑉 )
59 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
60 1 5 59 mulgnn0p1 ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 + 1 ) ↑ 𝑋 ) = ( ( 𝑦 ↑ 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) )
61 56 57 58 60 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 + 1 ) ↑ 𝑋 ) = ( ( 𝑦 ↑ 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) )
62 61 oveq2d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) = ( 𝑅 · ( ( 𝑦 ↑ 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) ) )
63 simpr ⊢ ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝑊 ∈ LMod )
64 63 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑊 ∈ LMod )
65 simprll ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑅 ∈ 𝐾 )
66 1 5 mulgnn0cl ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑦 ↑ 𝑋 ) ∈ 𝑉 )
67 56 57 58 66 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝑦 ↑ 𝑋 ) ∈ 𝑉 )
68 1 59 2 3 4 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ ( 𝑦 ↑ 𝑋 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑅 · ( ( 𝑦 ↑ 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) ) = ( ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) )
69 64 65 67 58 68 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝑅 · ( ( 𝑦 ↑ 𝑋 ) ( +g ‘ 𝑊 ) 𝑋 ) ) = ( ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) )
70 62 69 eqtrd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) = ( ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) )
71 oveq1 ⊢ ( ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) → ( ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) = ( ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) )
72 70 71 sylan9eq ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ) → ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) = ( ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) )
73 2 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )
74 73 grpmndd ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Mnd )
75 74 ad2antll ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝐹 ∈ Mnd )
76 4 6 mulgnn0cl ⊢ ( ( 𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑅 ∈ 𝐾 ) → ( 𝑦 𝐸 𝑅 ) ∈ 𝐾 )
77 75 57 65 76 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝑦 𝐸 𝑅 ) ∈ 𝐾 )
78 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
79 1 59 2 3 4 78 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 𝐸 𝑅 ) ∈ 𝐾 ∧ 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 𝑦 𝐸 𝑅 ) ( +g ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) )
80 64 77 65 58 79 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝑅 ) ( +g ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) )
81 4 6 78 mulgnn0p1 ⊢ ( ( 𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑅 ∈ 𝐾 ) → ( ( 𝑦 + 1 ) 𝐸 𝑅 ) = ( ( 𝑦 𝐸 𝑅 ) ( +g ‘ 𝐹 ) 𝑅 ) )
82 75 57 65 81 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 + 1 ) 𝐸 𝑅 ) = ( ( 𝑦 𝐸 𝑅 ) ( +g ‘ 𝐹 ) 𝑅 ) )
83 82 eqcomd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 𝐸 𝑅 ) ( +g ‘ 𝐹 ) 𝑅 ) = ( ( 𝑦 + 1 ) 𝐸 𝑅 ) )
84 83 oveq1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝑅 ) ( +g ‘ 𝐹 ) 𝑅 ) · 𝑋 ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) )
85 80 84 eqtr3d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) )
86 85 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ) → ( ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝑅 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) )
87 72 86 eqtrd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ) → ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) )
88 87 exp31 ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) → ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) ) ) )
89 88 a2d ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 𝑦 ↑ 𝑋 ) ) = ( ( 𝑦 𝐸 𝑅 ) · 𝑋 ) ) → ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( ( 𝑦 + 1 ) ↑ 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝑅 ) · 𝑋 ) ) ) )
90 12 18 24 30 53 89 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝑅 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) ) )
91 90 exp4c ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑅 ∈ 𝐾 → ( 𝑋 ∈ 𝑉 → ( 𝑊 ∈ LMod → ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) ) ) ) )
92 91 com12 ⊢ ( 𝑅 ∈ 𝐾 → ( 𝑁 ∈ ℕ0 → ( 𝑋 ∈ 𝑉 → ( 𝑊 ∈ LMod → ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) ) ) ) )
93 92 3imp ⊢ ( ( 𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ∈ LMod → ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) ) )
94 93 impcom ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑅 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑅 · ( 𝑁 ↑ 𝑋 ) ) = ( ( 𝑁 𝐸 𝑅 ) · 𝑋 ) )