Metamath Proof Explorer

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 
|- ( 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 ) )