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	\|- ( ph -> O e. V )
	gsumind.2	\|- ( ph -> A C_ O )
	gsumind.3	\|- ( ph -> A e. Fin )
Assertion	gsumind	\|- ( ph -> ( CCfld gsum ( ( _Ind ` O ) ` A ) ) = ( # ` A ) )

Proof

Step	Hyp	Ref	Expression
1		gsumind.1	\|- ( ph -> O e. V )
2		gsumind.2	\|- ( ph -> A C_ O )
3		gsumind.3	\|- ( ph -> A e. Fin )
4		indval2	\|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) = ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) ) )
5	1 2 4	syl2anc	\|- ( ph -> ( ( _Ind ` O ) ` A ) = ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) ) )
6	5	reseq1d	\|- ( ph -> ( ( ( _Ind ` O ) ` A ) \|` A ) = ( ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) ) \|` A ) )
7		1ex	\|- 1 e. _V
8	7	fconst	\|- ( A X. { 1 } ) : A --> { 1 }
9	8	a1i	\|- ( ph -> ( A X. { 1 } ) : A --> { 1 } )
10	9	ffnd	\|- ( ph -> ( A X. { 1 } ) Fn A )
11		c0ex	\|- 0 e. _V
12	11	fconst	\|- ( ( O \ A ) X. { 0 } ) : ( O \ A ) --> { 0 }
13	12	a1i	\|- ( ph -> ( ( O \ A ) X. { 0 } ) : ( O \ A ) --> { 0 } )
14	13	ffnd	\|- ( ph -> ( ( O \ A ) X. { 0 } ) Fn ( O \ A ) )
15		disjdif	\|- ( A i^i ( O \ A ) ) = (/)
16	15	a1i	\|- ( ph -> ( A i^i ( O \ A ) ) = (/) )
17		fnunres1	\|- ( ( ( A X. { 1 } ) Fn A /\ ( ( O \ A ) X. { 0 } ) Fn ( O \ A ) /\ ( A i^i ( O \ A ) ) = (/) ) -> ( ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) ) \|` A ) = ( A X. { 1 } ) )
18	10 14 16 17	syl3anc	\|- ( ph -> ( ( ( A X. { 1 } ) u. ( ( O \ A ) X. { 0 } ) ) \|` A ) = ( A X. { 1 } ) )
19		fconstmpt	\|- ( A X. { 1 } ) = ( x e. A \|-> 1 )
20	19	a1i	\|- ( ph -> ( A X. { 1 } ) = ( x e. A \|-> 1 ) )
21	6 18 20	3eqtrd	\|- ( ph -> ( ( ( _Ind ` O ) ` A ) \|` A ) = ( x e. A \|-> 1 ) )
22	21	oveq2d	\|- ( ph -> ( CCfld gsum ( ( ( _Ind ` O ) ` A ) \|` A ) ) = ( CCfld gsum ( x e. A \|-> 1 ) ) )
23		cnfldbas	\|- CC = ( Base ` CCfld )
24		cnfld0	\|- 0 = ( 0g ` CCfld )
25		cnfldfld	\|- CCfld e. Field
26	25	a1i	\|- ( ph -> CCfld e. Field )
27	26	fldcrngd	\|- ( ph -> CCfld e. CRing )
28	27	crngringd	\|- ( ph -> CCfld e. Ring )
29	28	ringcmnd	\|- ( ph -> CCfld e. CMnd )
30		indf	\|- ( ( O e. V /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
31	1 2 30	syl2anc	\|- ( ph -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
32		0cnd	\|- ( ph -> 0 e. CC )
33		1cnd	\|- ( ph -> 1 e. CC )
34	32 33	prssd	\|- ( ph -> { 0 , 1 } C_ CC )
35	31 34	fssd	\|- ( ph -> ( ( _Ind ` O ) ` A ) : O --> CC )
36		indsupp	\|- ( ( O e. V /\ A C_ O ) -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = A )
37	1 2 36	syl2anc	\|- ( ph -> ( ( ( _Ind ` O ) ` A ) supp 0 ) = A )
38	37	eqimssd	\|- ( ph -> ( ( ( _Ind ` O ) ` A ) supp 0 ) C_ A )
39	1 2 3	indfsd	\|- ( ph -> ( ( _Ind ` O ) ` A ) finSupp 0 )
40	23 24 29 1 35 38 39	gsumres	\|- ( ph -> ( CCfld gsum ( ( ( _Ind ` O ) ` A ) \|` A ) ) = ( CCfld gsum ( ( _Ind ` O ) ` A ) ) )
41	27	crnggrpd	\|- ( ph -> CCfld e. Grp )
42	41	grpmndd	\|- ( ph -> CCfld e. Mnd )
43		eqid	\|- ( .g ` CCfld ) = ( .g ` CCfld )
44	23 43	gsumconst	\|- ( ( CCfld e. Mnd /\ A e. Fin /\ 1 e. CC ) -> ( CCfld gsum ( x e. A \|-> 1 ) ) = ( ( # ` A ) ( .g ` CCfld ) 1 ) )
45	42 3 33 44	syl3anc	\|- ( ph -> ( CCfld gsum ( x e. A \|-> 1 ) ) = ( ( # ` A ) ( .g ` CCfld ) 1 ) )
46	22 40 45	3eqtr3d	\|- ( ph -> ( CCfld gsum ( ( _Ind ` O ) ` A ) ) = ( ( # ` A ) ( .g ` CCfld ) 1 ) )
47		hashcl	\|- ( A e. Fin -> ( # ` A ) e. NN0 )
48	3 47	syl	\|- ( ph -> ( # ` A ) e. NN0 )
49	48	nn0zd	\|- ( ph -> ( # ` A ) e. ZZ )
50		cnfldmulg	\|- ( ( ( # ` A ) e. ZZ /\ 1 e. CC ) -> ( ( # ` A ) ( .g ` CCfld ) 1 ) = ( ( # ` A ) x. 1 ) )
51	49 33 50	syl2anc	\|- ( ph -> ( ( # ` A ) ( .g ` CCfld ) 1 ) = ( ( # ` A ) x. 1 ) )
52	48	nn0cnd	\|- ( ph -> ( # ` A ) e. CC )
53	52	mulridd	\|- ( ph -> ( ( # ` A ) x. 1 ) = ( # ` A ) )
54	46 51 53	3eqtrd	\|- ( ph -> ( CCfld gsum ( ( _Ind ` O ) ` A ) ) = ( # ` A ) )

Metamath Proof Explorer

Theorem gsumind

Proof