Metamath Proof Explorer

Theorem gsummulsubdishift2

Description: Distribute a subtraction over an indexed sum, shift one of the resulting sums, and regroup terms. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummulsubdishift.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
gsummulsubdishift.p ⊢ + = ( +g ‘ 𝑅 )
gsummulsubdishift.m ⊢ − = ( -g ‘ 𝑅 )
gsummulsubdishift.t ⊢ · = ( .r ‘ 𝑅 )
gsummulsubdishift.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
gsummulsubdishift.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
gsummulsubdishift.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
gsummulsubdishift.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
gsummulsubdishift.d ⊢ ( 𝜑 → 𝐷 : ( 0 ... 𝑁 ) ⟶ 𝐵 )
gsummulsubdishift2.e ⊢ ( 𝜑 → 𝐸 = ( ( ( 𝐷 ‘ 0 ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) ) )
gsummulsubdishift2.f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 = ( ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) )
Assertion gsummulsubdishift2 ( 𝜑 → ( ( 𝑅 Σg 𝐷 ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )

Proof

Step Hyp Ref Expression
1 gsummulsubdishift.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 gsummulsubdishift.p ⊢ + = ( +g ‘ 𝑅 )
3 gsummulsubdishift.m ⊢ − = ( -g ‘ 𝑅 )
4 gsummulsubdishift.t ⊢ · = ( .r ‘ 𝑅 )
5 gsummulsubdishift.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 gsummulsubdishift.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 gsummulsubdishift.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
8 gsummulsubdishift.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9 gsummulsubdishift.d ⊢ ( 𝜑 → 𝐷 : ( 0 ... 𝑁 ) ⟶ 𝐵 )
10 gsummulsubdishift2.e ⊢ ( 𝜑 → 𝐸 = ( ( ( 𝐷 ‘ 0 ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) ) )
11 gsummulsubdishift2.f ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 = ( ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) )
12 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
13 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
14 5 ringcmnd ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
15 ovexd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
16 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
17 fvexd ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ V )
18 9 16 17 fdmfifsupp ⊢ ( 𝜑 → 𝐷 finSupp ( 0g ‘ 𝑅 ) )
19 1 13 14 15 9 18 gsumcl ⊢ ( 𝜑 → ( 𝑅 Σg 𝐷 ) ∈ 𝐵 )
20 5 ringgrpd ⊢ ( 𝜑 → 𝑅 ∈ Grp )
21 1 3 20 7 6 grpsubcld ⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) ∈ 𝐵 )
22 1 4 12 5 19 21 ringmneg2 ⊢ ( 𝜑 → ( ( 𝑅 Σg 𝐷 ) · ( ( invg ‘ 𝑅 ) ‘ ( 𝐶 − 𝐴 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( 𝑅 Σg 𝐷 ) · ( 𝐶 − 𝐴 ) ) ) )
23 1 3 12 grpinvsub ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐶 ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( ( invg ‘ 𝑅 ) ‘ ( 𝐶 − 𝐴 ) ) = ( 𝐴 − 𝐶 ) )
24 20 7 6 23 syl3anc ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 𝐶 − 𝐴 ) ) = ( 𝐴 − 𝐶 ) )
25 24 oveq2d ⊢ ( 𝜑 → ( ( 𝑅 Σg 𝐷 ) · ( ( invg ‘ 𝑅 ) ‘ ( 𝐶 − 𝐴 ) ) ) = ( ( 𝑅 Σg 𝐷 ) · ( 𝐴 − 𝐶 ) ) )
26 10 fveq2d ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( 𝐷 ‘ 0 ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) ) ) )
27 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
28 8 27 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
29 9 28 ffvelcdmd ⊢ ( 𝜑 → ( 𝐷 ‘ 0 ) ∈ 𝐵 )
30 1 4 5 29 6 ringcld ⊢ ( 𝜑 → ( ( 𝐷 ‘ 0 ) · 𝐴 ) ∈ 𝐵 )
31 nn0fz0 ⊢ ( 𝑁 ∈ ℕ0 ↔ 𝑁 ∈ ( 0 ... 𝑁 ) )
32 8 31 sylib ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ... 𝑁 ) )
33 9 32 ffvelcdmd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑁 ) ∈ 𝐵 )
34 1 4 5 33 7 ringcld ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) ∈ 𝐵 )
35 1 3 12 grpinvsub ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝐷 ‘ 0 ) · 𝐴 ) ∈ 𝐵 ∧ ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) ∈ 𝐵 ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( 𝐷 ‘ 0 ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) ) ) = ( ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) − ( ( 𝐷 ‘ 0 ) · 𝐴 ) ) )
36 20 30 34 35 syl3anc ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( ( ( 𝐷 ‘ 0 ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) ) ) = ( ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) − ( ( 𝐷 ‘ 0 ) · 𝐴 ) ) )
37 26 36 eqtrd ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) = ( ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) − ( ( 𝐷 ‘ 0 ) · 𝐴 ) ) )
38 11 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) = ( ( invg ‘ 𝑅 ) ‘ ( ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) )
39 20 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑅 ∈ Grp )
40 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑅 ∈ Ring )
41 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐷 : ( 0 ... 𝑁 ) ⟶ 𝐵 )
42 fzofzp1 ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑘 + 1 ) ∈ ( 0 ... 𝑁 ) )
44 41 43 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ ( 𝑘 + 1 ) ) ∈ 𝐵 )
45 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ 𝐵 )
46 1 4 40 44 45 ringcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) ∈ 𝐵 )
47 fzossfz ⊢ ( 0 ..^ 𝑁 ) ⊆ ( 0 ... 𝑁 )
48 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( 0 ..^ 𝑁 ) )
49 47 48 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
50 41 49 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐷 ‘ 𝑘 ) ∈ 𝐵 )
51 7 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐶 ∈ 𝐵 )
52 1 4 40 50 51 ringcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ∈ 𝐵 )
53 1 3 12 grpinvsub ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) ∈ 𝐵 ∧ ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ∈ 𝐵 ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) = ( ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) − ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) ) )
54 39 46 52 53 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ) = ( ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) − ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) ) )
55 38 54 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) = ( ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) − ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) ) )
56 1 2 3 4 5 7 6 8 9 37 55 gsummulsubdishift1 ⊢ ( 𝜑 → ( ( 𝑅 Σg 𝐷 ) · ( 𝐶 − 𝐴 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) + ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ) )
57 56 fveq2d ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( ( 𝑅 Σg 𝐷 ) · ( 𝐶 − 𝐴 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) + ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ) ) )
58 5 ringabld ⊢ ( 𝜑 → 𝑅 ∈ Abel )
59 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
60 59 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
61 1 3 39 46 52 grpsubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( 𝐷 ‘ ( 𝑘 + 1 ) ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑘 ) · 𝐶 ) ) ∈ 𝐵 )
62 11 61 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 ∈ 𝐵 )
63 1 12 39 62 grpinvcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ∈ 𝐵 )
64 63 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ∈ 𝐵 )
65 1 14 60 64 gsummptcl ⊢ ( 𝜑 → ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ∈ 𝐵 )
66 1 3 20 30 34 grpsubcld ⊢ ( 𝜑 → ( ( ( 𝐷 ‘ 0 ) · 𝐴 ) − ( ( 𝐷 ‘ 𝑁 ) · 𝐶 ) ) ∈ 𝐵 )
67 10 66 eqeltrd ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
68 1 12 20 67 grpinvcld ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ∈ 𝐵 )
69 1 2 12 ablinvadd ⊢ ( ( 𝑅 ∈ Abel ∧ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ∈ 𝐵 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ∈ 𝐵 ) → ( ( invg ‘ 𝑅 ) ‘ ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) + ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ) + ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ) ) )
70 58 65 68 69 syl3anc ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) + ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ) ) = ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ) + ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ) ) )
71 63 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) : ( 0 ..^ 𝑁 ) ⟶ 𝐵 )
72 71 60 17 fidmfisupp ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) finSupp ( 0g ‘ 𝑅 ) )
73 1 13 12 58 60 71 72 gsuminv ⊢ ( 𝜑 → ( 𝑅 Σg ( ( invg ‘ 𝑅 ) ∘ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ) )
74 1 12 grpinvf ⊢ ( 𝑅 ∈ Grp → ( invg ‘ 𝑅 ) : 𝐵 ⟶ 𝐵 )
75 20 74 syl ⊢ ( 𝜑 → ( invg ‘ 𝑅 ) : 𝐵 ⟶ 𝐵 )
76 75 63 cofmpt ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ∘ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) )
77 1 12 39 62 grpinvinvd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) = 𝐹 )
78 77 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) )
79 76 78 eqtrd ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ∘ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) )
80 79 oveq2d ⊢ ( 𝜑 → ( 𝑅 Σg ( ( invg ‘ 𝑅 ) ∘ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) )
81 73 80 eqtr3d ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ) = ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) )
82 1 12 20 67 grpinvinvd ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ) = 𝐸 )
83 81 82 oveq12d ⊢ ( 𝜑 → ( ( ( invg ‘ 𝑅 ) ‘ ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( invg ‘ 𝑅 ) ‘ 𝐹 ) ) ) ) + ( ( invg ‘ 𝑅 ) ‘ ( ( invg ‘ 𝑅 ) ‘ 𝐸 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )
84 57 70 83 3eqtrd ⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( ( 𝑅 Σg 𝐷 ) · ( 𝐶 − 𝐴 ) ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )
85 22 25 84 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑅 Σg 𝐷 ) · ( 𝐴 − 𝐶 ) ) = ( ( 𝑅 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ 𝐹 ) ) + 𝐸 ) )