Theorem eulerpartlemsv1

Description: Lemma for eulerpart . Value of the sum of a partition A . (Contributed by Thierry Arnoux, 26-Aug-2018)

	Ref	Expression
Hypotheses	eulerpartlems.r	|- R = { f | ( `' f " NN ) e. Fin }
	eulerpartlems.s	|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
Assertion	eulerpartlemsv1	|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. NN ( ( A ` k ) x. k ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpartlems.r	|- R = { f | ( `' f " NN ) e. Fin }
2		eulerpartlems.s	|- S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) )
3	2	a1i	|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> S = ( f e. ( ( NN0 ^m NN ) i^i R ) |-> sum_ k e. NN ( ( f ` k ) x. k ) ) )
4		simplr	|- ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ f = A ) /\ k e. NN ) -> f = A )
5	4	fveq1d	|- ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ f = A ) /\ k e. NN ) -> ( f ` k ) = ( A ` k ) )
6	5	oveq1d	|- ( ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ f = A ) /\ k e. NN ) -> ( ( f ` k ) x. k ) = ( ( A ` k ) x. k ) )
7	6	sumeq2dv	|- ( ( A e. ( ( NN0 ^m NN ) i^i R ) /\ f = A ) -> sum_ k e. NN ( ( f ` k ) x. k ) = sum_ k e. NN ( ( A ` k ) x. k ) )
8		id	|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> A e. ( ( NN0 ^m NN ) i^i R ) )
9		sumex	|- sum_ k e. NN ( ( A ` k ) x. k ) e. _V
10	9	a1i	|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> sum_ k e. NN ( ( A ` k ) x. k ) e. _V )
11	3 7 8 10	fvmptd	|- ( A e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` A ) = sum_ k e. NN ( ( A ` k ) x. k ) )