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

Proof

Step Hyp Ref Expression
1 lmodvsmmulgdi.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lmodvsmmulgdi.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 lmodvsmmulgdi.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
4 lmodvsmmulgdi.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lmodvsmmulgdi.p ⊢ ↑ = ( .g ‘ 𝑊 )
6 lmodvsmmulgdi.e ⊢ 𝐸 = ( .g ‘ 𝐹 )
7 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( 0 ↑ ( 𝐶 · 𝑋 ) ) )
8 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 𝐸 𝐶 ) = ( 0 𝐸 𝐶 ) )
9 8 oveq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) = ( ( 0 𝐸 𝐶 ) · 𝑋 ) )
10 7 9 eqeq12d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ↔ ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 0 𝐸 𝐶 ) · 𝑋 ) ) )
11 10 imbi2d ⊢ ( 𝑥 = 0 → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ) ↔ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 0 𝐸 𝐶 ) · 𝑋 ) ) ) )
12 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) )
13 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐸 𝐶 ) = ( 𝑦 𝐸 𝐶 ) )
14 13 oveq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) )
15 12 14 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ↔ ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) )
16 15 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ) ↔ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) ) )
17 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) )
18 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 𝐸 𝐶 ) = ( ( 𝑦 + 1 ) 𝐸 𝐶 ) )
19 18 oveq1d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) )
20 17 19 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ↔ ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) )
21 20 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ) ↔ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) ) )
22 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) )
23 oveq1 ⊢ ( 𝑥 = 𝑁 → ( 𝑥 𝐸 𝐶 ) = ( 𝑁 𝐸 𝐶 ) )
24 23 oveq1d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) )
25 22 24 eqeq12d ⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ↔ ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) )
26 25 imbi2d ⊢ ( 𝑥 = 𝑁 → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑥 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑥 𝐸 𝐶 ) · 𝑋 ) ) ↔ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) ) )
27 simpr ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝑊 ∈ LMod )
28 simpr ⊢ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
29 28 adantr ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝑋 ∈ 𝑉 )
30 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
31 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
32 1 2 3 30 31 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) )
33 27 29 32 syl2anc ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 0g ‘ 𝐹 ) · 𝑋 ) = ( 0g ‘ 𝑊 ) )
34 simpl ⊢ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → 𝐶 ∈ 𝐾 )
35 34 adantr ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → 𝐶 ∈ 𝐾 )
36 4 30 6 mulg0 ⊢ ( 𝐶 ∈ 𝐾 → ( 0 𝐸 𝐶 ) = ( 0g ‘ 𝐹 ) )
37 35 36 syl ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 𝐸 𝐶 ) = ( 0g ‘ 𝐹 ) )
38 37 oveq1d ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 0 𝐸 𝐶 ) · 𝑋 ) = ( ( 0g ‘ 𝐹 ) · 𝑋 ) )
39 1 2 3 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐶 · 𝑋 ) ∈ 𝑉 )
40 27 35 29 39 syl3anc ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝐶 · 𝑋 ) ∈ 𝑉 )
41 1 31 5 mulg0 ⊢ ( ( 𝐶 · 𝑋 ) ∈ 𝑉 → ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( 0g ‘ 𝑊 ) )
42 40 41 syl ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( 0g ‘ 𝑊 ) )
43 33 38 42 3eqtr4rd ⊢ ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 0 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 0 𝐸 𝐶 ) · 𝑋 ) )
44 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
45 grpmnd ⊢ ( 𝑊 ∈ Grp → 𝑊 ∈ Mnd )
46 44 45 syl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Mnd )
47 46 ad2antll ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑊 ∈ Mnd )
48 simpl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑦 ∈ ℕ0 )
49 40 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝐶 · 𝑋 ) ∈ 𝑉 )
50 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
51 1 5 50 mulgnn0p1 ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ ( 𝐶 · 𝑋 ) ∈ 𝑉 ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) )
52 47 48 49 51 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) )
53 52 adantr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) )
54 oveq1 ⊢ ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) → ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) )
55 27 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑊 ∈ LMod )
56 2 lmodring ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Ring )
57 ringmnd ⊢ ( 𝐹 ∈ Ring → 𝐹 ∈ Mnd )
58 56 57 syl ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Mnd )
59 58 ad2antll ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝐹 ∈ Mnd )
60 simprll ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝐶 ∈ 𝐾 )
61 4 6 mulgnn0cl ⊢ ( ( 𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ 𝐾 ) → ( 𝑦 𝐸 𝐶 ) ∈ 𝐾 )
62 59 48 60 61 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( 𝑦 𝐸 𝐶 ) ∈ 𝐾 )
63 29 adantl ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → 𝑋 ∈ 𝑉 )
64 eqid ⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
65 1 50 2 3 4 64 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 𝐸 𝐶 ) ∈ 𝐾 ∧ 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) · 𝑋 ) = ( ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) )
66 55 62 60 63 65 syl13anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) · 𝑋 ) = ( ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) )
67 4 6 64 mulgnn0p1 ⊢ ( ( 𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ 𝐾 ) → ( ( 𝑦 + 1 ) 𝐸 𝐶 ) = ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) )
68 59 48 60 67 syl3anc ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 + 1 ) 𝐸 𝐶 ) = ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) )
69 68 eqcomd ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) = ( ( 𝑦 + 1 ) 𝐸 𝐶 ) )
70 69 oveq1d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝐶 ) ( +g ‘ 𝐹 ) 𝐶 ) · 𝑋 ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) )
71 66 70 eqtr3d ⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) → ( ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) )
72 54 71 sylan9eqr ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) → ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) ( +g ‘ 𝑊 ) ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) )
73 53 72 eqtrd ⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) ) ∧ ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) )
74 73 exp31 ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) ) )
75 74 a2d ⊢ ( 𝑦 ∈ ℕ0 → ( ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑦 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑦 𝐸 𝐶 ) · 𝑋 ) ) → ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( ( 𝑦 + 1 ) ↑ ( 𝐶 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) 𝐸 𝐶 ) · 𝑋 ) ) ) )
76 11 16 21 26 43 75 nn0ind ⊢ ( 𝑁 ∈ ℕ0 → ( ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ LMod ) → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) )
77 76 exp4c ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐶 ∈ 𝐾 → ( 𝑋 ∈ 𝑉 → ( 𝑊 ∈ LMod → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) ) ) )
78 77 3imp21 ⊢ ( ( 𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ∈ LMod → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) ) )
79 78 impcom ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) ) → ( 𝑁 ↑ ( 𝐶 · 𝑋 ) ) = ( ( 𝑁 𝐸 𝐶 ) · 𝑋 ) )