gsumpt

Description: Sum of a family that is nonzero at at most one point. (Contributed by Stefan O'Rear, 7-Feb-2015) (Revised by Mario Carneiro, 25-Apr-2016) (Revised by AV, 6-Jun-2019)

	Ref	Expression
Hypotheses	gsumpt.b	$⊢ B = {Base}_{G}$
	gsumpt.z	$⊢ \underset{˙}{0} = 0_{G}$
	gsumpt.g	$⊢ φ \to G \in Mnd$
	gsumpt.a	$⊢ φ \to A \in V$
	gsumpt.x	$⊢ φ \to X \in A$
	gsumpt.f	$⊢ φ \to F : A ⟶ B$
	gsumpt.s	$⊢ φ \to F supp \underset{˙}{0} \subseteq \{X\}$
Assertion	gsumpt	$⊢ φ \to \sum_{G} F = F (X)$

Proof

Step	Hyp	Ref	Expression
1		gsumpt.b	$⊢ B = {Base}_{G}$
2		gsumpt.z	$⊢ \underset{˙}{0} = 0_{G}$
3		gsumpt.g	$⊢ φ \to G \in Mnd$
4		gsumpt.a	$⊢ φ \to A \in V$
5		gsumpt.x	$⊢ φ \to X \in A$
6		gsumpt.f	$⊢ φ \to F : A ⟶ B$
7		gsumpt.s	$⊢ φ \to F supp \underset{˙}{0} \subseteq \{X\}$
8	5	snssd	$⊢ φ \to \{X\} \subseteq A$
9	6 8	feqresmpt	$⊢ φ \to {F ↾}_{\{X\}} = (a \in \{X\} ⟼ F (a))$
10	9	oveq2d	$⊢ φ \to \sum_{G} ({F ↾}_{\{X\}}) = \underset{a \in \{X\}}{\sum_{G}} F (a)$
11		eqid	$⊢ Cntz (G) = Cntz (G)$
12	6 5	ffvelrnd	$⊢ φ \to F (X) \in B$
13		eqidd	$⊢ φ \to F (X) +_{G} F (X) = F (X) +_{G} F (X)$
14		eqid	$⊢ +_{G} = +_{G}$
15	1 14 11	elcntzsn	$⊢ F (X) \in B \to (F (X) \in Cntz (G) (\{F (X)\}) \leftrightarrow (F (X) \in B \land F (X) +_{G} F (X) = F (X) +_{G} F (X)))$
16	12 15	syl	$⊢ φ \to (F (X) \in Cntz (G) (\{F (X)\}) \leftrightarrow (F (X) \in B \land F (X) +_{G} F (X) = F (X) +_{G} F (X)))$
17	12 13 16	mpbir2and	$⊢ φ \to F (X) \in Cntz (G) (\{F (X)\})$
18	17	snssd	$⊢ φ \to \{F (X)\} \subseteq Cntz (G) (\{F (X)\})$
19		eqid	$⊢ mrCls (SubMnd (G)) = mrCls (SubMnd (G))$
20		eqid	$⊢ G ↾_{𝑠} mrCls (SubMnd (G)) (\{F (X)\}) = G ↾_{𝑠} mrCls (SubMnd (G)) (\{F (X)\})$
21	11 19 20	cntzspan	$⊢ (G \in Mnd \land \{F (X)\} \subseteq Cntz (G) (\{F (X)\})) \to G ↾_{𝑠} mrCls (SubMnd (G)) (\{F (X)\}) \in CMnd$
22	3 18 21	syl2anc	$⊢ φ \to G ↾_{𝑠} mrCls (SubMnd (G)) (\{F (X)\}) \in CMnd$
23	1	submacs	$⊢ G \in Mnd \to SubMnd (G) \in ACS (B)$
24		acsmre	$⊢ SubMnd (G) \in ACS (B) \to SubMnd (G) \in Moore (B)$
25	3 23 24	3syl	$⊢ φ \to SubMnd (G) \in Moore (B)$
26	12	snssd	$⊢ φ \to \{F (X)\} \subseteq B$
27	19	mrccl	$⊢ (SubMnd (G) \in Moore (B) \land \{F (X)\} \subseteq B) \to mrCls (SubMnd (G)) (\{F (X)\}) \in SubMnd (G)$
28	25 26 27	syl2anc	$⊢ φ \to mrCls (SubMnd (G)) (\{F (X)\}) \in SubMnd (G)$
29	20 11	submcmn2	$⊢ mrCls (SubMnd (G)) (\{F (X)\}) \in SubMnd (G) \to (G ↾_{𝑠} mrCls (SubMnd (G)) (\{F (X)\}) \in CMnd \leftrightarrow mrCls (SubMnd (G)) (\{F (X)\}) \subseteq Cntz (G) (mrCls (SubMnd (G)) (\{F (X)\})))$
30	28 29	syl	$⊢ φ \to (G ↾_{𝑠} mrCls (SubMnd (G)) (\{F (X)\}) \in CMnd \leftrightarrow mrCls (SubMnd (G)) (\{F (X)\}) \subseteq Cntz (G) (mrCls (SubMnd (G)) (\{F (X)\})))$
31	22 30	mpbid	$⊢ φ \to mrCls (SubMnd (G)) (\{F (X)\}) \subseteq Cntz (G) (mrCls (SubMnd (G)) (\{F (X)\}))$
32	6	ffnd	$⊢ φ \to F Fn A$
33		simpr	$⊢ ((φ \land a \in A) \land a = X) \to a = X$
34	33	fveq2d	$⊢ ((φ \land a \in A) \land a = X) \to F (a) = F (X)$
35	25 19 26	mrcssidd	$⊢ φ \to \{F (X)\} \subseteq mrCls (SubMnd (G)) (\{F (X)\})$
36		fvex	$⊢ F (X) \in V$
37	36	snss	$⊢ F (X) \in mrCls (SubMnd (G)) (\{F (X)\}) \leftrightarrow \{F (X)\} \subseteq mrCls (SubMnd (G)) (\{F (X)\})$
38	35 37	sylibr	$⊢ φ \to F (X) \in mrCls (SubMnd (G)) (\{F (X)\})$
39	38	ad2antrr	$⊢ ((φ \land a \in A) \land a = X) \to F (X) \in mrCls (SubMnd (G)) (\{F (X)\})$
40	34 39	eqeltrd	$⊢ ((φ \land a \in A) \land a = X) \to F (a) \in mrCls (SubMnd (G)) (\{F (X)\})$
41		eldifsn	$⊢ a \in (A ∖ \{X\}) \leftrightarrow (a \in A \land a \neq X)$
42	2	fvexi	$⊢ \underset{˙}{0} \in V$
43	42	a1i	$⊢ φ \to \underset{˙}{0} \in V$
44	6 7 4 43	suppssr	$⊢ (φ \land a \in (A ∖ \{X\})) \to F (a) = \underset{˙}{0}$
45	41 44	sylan2br	$⊢ (φ \land (a \in A \land a \neq X)) \to F (a) = \underset{˙}{0}$
46	2	subm0cl	$⊢ mrCls (SubMnd (G)) (\{F (X)\}) \in SubMnd (G) \to \underset{˙}{0} \in mrCls (SubMnd (G)) (\{F (X)\})$
47	28 46	syl	$⊢ φ \to \underset{˙}{0} \in mrCls (SubMnd (G)) (\{F (X)\})$
48	47	adantr	$⊢ (φ \land (a \in A \land a \neq X)) \to \underset{˙}{0} \in mrCls (SubMnd (G)) (\{F (X)\})$
49	45 48	eqeltrd	$⊢ (φ \land (a \in A \land a \neq X)) \to F (a) \in mrCls (SubMnd (G)) (\{F (X)\})$
50	49	anassrs	$⊢ ((φ \land a \in A) \land a \neq X) \to F (a) \in mrCls (SubMnd (G)) (\{F (X)\})$
51	40 50	pm2.61dane	$⊢ (φ \land a \in A) \to F (a) \in mrCls (SubMnd (G)) (\{F (X)\})$
52	51	ralrimiva	$⊢ φ \to \forall a \in A F (a) \in mrCls (SubMnd (G)) (\{F (X)\})$
53		ffnfv	$⊢ F : A ⟶ mrCls (SubMnd (G)) (\{F (X)\}) \leftrightarrow (F Fn A \land \forall a \in A F (a) \in mrCls (SubMnd (G)) (\{F (X)\}))$
54	32 52 53	sylanbrc	$⊢ φ \to F : A ⟶ mrCls (SubMnd (G)) (\{F (X)\})$
55	54	frnd	$⊢ φ \to ran F \subseteq mrCls (SubMnd (G)) (\{F (X)\})$
56	11	cntzidss	$⊢ (mrCls (SubMnd (G)) (\{F (X)\}) \subseteq Cntz (G) (mrCls (SubMnd (G)) (\{F (X)\})) \land ran F \subseteq mrCls (SubMnd (G)) (\{F (X)\})) \to ran F \subseteq Cntz (G) (ran F)$
57	31 55 56	syl2anc	$⊢ φ \to ran F \subseteq Cntz (G) (ran F)$
58	6	ffund	$⊢ φ \to Fun F$
59		snfi	$⊢ \{X\} \in Fin$
60		ssfi	$⊢ (\{X\} \in Fin \land F supp \underset{˙}{0} \subseteq \{X\}) \to F supp \underset{˙}{0} \in Fin$
61	59 7 60	sylancr	$⊢ φ \to F supp \underset{˙}{0} \in Fin$
62		fex	$⊢ (F : A ⟶ B \land A \in V) \to F \in V$
63	6 4 62	syl2anc	$⊢ φ \to F \in V$
64		isfsupp	$⊢ (F \in V \land \underset{˙}{0} \in V) \to ({finSupp}_{\underset{˙}{0}} (F) \leftrightarrow (Fun F \land F supp \underset{˙}{0} \in Fin))$
65	63 43 64	syl2anc	$⊢ φ \to ({finSupp}_{\underset{˙}{0}} (F) \leftrightarrow (Fun F \land F supp \underset{˙}{0} \in Fin))$
66	58 61 65	mpbir2and	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$
67	1 2 11 3 4 6 57 7 66	gsumzres	$⊢ φ \to \sum_{G} ({F ↾}_{\{X\}}) = \sum_{G} F$
68		fveq2	$⊢ a = X \to F (a) = F (X)$
69	1 68	gsumsn	$⊢ (G \in Mnd \land X \in A \land F (X) \in B) \to \underset{a \in \{X\}}{\sum_{G}} F (a) = F (X)$
70	3 5 12 69	syl3anc	$⊢ φ \to \underset{a \in \{X\}}{\sum_{G}} F (a) = F (X)$
71	10 67 70	3eqtr3d	$⊢ φ \to \sum_{G} F = F (X)$

Metamath Proof Explorer

Theorem gsumpt

Proof