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	$⊢ B = {Base}_{R}$
	gsummulsubdishift.p	$⊢ \underset{˙}{+} = +_{R}$
	gsummulsubdishift.m	$⊢ \underset{˙}{-} = -_{R}$
	gsummulsubdishift.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	gsummulsubdishift.r	$⊢ φ \to R \in Ring$
	gsummulsubdishift.a	$⊢ φ \to A \in B$
	gsummulsubdishift.c	$⊢ φ \to C \in B$
	gsummulsubdishift.n	$⊢ φ \to N \in ℕ_{0}$
	gsummulsubdishift.d	$⊢ φ \to D : (0 \dots N) ⟶ B$
	gsummulsubdishift2.e	$⊢ φ \to E = (D (0) \underset{˙}{\cdot} A) \underset{˙}{-} (D (N) \underset{˙}{\cdot} C)$
	gsummulsubdishift2.f	$⊢ (φ \land k \in (0 ..^N)) \to F = (D (k + 1) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k) \underset{˙}{\cdot} C)$
Assertion	gsummulsubdishift2	$⊢ φ \to (\sum_{R}, D) \underset{˙}{\cdot} (A \underset{˙}{-} C) = (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E$

Proof

Step	Hyp	Ref	Expression
1		gsummulsubdishift.b	$⊢ B = {Base}_{R}$
2		gsummulsubdishift.p	$⊢ \underset{˙}{+} = +_{R}$
3		gsummulsubdishift.m	$⊢ \underset{˙}{-} = -_{R}$
4		gsummulsubdishift.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
5		gsummulsubdishift.r	$⊢ φ \to R \in Ring$
6		gsummulsubdishift.a	$⊢ φ \to A \in B$
7		gsummulsubdishift.c	$⊢ φ \to C \in B$
8		gsummulsubdishift.n	$⊢ φ \to N \in ℕ_{0}$
9		gsummulsubdishift.d	$⊢ φ \to D : (0 \dots N) ⟶ B$
10		gsummulsubdishift2.e	$⊢ φ \to E = (D (0) \underset{˙}{\cdot} A) \underset{˙}{-} (D (N) \underset{˙}{\cdot} C)$
11		gsummulsubdishift2.f	$⊢ (φ \land k \in (0 ..^N)) \to F = (D (k + 1) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k) \underset{˙}{\cdot} C)$
12		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
13		eqid	$⊢ 0_{R} = 0_{R}$
14	5	ringcmnd	$⊢ φ \to R \in CMnd$
15		ovexd	$⊢ φ \to (0 \dots N) \in V$
16		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
17		fvexd	$⊢ φ \to 0_{R} \in V$
18	9 16 17	fdmfifsupp	$⊢ φ \to {finSupp}_{0_{R}} (D)$
19	1 13 14 15 9 18	gsumcl	$⊢ φ \to \sum_{R} D \in B$
20	5	ringgrpd	$⊢ φ \to R \in Grp$
21	1 3 20 7 6	grpsubcld	$⊢ φ \to C \underset{˙}{-} A \in B$
22	1 4 12 5 19 21	ringmneg2	$⊢ φ \to (\sum_{R}, D) \underset{˙}{\cdot} {inv}_{g} (R) (C \underset{˙}{-} A) = {inv}_{g} (R) ((\sum_{R}, D) \underset{˙}{\cdot} (C \underset{˙}{-} A))$
23	1 3 12	grpinvsub	$⊢ (R \in Grp \land C \in B \land A \in B) \to {inv}_{g} (R) (C \underset{˙}{-} A) = A \underset{˙}{-} C$
24	20 7 6 23	syl3anc	$⊢ φ \to {inv}_{g} (R) (C \underset{˙}{-} A) = A \underset{˙}{-} C$
25	24	oveq2d	$⊢ φ \to (\sum_{R}, D) \underset{˙}{\cdot} {inv}_{g} (R) (C \underset{˙}{-} A) = (\sum_{R}, D) \underset{˙}{\cdot} (A \underset{˙}{-} C)$
26	10	fveq2d	$⊢ φ \to {inv}_{g} (R) (E) = {inv}_{g} (R) ((D (0) \underset{˙}{\cdot} A) \underset{˙}{-} (D (N) \underset{˙}{\cdot} C))$
27		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
28	8 27	syl	$⊢ φ \to 0 \in (0 \dots N)$
29	9 28	ffvelcdmd	$⊢ φ \to D (0) \in B$
30	1 4 5 29 6	ringcld	$⊢ φ \to D (0) \underset{˙}{\cdot} A \in B$
31		nn0fz0	$⊢ N \in ℕ_{0} \leftrightarrow N \in (0 \dots N)$
32	8 31	sylib	$⊢ φ \to N \in (0 \dots N)$
33	9 32	ffvelcdmd	$⊢ φ \to D (N) \in B$
34	1 4 5 33 7	ringcld	$⊢ φ \to D (N) \underset{˙}{\cdot} C \in B$
35	1 3 12	grpinvsub	$⊢ (R \in Grp \land D (0) \underset{˙}{\cdot} A \in B \land D (N) \underset{˙}{\cdot} C \in B) \to {inv}_{g} (R) ((D (0) \underset{˙}{\cdot} A) \underset{˙}{-} (D (N) \underset{˙}{\cdot} C)) = (D (N) \underset{˙}{\cdot} C) \underset{˙}{-} (D (0) \underset{˙}{\cdot} A)$
36	20 30 34 35	syl3anc	$⊢ φ \to {inv}_{g} (R) ((D (0) \underset{˙}{\cdot} A) \underset{˙}{-} (D (N) \underset{˙}{\cdot} C)) = (D (N) \underset{˙}{\cdot} C) \underset{˙}{-} (D (0) \underset{˙}{\cdot} A)$
37	26 36	eqtrd	$⊢ φ \to {inv}_{g} (R) (E) = (D (N) \underset{˙}{\cdot} C) \underset{˙}{-} (D (0) \underset{˙}{\cdot} A)$
38	11	fveq2d	$⊢ (φ \land k \in (0 ..^N)) \to {inv}_{g} (R) (F) = {inv}_{g} (R) ((D (k + 1) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k) \underset{˙}{\cdot} C))$
39	20	adantr	$⊢ (φ \land k \in (0 ..^N)) \to R \in Grp$
40	5	adantr	$⊢ (φ \land k \in (0 ..^N)) \to R \in Ring$
41	9	adantr	$⊢ (φ \land k \in (0 ..^N)) \to D : (0 \dots N) ⟶ B$
42		fzofzp1	$⊢ k \in (0 ..^N) \to k + 1 \in (0 \dots N)$
43	42	adantl	$⊢ (φ \land k \in (0 ..^N)) \to k + 1 \in (0 \dots N)$
44	41 43	ffvelcdmd	$⊢ (φ \land k \in (0 ..^N)) \to D (k + 1) \in B$
45	6	adantr	$⊢ (φ \land k \in (0 ..^N)) \to A \in B$
46	1 4 40 44 45	ringcld	$⊢ (φ \land k \in (0 ..^N)) \to D (k + 1) \underset{˙}{\cdot} A \in B$
47		fzossfz	$⊢ (0 ..^N) \subseteq (0 \dots N)$
48		simpr	$⊢ (φ \land k \in (0 ..^N)) \to k \in (0 ..^N)$
49	47 48	sselid	$⊢ (φ \land k \in (0 ..^N)) \to k \in (0 \dots N)$
50	41 49	ffvelcdmd	$⊢ (φ \land k \in (0 ..^N)) \to D (k) \in B$
51	7	adantr	$⊢ (φ \land k \in (0 ..^N)) \to C \in B$
52	1 4 40 50 51	ringcld	$⊢ (φ \land k \in (0 ..^N)) \to D (k) \underset{˙}{\cdot} C \in B$
53	1 3 12	grpinvsub	$⊢ (R \in Grp \land D (k + 1) \underset{˙}{\cdot} A \in B \land D (k) \underset{˙}{\cdot} C \in B) \to {inv}_{g} (R) ((D (k + 1) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k) \underset{˙}{\cdot} C)) = (D (k) \underset{˙}{\cdot} C) \underset{˙}{-} (D (k + 1) \underset{˙}{\cdot} A)$
54	39 46 52 53	syl3anc	$⊢ (φ \land k \in (0 ..^N)) \to {inv}_{g} (R) ((D (k + 1) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k) \underset{˙}{\cdot} C)) = (D (k) \underset{˙}{\cdot} C) \underset{˙}{-} (D (k + 1) \underset{˙}{\cdot} A)$
55	38 54	eqtrd	$⊢ (φ \land k \in (0 ..^N)) \to {inv}_{g} (R) (F) = (D (k) \underset{˙}{\cdot} C) \underset{˙}{-} (D (k + 1) \underset{˙}{\cdot} A)$
56	1 2 3 4 5 7 6 8 9 37 55	gsummulsubdishift1	$⊢ φ \to (\sum_{R}, D) \underset{˙}{\cdot} (C \underset{˙}{-} A) = (\underset{k \in (0 ..^N)}{\sum_{R}}, {inv}_{g} (R) (F)) \underset{˙}{+} {inv}_{g} (R) (E)$
57	56	fveq2d	$⊢ φ \to {inv}_{g} (R) ((\sum_{R}, D) \underset{˙}{\cdot} (C \underset{˙}{-} A)) = {inv}_{g} (R) ((\underset{k \in (0 ..^N)}{\sum_{R}}, {inv}_{g} (R) (F)) \underset{˙}{+} {inv}_{g} (R) (E))$
58	5	ringabld	$⊢ φ \to R \in Abel$
59		fzofi	$⊢ (0 ..^N) \in Fin$
60	59	a1i	$⊢ φ \to (0 ..^N) \in Fin$
61	1 3 39 46 52	grpsubcld	$⊢ (φ \land k \in (0 ..^N)) \to (D (k + 1) \underset{˙}{\cdot} A) \underset{˙}{-} (D (k) \underset{˙}{\cdot} C) \in B$
62	11 61	eqeltrd	$⊢ (φ \land k \in (0 ..^N)) \to F \in B$
63	1 12 39 62	grpinvcld	$⊢ (φ \land k \in (0 ..^N)) \to {inv}_{g} (R) (F) \in B$
64	63	ralrimiva	$⊢ φ \to \forall k \in (0 ..^N) {inv}_{g} (R) (F) \in B$
65	1 14 60 64	gsummptcl	$⊢ φ \to \underset{k \in (0 ..^N)}{\sum_{R}} {inv}_{g} (R) (F) \in B$
66	1 3 20 30 34	grpsubcld	$⊢ φ \to (D (0) \underset{˙}{\cdot} A) \underset{˙}{-} (D (N) \underset{˙}{\cdot} C) \in B$
67	10 66	eqeltrd	$⊢ φ \to E \in B$
68	1 12 20 67	grpinvcld	$⊢ φ \to {inv}_{g} (R) (E) \in B$
69	1 2 12	ablinvadd	$⊢ (R \in Abel \land \underset{k \in (0 ..^N)}{\sum_{R}} {inv}_{g} (R) (F) \in B \land {inv}_{g} (R) (E) \in B) \to {inv}_{g} (R) ((\underset{k \in (0 ..^N)}{\sum_{R}}, {inv}_{g} (R) (F)) \underset{˙}{+} {inv}_{g} (R) (E)) = {inv}_{g} (R) (\underset{k \in (0 ..^N)}{\sum_{R}} {inv}_{g} (R) (F)) \underset{˙}{+} {inv}_{g} (R) ({inv}_{g} (R) (E))$
70	58 65 68 69	syl3anc	$⊢ φ \to {inv}_{g} (R) ((\underset{k \in (0 ..^N)}{\sum_{R}}, {inv}_{g} (R) (F)) \underset{˙}{+} {inv}_{g} (R) (E)) = {inv}_{g} (R) (\underset{k \in (0 ..^N)}{\sum_{R}} {inv}_{g} (R) (F)) \underset{˙}{+} {inv}_{g} (R) ({inv}_{g} (R) (E))$
71	63	fmpttd	$⊢ φ \to (k \in (0 ..^N) ⟼ {inv}_{g} (R) (F)) : (0 ..^N) ⟶ B$
72	71 60 17	fidmfisupp	$⊢ φ \to {finSupp}_{0_{R}} ((k \in (0 ..^N) ⟼ {inv}_{g} (R) (F)))$
73	1 13 12 58 60 71 72	gsuminv	$⊢ φ \to \sum_{R} ({inv}_{g} (R) \circ (k \in (0 ..^N) ⟼ {inv}_{g} (R) (F))) = {inv}_{g} (R) (\underset{k \in (0 ..^N)}{\sum_{R}} {inv}_{g} (R) (F))$
74	1 12	grpinvf	$⊢ R \in Grp \to {inv}_{g} (R) : B ⟶ B$
75	20 74	syl	$⊢ φ \to {inv}_{g} (R) : B ⟶ B$
76	75 63	cofmpt	$⊢ φ \to {inv}_{g} (R) \circ (k \in (0 ..^N) ⟼ {inv}_{g} (R) (F)) = (k \in (0 ..^N) ⟼ {inv}_{g} (R) ({inv}_{g} (R) (F)))$
77	1 12 39 62	grpinvinvd	$⊢ (φ \land k \in (0 ..^N)) \to {inv}_{g} (R) ({inv}_{g} (R) (F)) = F$
78	77	mpteq2dva	$⊢ φ \to (k \in (0 ..^N) ⟼ {inv}_{g} (R) ({inv}_{g} (R) (F))) = (k \in (0 ..^N) ⟼ F)$
79	76 78	eqtrd	$⊢ φ \to {inv}_{g} (R) \circ (k \in (0 ..^N) ⟼ {inv}_{g} (R) (F)) = (k \in (0 ..^N) ⟼ F)$
80	79	oveq2d	$⊢ φ \to \sum_{R} ({inv}_{g} (R) \circ (k \in (0 ..^N) ⟼ {inv}_{g} (R) (F))) = \underset{k \in (0 ..^N)}{\sum_{R}} F$
81	73 80	eqtr3d	$⊢ φ \to {inv}_{g} (R) (\underset{k \in (0 ..^N)}{\sum_{R}} {inv}_{g} (R) (F)) = \underset{k \in (0 ..^N)}{\sum_{R}} F$
82	1 12 20 67	grpinvinvd	$⊢ φ \to {inv}_{g} (R) ({inv}_{g} (R) (E)) = E$
83	81 82	oveq12d	$⊢ φ \to {inv}_{g} (R) (\underset{k \in (0 ..^N)}{\sum_{R}} {inv}_{g} (R) (F)) \underset{˙}{+} {inv}_{g} (R) ({inv}_{g} (R) (E)) = (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E$
84	57 70 83	3eqtrd	$⊢ φ \to {inv}_{g} (R) ((\sum_{R}, D) \underset{˙}{\cdot} (C \underset{˙}{-} A)) = (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E$
85	22 25 84	3eqtr3d	$⊢ φ \to (\sum_{R}, D) \underset{˙}{\cdot} (A \underset{˙}{-} C) = (\underset{k \in (0 ..^N)}{\sum_{R}}, F) \underset{˙}{+} E$

Metamath Proof Explorer

Theorem gsummulsubdishift2

Proof