Theorem eulerpartlemgf

Description: Lemma for eulerpart : Images under G have finite support. (Contributed by Thierry Arnoux, 29-Aug-2018)

	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	eulerpartlemgf	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$

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	1 2 3 4 5 6 7 8 9 10	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)$$
12	11	cnveqd	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}={{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\right)}^{-1}$$
13	12	imaeq1d	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}\left[\left\{1\right\}\right]={{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\right)}^{-1}\left[\left\{1\right\}\right]$$
14		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
15		imassrn	$$⊢F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\subseteq \mathrm{ran}F$$
16	4 5	oddpwdc	$$⊢F:J\times {\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathbb{N}$$
17		f1of	$$⊢F:J\times {\mathbb{N}}_0\underset{1-1\; onto}{⟶}\mathbb{N}\to F:J\times {\mathbb{N}}_0⟶\mathbb{N}$$
18		frn	$$⊢F:J\times {\mathbb{N}}_0⟶\mathbb{N}\to \mathrm{ran}F\subseteq \mathbb{N}$$
19	16 17 18	mp2b	$$⊢\mathrm{ran}F\subseteq \mathbb{N}$$
20	15 19	sstri	$$⊢F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\subseteq \mathbb{N}$$
21		indpi1	$$⊢\left(\mathbb{N}\in \mathrm{V}\wedge F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\subseteq \mathbb{N}\right)\to {{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\right)}^{-1}\left[\left\{1\right\}\right]=F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]$$
22	14 20 21	mp2an	$$⊢{{𝟙}_{\mathbb{N}}\left(F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\right)}^{-1}\left[\left\{1\right\}\right]=F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]$$
23	13 22	eqtrdi	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}\left[\left\{1\right\}\right]=F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]$$
24		ffun	$$⊢F:J\times {\mathbb{N}}_0⟶\mathbb{N}\to \mathrm{Fun}F$$
25	16 17 24	mp2b	$$⊢\mathrm{Fun}F$$
26		inss2	$$⊢𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}\subseteq \mathrm{Fin}$$
27	1 2 3 4 5 6 7 8 9 10	eulerpartlemmf	$$⊢A\in \left(T\cap R\right)\to \mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in H$$
28	1 2 3 4 5 6 7	eulerpartlem1	$$⊢M:H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}$$
29		f1of	$$⊢M:H\underset{1-1\; onto}{⟶}𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}\to M:H⟶𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}$$
30	28 29	ax-mp	$$⊢M:H⟶𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}$$
31	30	ffvelrni	$$⊢\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\in H\to M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\in \left(𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}\right)$$
32	27 31	syl	$$⊢A\in \left(T\cap R\right)\to M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\in \left(𝒫\left(J\times {\mathbb{N}}_0\right)\cap \mathrm{Fin}\right)$$
33	26 32	sseldi	$$⊢A\in \left(T\cap R\right)\to M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\in \mathrm{Fin}$$
34		imafi	$$⊢\left(\mathrm{Fun}F\wedge M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\in \mathrm{Fin}\right)\to F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\in \mathrm{Fin}$$
35	25 33 34	sylancr	$$⊢A\in \left(T\cap R\right)\to F\left[M\left(\mathrm{bits}\circ \left({A\upharpoonright }_J\right)\right)\right]\in \mathrm{Fin}$$
36	23 35	eqeltrd	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}\left[\left\{1\right\}\right]\in \mathrm{Fin}$$
37	1 2 3 4 5 6 7 8 9 10	eulerpartgbij	$$⊢G:T\cap R\underset{1-1\; onto}{⟶}\left({\left\{0,1\right\}}^{\mathbb{N}}\right)\cap R$$
38		f1of	$$⊢G:T\cap R\underset{1-1\; onto}{⟶}\left({\left\{0,1\right\}}^{\mathbb{N}}\right)\cap R\to G:T\cap R⟶\left({\left\{0,1\right\}}^{\mathbb{N}}\right)\cap R$$
39	37 38	ax-mp	$$⊢G:T\cap R⟶\left({\left\{0,1\right\}}^{\mathbb{N}}\right)\cap R$$
40	39	ffvelrni	$$⊢A\in \left(T\cap R\right)\to G\left(A\right)\in \left(\left({\left\{0,1\right\}}^{\mathbb{N}}\right)\cap R\right)$$
41		elin	$$⊢G\left(A\right)\in \left(\left({\left\{0,1\right\}}^{\mathbb{N}}\right)\cap R\right)\leftrightarrow \left(G\left(A\right)\in \left({\left\{0,1\right\}}^{\mathbb{N}}\right)\wedge G\left(A\right)\in R\right)$$
42	41	simplbi	$$⊢G\left(A\right)\in \left(\left({\left\{0,1\right\}}^{\mathbb{N}}\right)\cap R\right)\to G\left(A\right)\in \left({\left\{0,1\right\}}^{\mathbb{N}}\right)$$
43		elmapi	$$⊢G\left(A\right)\in \left({\left\{0,1\right\}}^{\mathbb{N}}\right)\to G\left(A\right):\mathbb{N}⟶\left\{0,1\right\}$$
44	40 42 43	3syl	$$⊢A\in \left(T\cap R\right)\to G\left(A\right):\mathbb{N}⟶\left\{0,1\right\}$$
45	44	ffund	$$⊢A\in \left(T\cap R\right)\to \mathrm{Fun}G\left(A\right)$$
46		ssv	$$⊢{\mathbb{N}}_0\subseteq \mathrm{V}$$
47		dfn2	$$⊢\mathbb{N}={\mathbb{N}}_0\setminus \left\{0\right\}$$
48		ssdif	$$⊢{\mathbb{N}}_0\subseteq \mathrm{V}\to {\mathbb{N}}_0\setminus \left\{0\right\}\subseteq \mathrm{V}\setminus \left\{0\right\}$$
49	47 48	eqsstrid	$$⊢{\mathbb{N}}_0\subseteq \mathrm{V}\to \mathbb{N}\subseteq \mathrm{V}\setminus \left\{0\right\}$$
50	46 49	ax-mp	$$⊢\mathbb{N}\subseteq \mathrm{V}\setminus \left\{0\right\}$$
51		sspreima	$$⊢\left(\mathrm{Fun}G\left(A\right)\wedge \mathbb{N}\subseteq \mathrm{V}\setminus \left\{0\right\}\right)\to {G\left(A\right)}^{-1}\left[\mathbb{N}\right]\subseteq {G\left(A\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$$
52	45 50 51	sylancl	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}\left[\mathbb{N}\right]\subseteq {G\left(A\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$$
53		fvex	$$⊢G\left(A\right)\in \mathrm{V}$$
54		0nn0	$$⊢0\in {\mathbb{N}}_0$$
55		suppimacnv	$$⊢\left(G\left(A\right)\in \mathrm{V}\wedge 0\in {\mathbb{N}}_0\right)\to G\left(A\right)\mathrm{supp}0={G\left(A\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$$
56	53 54 55	mp2an	$$⊢G\left(A\right)\mathrm{supp}0={G\left(A\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]$$
57		0ne1	$$⊢0\ne 1$$
58		difprsn1	$$⊢0\ne 1\to \left\{0,1\right\}\setminus \left\{0\right\}=\left\{1\right\}$$
59	57 58	ax-mp	$$⊢\left\{0,1\right\}\setminus \left\{0\right\}=\left\{1\right\}$$
60	59	eqcomi	$$⊢\left\{1\right\}=\left\{0,1\right\}\setminus \left\{0\right\}$$
61	60	ffs2	$$⊢\left(\mathbb{N}\in \mathrm{V}\wedge 0\in {\mathbb{N}}_0\wedge G\left(A\right):\mathbb{N}⟶\left\{0,1\right\}\right)\to G\left(A\right)\mathrm{supp}0={G\left(A\right)}^{-1}\left[\left\{1\right\}\right]$$
62	14 54 61	mp3an12	$$⊢G\left(A\right):\mathbb{N}⟶\left\{0,1\right\}\to G\left(A\right)\mathrm{supp}0={G\left(A\right)}^{-1}\left[\left\{1\right\}\right]$$
63	44 62	syl	$$⊢A\in \left(T\cap R\right)\to G\left(A\right)\mathrm{supp}0={G\left(A\right)}^{-1}\left[\left\{1\right\}\right]$$
64	56 63	syl5eqr	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}\left[\mathrm{V}\setminus \left\{0\right\}\right]={G\left(A\right)}^{-1}\left[\left\{1\right\}\right]$$
65	52 64	sseqtrd	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}\left[\mathbb{N}\right]\subseteq {G\left(A\right)}^{-1}\left[\left\{1\right\}\right]$$
66		ssfi	$$⊢\left({G\left(A\right)}^{-1}\left[\left\{1\right\}\right]\in \mathrm{Fin}\wedge {G\left(A\right)}^{-1}\left[\mathbb{N}\right]\subseteq {G\left(A\right)}^{-1}\left[\left\{1\right\}\right]\right)\to {G\left(A\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
67	36 65 66	syl2anc	$$⊢A\in \left(T\cap R\right)\to {G\left(A\right)}^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$