Theorem eulerpartlemgv

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

	Ref	Expression
Hypotheses	eulerpart.p	|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
	eulerpart.o	|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
	eulerpart.d	|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
	eulerpart.j	|- J = { z e. NN | -. 2 || z }
	eulerpart.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
	eulerpart.h	|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
	eulerpart.m	|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
	eulerpart.r	|- R = { f | ( `' f " NN ) e. Fin }
	eulerpart.t	|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
	eulerpart.g	|- G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
Assertion	eulerpartlemgv	|- ( A e. ( T i^i R ) -> ( G ` A ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2		eulerpart.o	|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3		eulerpart.d	|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4		eulerpart.j	|- J = { z e. NN | -. 2 || z }
5		eulerpart.f	|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
6		eulerpart.h	|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
7		eulerpart.m	|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
8		eulerpart.r	|- R = { f | ( `' f " NN ) e. Fin }
9		eulerpart.t	|- T = { f e. ( NN0 ^m NN ) | ( `' f " NN ) C_ J }
10		eulerpart.g	|- G = ( o e. ( T i^i R ) |-> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) )
11		reseq1	|- ( o = A -> ( o |` J ) = ( A |` J ) )
12	11	coeq2d	|- ( o = A -> ( bits o. ( o |` J ) ) = ( bits o. ( A |` J ) ) )
13	12	fveq2d	|- ( o = A -> ( M ` ( bits o. ( o |` J ) ) ) = ( M ` ( bits o. ( A |` J ) ) ) )
14	13	imaeq2d	|- ( o = A -> ( F " ( M ` ( bits o. ( o |` J ) ) ) ) = ( F " ( M ` ( bits o. ( A |` J ) ) ) ) )
15	14	fveq2d	|- ( o = A -> ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( o |` J ) ) ) ) ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) )
16		fvex	|- ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) e. _V
17	15 10 16	fvmpt	|- ( A e. ( T i^i R ) -> ( G ` A ) = ( ( _Ind ` NN ) ` ( F " ( M ` ( bits o. ( A |` J ) ) ) ) ) )