This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
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 ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )