Metamath Proof Explorer


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 ) )