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	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	gsumind.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
	gsumind.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion	gsumind	⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumind.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		gsumind.2	⊢ ( 𝜑 → 𝐴 ⊆ 𝑂 )
3		gsumind.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		indval2	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) ) )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) ) )
6	5	reseq1d	⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ↾ 𝐴 ) = ( ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) ) ↾ 𝐴 ) )
7		1ex	⊢ 1 ∈ V
8	7	fconst	⊢ ( 𝐴 × { 1 } ) : 𝐴 ⟶ { 1 }
9	8	a1i	⊢ ( 𝜑 → ( 𝐴 × { 1 } ) : 𝐴 ⟶ { 1 } )
10	9	ffnd	⊢ ( 𝜑 → ( 𝐴 × { 1 } ) Fn 𝐴 )
11		c0ex	⊢ 0 ∈ V
12	11	fconst	⊢ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) : ( 𝑂 ∖ 𝐴 ) ⟶ { 0 }
13	12	a1i	⊢ ( 𝜑 → ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) : ( 𝑂 ∖ 𝐴 ) ⟶ { 0 } )
14	13	ffnd	⊢ ( 𝜑 → ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) Fn ( 𝑂 ∖ 𝐴 ) )
15		disjdif	⊢ ( 𝐴 ∩ ( 𝑂 ∖ 𝐴 ) ) = ∅
16	15	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝑂 ∖ 𝐴 ) ) = ∅ )
17		fnunres1	⊢ ( ( ( 𝐴 × { 1 } ) Fn 𝐴 ∧ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) Fn ( 𝑂 ∖ 𝐴 ) ∧ ( 𝐴 ∩ ( 𝑂 ∖ 𝐴 ) ) = ∅ ) → ( ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) ) ↾ 𝐴 ) = ( 𝐴 × { 1 } ) )
18	10 14 16 17	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐴 × { 1 } ) ∪ ( ( 𝑂 ∖ 𝐴 ) × { 0 } ) ) ↾ 𝐴 ) = ( 𝐴 × { 1 } ) )
19		fconstmpt	⊢ ( 𝐴 × { 1 } ) = ( 𝑥 ∈ 𝐴 ↦ 1 )
20	19	a1i	⊢ ( 𝜑 → ( 𝐴 × { 1 } ) = ( 𝑥 ∈ 𝐴 ↦ 1 ) )
21	6 18 20	3eqtrd	⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ↾ 𝐴 ) = ( 𝑥 ∈ 𝐴 ↦ 1 ) )
22	21	oveq2d	⊢ ( 𝜑 → ( ℂfld Σg ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ↾ 𝐴 ) ) = ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ 1 ) ) )
23		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
24		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
25		cnfldfld	⊢ ℂfld ∈ Field
26	25	a1i	⊢ ( 𝜑 → ℂfld ∈ Field )
27	26	fldcrngd	⊢ ( 𝜑 → ℂfld ∈ CRing )
28	27	crngringd	⊢ ( 𝜑 → ℂfld ∈ Ring )
29	28	ringcmnd	⊢ ( 𝜑 → ℂfld ∈ CMnd )
30		indf	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
31	1 2 30	syl2anc	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
32		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
33		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
34	32 33	prssd	⊢ ( 𝜑 → { 0 , 1 } ⊆ ℂ )
35	31 34	fssd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ ℂ )
36		indsupp	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = 𝐴 )
37	1 2 36	syl2anc	⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = 𝐴 )
38	37	eqimssd	⊢ ( 𝜑 → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) ⊆ 𝐴 )
39	1 2 3	indfsd	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) finSupp 0 )
40	23 24 29 1 35 38 39	gsumres	⊢ ( 𝜑 → ( ℂfld Σg ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ↾ 𝐴 ) ) = ( ℂfld Σg ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ) )
41	27	crnggrpd	⊢ ( 𝜑 → ℂfld ∈ Grp )
42	41	grpmndd	⊢ ( 𝜑 → ℂfld ∈ Mnd )
43		eqid	⊢ ( .g ‘ ℂfld ) = ( .g ‘ ℂfld )
44	23 43	gsumconst	⊢ ( ( ℂfld ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 1 ∈ ℂ ) → ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ 1 ) ) = ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) 1 ) )
45	42 3 33 44	syl3anc	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ 1 ) ) = ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) 1 ) )
46	22 40 45	3eqtr3d	⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ) = ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) 1 ) )
47		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
48	3 47	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
49	48	nn0zd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℤ )
50		cnfldmulg	⊢ ( ( ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ 1 ∈ ℂ ) → ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) 1 ) = ( ( ♯ ‘ 𝐴 ) · 1 ) )
51	49 33 50	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) ( .g ‘ ℂfld ) 1 ) = ( ( ♯ ‘ 𝐴 ) · 1 ) )
52	48	nn0cnd	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℂ )
53	52	mulridd	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) · 1 ) = ( ♯ ‘ 𝐴 ) )
54	46 51 53	3eqtrd	⊢ ( 𝜑 → ( ℂfld Σg ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )