Theorem gsumind

Description: The group sum of an indicator function of the set A gives the size of A . (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	gsumind.1	$$⊢\phi \to O\in V$$
	gsumind.2	$$⊢\phi \to A\subseteq O$$
	gsumind.3	$$⊢\phi \to A\in \mathrm{Fin}$$
Assertion	gsumind	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}{𝟙}_O\left(A\right)=\left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		gsumind.1	$$⊢\phi \to O\in V$$
2		gsumind.2	$$⊢\phi \to A\subseteq O$$
3		gsumind.3	$$⊢\phi \to A\in \mathrm{Fin}$$
4		indval2	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)=\left(A\times \left\{1\right\}\right)\cup \left(\left(O\setminus A\right)\times \left\{0\right\}\right)$$
5	1 2 4	syl2anc	$$⊢\phi \to {𝟙}_O\left(A\right)=\left(A\times \left\{1\right\}\right)\cup \left(\left(O\setminus A\right)\times \left\{0\right\}\right)$$
6	5	reseq1d	$$⊢\phi \to {{𝟙}_O\left(A\right)\upharpoonright }_A={\left(\left(A\times \left\{1\right\}\right)\cup \left(\left(O\setminus A\right)\times \left\{0\right\}\right)\right)\upharpoonright }_A$$
7		1ex	$$⊢1\in \mathrm{V}$$
8	7	fconst	$$⊢\left(A\times \left\{1\right\}\right):A⟶\left\{1\right\}$$
9	8	a1i	$$⊢\phi \to \left(A\times \left\{1\right\}\right):A⟶\left\{1\right\}$$
10	9	ffnd	$$⊢\phi \to \left(A\times \left\{1\right\}\right)FnA$$
11		c0ex	$$⊢0\in \mathrm{V}$$
12	11	fconst	$$⊢\left(\left(O\setminus A\right)\times \left\{0\right\}\right):O\setminus A⟶\left\{0\right\}$$
13	12	a1i	$$⊢\phi \to \left(\left(O\setminus A\right)\times \left\{0\right\}\right):O\setminus A⟶\left\{0\right\}$$
14	13	ffnd	$$⊢\phi \to \left(\left(O\setminus A\right)\times \left\{0\right\}\right)Fn\left(O\setminus A\right)$$
15		disjdif	$$⊢A\cap \left(O\setminus A\right)=\varnothing$$
16	15	a1i	$$⊢\phi \to A\cap \left(O\setminus A\right)=\varnothing$$
17		fnunres1	$$⊢\left(\left(A\times \left\{1\right\}\right)FnA\wedge \left(\left(O\setminus A\right)\times \left\{0\right\}\right)Fn\left(O\setminus A\right)\wedge A\cap \left(O\setminus A\right)=\varnothing \right)\to {\left(\left(A\times \left\{1\right\}\right)\cup \left(\left(O\setminus A\right)\times \left\{0\right\}\right)\right)\upharpoonright }_A=A\times \left\{1\right\}$$
18	10 14 16 17	syl3anc	$$⊢\phi \to {\left(\left(A\times \left\{1\right\}\right)\cup \left(\left(O\setminus A\right)\times \left\{0\right\}\right)\right)\upharpoonright }_A=A\times \left\{1\right\}$$
19		fconstmpt	$$⊢A\times \left\{1\right\}=\left(x\in A⟼1\right)$$
20	19	a1i	$$⊢\phi \to A\times \left\{1\right\}=\left(x\in A⟼1\right)$$
21	6 18 20	3eqtrd	$$⊢\phi \to {{𝟙}_O\left(A\right)\upharpoonright }_A=\left(x\in A⟼1\right)$$
22	21	oveq2d	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{𝟙}_O\left(A\right)\upharpoonright }_A\right)=\underset{x\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}}}1$$
23		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
24		cnfld0	$$⊢0=0_{{ℂ}_{\mathrm{fld}}}$$
25		cnfldfld	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
26	25	a1i	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{Field}$$
27	26	fldcrngd	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
28	27	crngringd	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$$
29	28	ringcmnd	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$$
30		indf	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right):O⟶\left\{0,1\right\}$$
31	1 2 30	syl2anc	$$⊢\phi \to {𝟙}_O\left(A\right):O⟶\left\{0,1\right\}$$
32		0cnd	$$⊢\phi \to 0\in ℂ$$
33		1cnd	$$⊢\phi \to 1\in ℂ$$
34	32 33	prssd	$$⊢\phi \to \left\{0,1\right\}\subseteq ℂ$$
35	31 34	fssd	$$⊢\phi \to {𝟙}_O\left(A\right):O⟶ℂ$$
36		indsupp	$$⊢\left(O\in V\wedge A\subseteq O\right)\to {𝟙}_O\left(A\right)\mathrm{supp}0=A$$
37	1 2 36	syl2anc	$$⊢\phi \to {𝟙}_O\left(A\right)\mathrm{supp}0=A$$
38	37	eqimssd	$$⊢\phi \to {𝟙}_O\left(A\right)\mathrm{supp}0\subseteq A$$
39	1 2 3	indfsd	$$⊢\phi \to {finSupp}_0\left({𝟙}_O\left(A\right)\right)$$
40	23 24 29 1 35 38 39	gsumres	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{𝟙}_O\left(A\right)\upharpoonright }_A\right)={\sum }_{{ℂ}_{\mathrm{fld}}}{𝟙}_O\left(A\right)$$
41	27	crnggrpd	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{Grp}$$
42	41	grpmndd	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$$
43		eqid	$$⊢{\cdot }_{{ℂ}_{\mathrm{fld}}}={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
44	23 43	gsumconst	$$⊢\left({ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}\wedge A\in \mathrm{Fin}\wedge 1\in ℂ\right)\to \underset{x\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}}}1=\left|A\right|{\cdot }_{{ℂ}_{\mathrm{fld}}}1$$
45	42 3 33 44	syl3anc	$$⊢\phi \to \underset{x\in A}{{\sum }_{{ℂ}_{\mathrm{fld}}}}1=\left|A\right|{\cdot }_{{ℂ}_{\mathrm{fld}}}1$$
46	22 40 45	3eqtr3d	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}{𝟙}_O\left(A\right)=\left|A\right|{\cdot }_{{ℂ}_{\mathrm{fld}}}1$$
47		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
48	3 47	syl	$$⊢\phi \to \left|A\right|\in {\mathbb{N}}_0$$
49	48	nn0zd	$$⊢\phi \to \left|A\right|\in \mathbb{Z}$$
50		cnfldmulg	$$⊢\left(\left|A\right|\in \mathbb{Z}\wedge 1\in ℂ\right)\to \left|A\right|{\cdot }_{{ℂ}_{\mathrm{fld}}}1=\left|A\right|\cdot 1$$
51	49 33 50	syl2anc	$$⊢\phi \to \left|A\right|{\cdot }_{{ℂ}_{\mathrm{fld}}}1=\left|A\right|\cdot 1$$
52	48	nn0cnd	$$⊢\phi \to \left|A\right|\in ℂ$$
53	52	mulridd	$$⊢\phi \to \left|A\right|\cdot 1=\left|A\right|$$
54	46 51 53	3eqtrd	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}{𝟙}_O\left(A\right)=\left|A\right|$$