Theorem sticksstones21

Description: Lift sticks and stones to arbitrary finite non-empty sets. (Contributed by metakunt, 24-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones21.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sticksstones21.2	$$⊢\phi \to S\in \mathrm{Fin}$$
	sticksstones21.3	$$⊢\phi \to S\ne \varnothing$$
	sticksstones21.4	$$⊢A=\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)=N\right)\right\}$$
Assertion	sticksstones21	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+\left|S\right|-1}{\left|S\right|-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sticksstones21.1	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		sticksstones21.2	$$⊢\phi \to S\in \mathrm{Fin}$$
3		sticksstones21.3	$$⊢\phi \to S\ne \varnothing$$
4		sticksstones21.4	$$⊢A=\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)=N\right)\right\}$$
5		hashnncl	$$⊢S\in \mathrm{Fin}\to \left(\left|S\right|\in \mathbb{N}\leftrightarrow S\ne \varnothing \right)$$
6	2 5	syl	$$⊢\phi \to \left(\left|S\right|\in \mathbb{N}\leftrightarrow S\ne \varnothing \right)$$
7	3 6	mpbird	$$⊢\phi \to \left|S\right|\in \mathbb{N}$$
8		fveq2	$$⊢j=k\to g\left(j\right)=g\left(k\right)$$
9	8	cbvsumv	$$⊢\sum _{j=1}^{\left|S\right|}g\left(j\right)=\sum _{k=1}^{\left|S\right|}g\left(k\right)$$
10	9	eqeq1i	$$⊢\sum _{j=1}^{\left|S\right|}g\left(j\right)=N\leftrightarrow \sum _{k=1}^{\left|S\right|}g\left(k\right)=N$$
11	10	anbi2i	$$⊢\left(g:\left(1\dots \left|S\right|\right)⟶{\mathbb{N}}_0\wedge \sum _{j=1}^{\left|S\right|}g\left(j\right)=N\right)\leftrightarrow \left(g:\left(1\dots \left|S\right|\right)⟶{\mathbb{N}}_0\wedge \sum _{k=1}^{\left|S\right|}g\left(k\right)=N\right)$$
12	11	abbii	$$⊢\left\{g|\left(g:\left(1\dots \left|S\right|\right)⟶{\mathbb{N}}_0\wedge \sum _{j=1}^{\left|S\right|}g\left(j\right)=N\right)\right\}=\left\{g|\left(g:\left(1\dots \left|S\right|\right)⟶{\mathbb{N}}_0\wedge \sum _{k=1}^{\left|S\right|}g\left(k\right)=N\right)\right\}$$
13		fveq2	$$⊢i=k\to f\left(i\right)=f\left(k\right)$$
14	13	cbvsumv	$$⊢\sum _{i\in S}f\left(i\right)=\sum _{k\in S}f\left(k\right)$$
15	14	eqeq1i	$$⊢\sum _{i\in S}f\left(i\right)=N\leftrightarrow \sum _{k\in S}f\left(k\right)=N$$
16	15	anbi2i	$$⊢\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)=N\right)\leftrightarrow \left(f:S⟶{\mathbb{N}}_0\wedge \sum _{k\in S}f\left(k\right)=N\right)$$
17	16	abbii	$$⊢\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{i\in S}f\left(i\right)=N\right)\right\}=\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{k\in S}f\left(k\right)=N\right)\right\}$$
18	4 17	eqtri	$$⊢A=\left\{f|\left(f:S⟶{\mathbb{N}}_0\wedge \sum _{k\in S}f\left(k\right)=N\right)\right\}$$
19		eqidd	$$⊢\phi \to \left|S\right|=\left|S\right|$$
20	1 2 7 12 18 19	sticksstones20	$$⊢\phi \to \left|A\right|=\left(\genfrac{}{}{0ex}{}{N+\left|S\right|-1}{\left|S\right|-1}\right)$$