Theorem eulerpartlemgv

Description: Lemma for eulerpart : value of the function G . (Contributed by Thierry Arnoux, 13-Nov-2017)

	Ref	Expression
Hypotheses	eulerpart.p	$$⊢P=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|\left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge \sum _{k\in \mathbb{N}}f\left(k\right)k=N\right)\right\}$$
	eulerpart.o	$$⊢O=\left\{g\in P|\forall n\in g^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\right\}$$
	eulerpart.d	$$⊢D=\left\{g\in P|\forall n\in \mathbb{N}g\left(n\right)\le 1\right\}$$
	eulerpart.j	$$⊢J=\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}$$
	eulerpart.f	$$⊢F=\left(x\in J,y\in {\mathbb{N}}_0⟼2^{y}x\right)$$
	eulerpart.h	$$⊢H=\left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$$
	eulerpart.m	$$⊢M=\left(r\in H⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)$$
	eulerpart.r	$$⊢R=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	eulerpart.t	$$⊢T=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|f^{-1}\left[\mathbb{N}\right]\subseteq J\right\}$$
	eulerpart.g	$$⊢G=\left(o\in \left(T\cap R\right)⟼{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({o\upharpoonright }_J\right)\right)\right]\right)\right)$$
Assertion	eulerpartlemgv	$$⊢A\in \left(T\cap R\right)\to G\left(A\right)={𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	$$⊢P=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|\left(f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\wedge \sum _{k\in \mathbb{N}}f\left(k\right)k=N\right)\right\}$$
2		eulerpart.o	$$⊢O=\left\{g\in P|\forall n\in g^{-1}\left[\mathbb{N}\right]\neg 2\parallel n\right\}$$
3		eulerpart.d	$$⊢D=\left\{g\in P|\forall n\in \mathbb{N}g\left(n\right)\le 1\right\}$$
4		eulerpart.j	$$⊢J=\left\{z\in \mathbb{N}|\neg 2\parallel z\right\}$$
5		eulerpart.f	$$⊢F=\left(x\in J,y\in {\mathbb{N}}_0⟼2^{y}x\right)$$
6		eulerpart.h	$$⊢H=\left\{r\in \left({\left(𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\right)}^J\right)|r\mathrm{supp}\varnothing \in \mathrm{Fin}\right\}$$
7		eulerpart.m	$$⊢M=\left(r\in H⟼\left\{⟨x,y⟩|\left(x\in J\wedge y\in r\left(x\right)\right)\right\}\right)$$
8		eulerpart.r	$$⊢R=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
9		eulerpart.t	$$⊢T=\left\{f\in \left({{\mathbb{N}}_0}^{\mathbb{N}}\right)|f^{-1}\left[\mathbb{N}\right]\subseteq J\right\}$$
10		eulerpart.g	$$⊢G=\left(o\in \left(T\cap R\right)⟼{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({o\upharpoonright }_J\right)\right)\right]\right)\right)$$
11		reseq1	$$⊢o=A\to {o\upharpoonright }_J={A\upharpoonright }_J$$
12	11	coeq2d	$$⊢o=A\to \mathrm{bits}\circ \left({o\upharpoonright }_J\right)=\mathrm{bits}\circ \left({A\upharpoonright }_J\right)$$
13	12	fveq2d	$$⊢o=A\to M\left(\mathrm{bits}\circ \left({o\upharpoonright }_J\right)\right)=M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)$$
14	13	imaeq2d	$$⊢o=A\to F\left[M\left(\mathrm{bits}\circ \left({o\upharpoonright }_J\right)\right)\right]=F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]$$
15	14	fveq2d	$$⊢o=A\to {𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({o\upharpoonright }_J\right)\right)\right]\right)={𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\right)$$
16		fvex	$$⊢{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\right)\in \mathrm{V}$$
17	15 10 16	fvmpt	$$⊢A\in \left(T\cap R\right)\to G\left(A\right)={𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\right)$$