Theorem fsumconst1

Description: The sum of 1 over a finite set equals the size of the set. (Contributed by AV, 10-Apr-2026)

	Ref	Expression
Assertion	fsumconst1	|- ( A e. Fin -> sum_ k e. A 1 = ( # ` A ) )

Proof

Step	Hyp	Ref	Expression
1		1cnd	|- ( A e. Fin -> 1 e. CC )
2		fsumconst	|- ( ( A e. Fin /\ 1 e. CC ) -> sum_ k e. A 1 = ( ( # ` A ) x. 1 ) )
3	1 2	mpdan	|- ( A e. Fin -> sum_ k e. A 1 = ( ( # ` A ) x. 1 ) )
4		hashcl	|- ( A e. Fin -> ( # ` A ) e. NN0 )
5	4	nn0cnd	|- ( A e. Fin -> ( # ` A ) e. CC )
6	5	mulridd	|- ( A e. Fin -> ( ( # ` A ) x. 1 ) = ( # ` A ) )
7	3 6	eqtrd	|- ( A e. Fin -> sum_ k e. A 1 = ( # ` A ) )