suppgsumssiun

Description: The support of a function defined as a group sum is a subset of the indexed union of the supports. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	suppgsumssiun.1	$⊢ Z = 0_{M}$
	suppgsumssiun.2	$⊢ φ \to M \in Mnd$
	suppgsumssiun.3	$⊢ φ \to B \in W$
	suppgsumssiun.4	$⊢ φ \to A \in V$
	suppgsumssiun.5	$⊢ ((φ \land x \in A) \land y \in B) \to C \in X$
Assertion	suppgsumssiun	$⊢ φ \to (x \in A ⟼ \underset{y \in B}{\sum_{M}} C) supp Z \subseteq ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C))$

Proof

Step	Hyp	Ref	Expression
1		suppgsumssiun.1	$⊢ Z = 0_{M}$
2		suppgsumssiun.2	$⊢ φ \to M \in Mnd$
3		suppgsumssiun.3	$⊢ φ \to B \in W$
4		suppgsumssiun.4	$⊢ φ \to A \in V$
5		suppgsumssiun.5	$⊢ ((φ \land x \in A) \land y \in B) \to C \in X$
6		nfv	$⊢ Ⅎ x φ$
7		nfcv	$⊢ \underline{Ⅎ} x A$
8		nfcv	$⊢ \underline{Ⅎ} x B$
9		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ C)$
10		nfcv	$⊢ \underline{Ⅎ} x supp$
11		nfcv	$⊢ \underline{Ⅎ} x Z$
12	9 10 11	nfov	$⊢ \underline{Ⅎ} x {supp}_{Z} ((x \in A ⟼ C))$
13	8 12	nfiun	$⊢ \underline{Ⅎ} x ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C))$
14		mpt0	$⊢ (y \in \emptyset ⟼ C) = \emptyset$
15	14	oveq2i	$⊢ \underset{y \in \emptyset}{\sum_{M}} C = \sum_{M} \emptyset$
16	1	gsum0	$⊢ \sum_{M} \emptyset = Z$
17	15 16	eqtri	$⊢ \underset{y \in \emptyset}{\sum_{M}} C = Z$
18		mpteq1	$⊢ B = \emptyset \to (y \in B ⟼ C) = (y \in \emptyset ⟼ C)$
19	18	oveq2d	$⊢ B = \emptyset \to \underset{y \in B}{\sum_{M}} C = \underset{y \in \emptyset}{\sum_{M}} C$
20	19	adantl	$⊢ ((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B = \emptyset) \to \underset{y \in B}{\sum_{M}} C = \underset{y \in \emptyset}{\sum_{M}} C$
21	1	gsumz	$⊢ (M \in Mnd \land B \in W) \to \underset{y \in B}{\sum_{M}} Z = Z$
22	2 3 21	syl2anc	$⊢ φ \to \underset{y \in B}{\sum_{M}} Z = Z$
23	22	adantr	$⊢ (φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \to \underset{y \in B}{\sum_{M}} Z = Z$
24	23	adantr	$⊢ ((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B = \emptyset) \to \underset{y \in B}{\sum_{M}} Z = Z$
25	17 20 24	3eqtr4a	$⊢ ((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B = \emptyset) \to \underset{y \in B}{\sum_{M}} C = \underset{y \in B}{\sum_{M}} Z$
26		nfv	$⊢ Ⅎ y φ$
27		nfcv	$⊢ \underline{Ⅎ} y A$
28		nfiu1	$⊢ \underline{Ⅎ} y ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C))$
29	27 28	nfdif	$⊢ \underline{Ⅎ} y (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))$
30	29	nfcri	$⊢ Ⅎ y x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))$
31	26 30	nfan	$⊢ Ⅎ y (φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C))))$
32		nfv	$⊢ Ⅎ y B \neq \emptyset$
33	31 32	nfan	$⊢ Ⅎ y ((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset)$
34		simpllr	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))$
35		iindif2	$⊢ B \neq \emptyset \to ⋂_{y \in B} (A ∖ {supp}_{Z} ((x \in A ⟼ C))) = A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C))$
36	35	ad2antlr	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to ⋂_{y \in B} (A ∖ {supp}_{Z} ((x \in A ⟼ C))) = A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C))$
37	34 36	eleqtrrd	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to x \in ⋂_{y \in B} (A ∖ {supp}_{Z} ((x \in A ⟼ C)))$
38		eliin	$⊢ x \in ⋂_{y \in B} (A ∖ {supp}_{Z} ((x \in A ⟼ C))) \to (x \in ⋂_{y \in B} (A ∖ {supp}_{Z} ((x \in A ⟼ C))) \leftrightarrow \forall y \in B x \in (A ∖ {supp}_{Z} ((x \in A ⟼ C))))$
39	38	ibi	$⊢ x \in ⋂_{y \in B} (A ∖ {supp}_{Z} ((x \in A ⟼ C))) \to \forall y \in B x \in (A ∖ {supp}_{Z} ((x \in A ⟼ C)))$
40	39	r19.21bi	$⊢ (x \in ⋂_{y \in B} (A ∖ {supp}_{Z} ((x \in A ⟼ C))) \land y \in B) \to x \in (A ∖ {supp}_{Z} ((x \in A ⟼ C)))$
41	37 40	sylancom	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to x \in (A ∖ {supp}_{Z} ((x \in A ⟼ C)))$
42	41	eldifbd	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to \neg x \in {supp}_{Z} ((x \in A ⟼ C))$
43	34	eldifad	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to x \in A$
44		nfv	$⊢ Ⅎ x ((φ \land B \neq \emptyset) \land y \in B)$
45	5	an32s	$⊢ ((φ \land y \in B) \land x \in A) \to C \in X$
46	45	adantllr	$⊢ (((φ \land B \neq \emptyset) \land y \in B) \land x \in A) \to C \in X$
47		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
48	44 46 47	fnmptd	$⊢ ((φ \land B \neq \emptyset) \land y \in B) \to (x \in A ⟼ C) Fn A$
49	48	adantllr	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to (x \in A ⟼ C) Fn A$
50	4	ad3antrrr	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to A \in V$
51		eqid	$⊢ {Base}_{M} = {Base}_{M}$
52	51 1	mndidcl	$⊢ M \in Mnd \to Z \in {Base}_{M}$
53	2 52	syl	$⊢ φ \to Z \in {Base}_{M}$
54	53	ad3antrrr	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to Z \in {Base}_{M}$
55		elsuppfn	$⊢ ((x \in A ⟼ C) Fn A \land A \in V \land Z \in {Base}_{M}) \to (x \in {supp}_{Z} ((x \in A ⟼ C)) \leftrightarrow (x \in A \land (x \in A ⟼ C) (x) \neq Z))$
56	49 50 54 55	syl3anc	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to (x \in {supp}_{Z} ((x \in A ⟼ C)) \leftrightarrow (x \in A \land (x \in A ⟼ C) (x) \neq Z))$
57	43 56	mpbirand	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to (x \in {supp}_{Z} ((x \in A ⟼ C)) \leftrightarrow (x \in A ⟼ C) (x) \neq Z)$
58		difssd	$⊢ φ \to A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)) \subseteq A$
59	58	sselda	$⊢ (φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \to x \in A$
60	59 5	syldanl	$⊢ ((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land y \in B) \to C \in X$
61	60	adantlr	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to C \in X$
62	47	fvmpt2	$⊢ (x \in A \land C \in X) \to (x \in A ⟼ C) (x) = C$
63	43 61 62	syl2anc	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to (x \in A ⟼ C) (x) = C$
64	63	neeq1d	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to ((x \in A ⟼ C) (x) \neq Z \leftrightarrow C \neq Z)$
65	57 64	bitrd	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to (x \in {supp}_{Z} ((x \in A ⟼ C)) \leftrightarrow C \neq Z)$
66	65	necon2bbid	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to (C = Z \leftrightarrow \neg x \in {supp}_{Z} ((x \in A ⟼ C)))$
67	42 66	mpbird	$⊢ (((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \land y \in B) \to C = Z$
68	33 67	mpteq2da	$⊢ ((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \to (y \in B ⟼ C) = (y \in B ⟼ Z)$
69	68	oveq2d	$⊢ ((φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \land B \neq \emptyset) \to \underset{y \in B}{\sum_{M}} C = \underset{y \in B}{\sum_{M}} Z$
70	25 69	pm2.61dane	$⊢ (φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \to \underset{y \in B}{\sum_{M}} C = \underset{y \in B}{\sum_{M}} Z$
71	70 23	eqtrd	$⊢ (φ \land x \in (A ∖ ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C)))) \to \underset{y \in B}{\sum_{M}} C = Z$
72	6 7 13 71 4	suppss2f	$⊢ φ \to (x \in A ⟼ \underset{y \in B}{\sum_{M}} C) supp Z \subseteq ⋃_{y \in B} {supp}_{Z} ((x \in A ⟼ C))$

Metamath Proof Explorer

Theorem suppgsumssiun

Proof