gsummptres2

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 22-Jun-2024)

	Ref	Expression
Hypotheses	gsummptres2.b	$⊢ B = {Base}_{G}$
	gsummptres2.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsummptres2.g	$⊢ φ \to G \in CMnd$
	gsummptres2.a	$⊢ φ \to A \in V$
	gsummptres2.0	$⊢ (φ \land x \in (A ∖ S)) \to Y = \underset{˙}{0}$
	gsummptres2.1	$⊢ φ \to S \in Fin$
	gsummptres2.y	$⊢ (φ \land x \in A) \to Y \in B$
	gsummptres2.2	$⊢ φ \to S \subseteq A$
Assertion	gsummptres2	$⊢ φ \to \underset{x \in A}{\sum_{G}} Y = \underset{x \in S}{\sum_{G}} Y$

Proof

Step	Hyp	Ref	Expression
1		gsummptres2.b	$⊢ B = {Base}_{G}$
2		gsummptres2.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsummptres2.g	$⊢ φ \to G \in CMnd$
4		gsummptres2.a	$⊢ φ \to A \in V$
5		gsummptres2.0	$⊢ (φ \land x \in (A ∖ S)) \to Y = \underset{˙}{0}$
6		gsummptres2.1	$⊢ φ \to S \in Fin$
7		gsummptres2.y	$⊢ (φ \land x \in A) \to Y \in B$
8		gsummptres2.2	$⊢ φ \to S \subseteq A$
9		eqid	$⊢ +_{G} = +_{G}$
10	4	mptexd	$⊢ φ \to (x \in A ⟼ Y) \in V$
11		funmpt	$⊢ Fun (x \in A ⟼ Y)$
12	11	a1i	$⊢ φ \to Fun (x \in A ⟼ Y)$
13	2	fvexi	$⊢ \underset{˙}{0} \in V$
14	13	a1i	$⊢ φ \to \underset{˙}{0} \in V$
15	5 4	suppss2	$⊢ φ \to (x \in A ⟼ Y) supp \underset{˙}{0} \subseteq S$
16		suppssfifsupp	$⊢ (((x \in A ⟼ Y) \in V \land Fun (x \in A ⟼ Y) \land \underset{˙}{0} \in V) \land (S \in Fin \land (x \in A ⟼ Y) supp \underset{˙}{0} \subseteq S)) \to {finSupp}_{\underset{˙}{0}} ((x \in A ⟼ Y))$
17	10 12 14 6 15 16	syl32anc	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((x \in A ⟼ Y))$
18		disjdif	$⊢ S \cap (A ∖ S) = \emptyset$
19	18	a1i	$⊢ φ \to S \cap (A ∖ S) = \emptyset$
20		undif	$⊢ S \subseteq A \leftrightarrow S \cup (A ∖ S) = A$
21	8 20	sylib	$⊢ φ \to S \cup (A ∖ S) = A$
22	21	eqcomd	$⊢ φ \to A = S \cup (A ∖ S)$
23	1 2 9 3 4 7 17 19 22	gsumsplit2	$⊢ φ \to \underset{x \in A}{\sum_{G}} Y = (\underset{x \in S}{\sum_{G}}, Y) +_{G} (\underset{x \in A ∖ S}{\sum_{G}}, Y)$
24	5	mpteq2dva	$⊢ φ \to (x \in (A ∖ S) ⟼ Y) = (x \in (A ∖ S) ⟼ \underset{˙}{0})$
25	24	oveq2d	$⊢ φ \to \underset{x \in A ∖ S}{\sum_{G}} Y = \underset{x \in A ∖ S}{\sum_{G}} \underset{˙}{0}$
26	3	cmnmndd	$⊢ φ \to G \in Mnd$
27	4	difexd	$⊢ φ \to A ∖ S \in V$
28	2	gsumz	$⊢ (G \in Mnd \land A ∖ S \in V) \to \underset{x \in A ∖ S}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
29	26 27 28	syl2anc	$⊢ φ \to \underset{x \in A ∖ S}{\sum_{G}} \underset{˙}{0} = \underset{˙}{0}$
30	25 29	eqtrd	$⊢ φ \to \underset{x \in A ∖ S}{\sum_{G}} Y = \underset{˙}{0}$
31	30	oveq2d	$⊢ φ \to (\underset{x \in S}{\sum_{G}}, Y) +_{G} (\underset{x \in A ∖ S}{\sum_{G}}, Y) = (\underset{x \in S}{\sum_{G}}, Y) +_{G} \underset{˙}{0}$
32	7	ralrimiva	$⊢ φ \to \forall x \in A Y \in B$
33		ssralv	$⊢ S \subseteq A \to (\forall x \in A Y \in B \to \forall x \in S Y \in B)$
34	8 32 33	sylc	$⊢ φ \to \forall x \in S Y \in B$
35	1 3 6 34	gsummptcl	$⊢ φ \to \underset{x \in S}{\sum_{G}} Y \in B$
36	1 9 2	mndrid	$⊢ (G \in Mnd \land \underset{x \in S}{\sum_{G}} Y \in B) \to (\underset{x \in S}{\sum_{G}}, Y) +_{G} \underset{˙}{0} = \underset{x \in S}{\sum_{G}} Y$
37	26 35 36	syl2anc	$⊢ φ \to (\underset{x \in S}{\sum_{G}}, Y) +_{G} \underset{˙}{0} = \underset{x \in S}{\sum_{G}} Y$
38	23 31 37	3eqtrd	$⊢ φ \to \underset{x \in A}{\sum_{G}} Y = \underset{x \in S}{\sum_{G}} Y$

Metamath Proof Explorer

Theorem gsummptres2

Proof