Theorem eulerpartlemsf

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 8-Aug-2018)

	Ref	Expression
Hypotheses	eulerpartlems.r	$$⊢R=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	eulerpartlems.s	$$⊢S=\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)$$
Assertion	eulerpartlemsf	$$⊢S:\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R⟶{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		eulerpartlems.r	$$⊢R=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		eulerpartlems.s	$$⊢S=\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)$$
3		simpl	$$⊢\left(g=f\wedge k\in \mathbb{N}\right)\to g=f$$
4	3	fveq1d	$$⊢\left(g=f\wedge k\in \mathbb{N}\right)\to g\left(k\right)=f\left(k\right)$$
5	4	oveq1d	$$⊢\left(g=f\wedge k\in \mathbb{N}\right)\to g\left(k\right)k=f\left(k\right)k$$
6	5	sumeq2dv	$$⊢g=f\to \sum _{k\in \mathbb{N}}g\left(k\right)k=\sum _{k\in \mathbb{N}}f\left(k\right)k$$
7	6	eleq1d	$$⊢g=f\to \left(\sum _{k\in \mathbb{N}}g\left(k\right)k\in {\mathbb{N}}_0\leftrightarrow \sum _{k\in \mathbb{N}}f\left(k\right)k\in {\mathbb{N}}_0\right)$$
8	1 2	eulerpartlemsv2	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(g\right)=\sum _{k\in g^{-1}\left[\mathbb{N}\right]}g\left(k\right)k$$
9	1 2	eulerpartlemsv1	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(g\right)=\sum _{k\in \mathbb{N}}g\left(k\right)k$$
10	8 9	eqtr3d	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \sum _{k\in g^{-1}\left[\mathbb{N}\right]}g\left(k\right)k=\sum _{k\in \mathbb{N}}g\left(k\right)k$$
11	1 2	eulerpartlemelr	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \left(g:\mathbb{N}⟶{\mathbb{N}}_0\wedge g^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
12	11	simprd	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to g^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
13	11	simpld	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to g:\mathbb{N}⟶{\mathbb{N}}_0$$
14	13	adantr	$$⊢\left(g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in g^{-1}\left[\mathbb{N}\right]\right)\to g:\mathbb{N}⟶{\mathbb{N}}_0$$
15		cnvimass	$$⊢g^{-1}\left[\mathbb{N}\right]\subseteq \mathrm{dom}g$$
16	15 13	fssdm	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to g^{-1}\left[\mathbb{N}\right]\subseteq \mathbb{N}$$
17	16	sselda	$$⊢\left(g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in g^{-1}\left[\mathbb{N}\right]\right)\to k\in \mathbb{N}$$
18	14 17	ffvelrnd	$$⊢\left(g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in g^{-1}\left[\mathbb{N}\right]\right)\to g\left(k\right)\in {\mathbb{N}}_0$$
19	17	nnnn0d	$$⊢\left(g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in g^{-1}\left[\mathbb{N}\right]\right)\to k\in {\mathbb{N}}_0$$
20	18 19	nn0mulcld	$$⊢\left(g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in g^{-1}\left[\mathbb{N}\right]\right)\to g\left(k\right)k\in {\mathbb{N}}_0$$
21	12 20	fsumnn0cl	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \sum _{k\in g^{-1}\left[\mathbb{N}\right]}g\left(k\right)k\in {\mathbb{N}}_0$$
22	10 21	eqeltrrd	$$⊢g\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \sum _{k\in \mathbb{N}}g\left(k\right)k\in {\mathbb{N}}_0$$
23	7 22	vtoclga	$$⊢f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \sum _{k\in \mathbb{N}}f\left(k\right)k\in {\mathbb{N}}_0$$
24	2 23	fmpti	$$⊢S:\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R⟶{\mathbb{N}}_0$$