Metamath Proof Explorer

Theorem eulerpartlemsf

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 8-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 eulerpartlemsf 
|- S : ( ( NN0 ^m NN ) i^i R ) --> NN0

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 simpl 
 |-  ( ( g = f /\ k e. NN ) -> g = f )
4 3 fveq1d 
 |-  ( ( g = f /\ k e. NN ) -> ( g ` k ) = ( f ` k ) )
5 4 oveq1d 
 |-  ( ( g = f /\ k e. NN ) -> ( ( g ` k ) x. k ) = ( ( f ` k ) x. k ) )
6 5 sumeq2dv 
 |-  ( g = f -> sum_ k e. NN ( ( g ` k ) x. k ) = sum_ k e. NN ( ( f ` k ) x. k ) )
7 6 eleq1d 
 |-  ( g = f -> ( sum_ k e. NN ( ( g ` k ) x. k ) e. NN0 <-> sum_ k e. NN ( ( f ` k ) x. k ) e. NN0 ) )
8 1 2 eulerpartlemsv2 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` g ) = sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) )
9 1 2 eulerpartlemsv1 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> ( S ` g ) = sum_ k e. NN ( ( g ` k ) x. k ) )
10 8 9 eqtr3d 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) = sum_ k e. NN ( ( g ` k ) x. k ) )
11 1 2 eulerpartlemelr 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) )
12 11 simprd 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> ( `' g " NN ) e. Fin )
13 11 simpld 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> g : NN --> NN0 )
14 13 adantr 
 |-  ( ( g e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' g " NN ) ) -> g : NN --> NN0 )
15 cnvimass 
 |-  ( `' g " NN ) C_ dom g
16 15 13 fssdm 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> ( `' g " NN ) C_ NN )
17 16 sselda 
 |-  ( ( g e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' g " NN ) ) -> k e. NN )
18 14 17 ffvelcdmd 
 |-  ( ( g e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' g " NN ) ) -> ( g ` k ) e. NN0 )
19 17 nnnn0d 
 |-  ( ( g e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' g " NN ) ) -> k e. NN0 )
20 18 19 nn0mulcld 
 |-  ( ( g e. ( ( NN0 ^m NN ) i^i R ) /\ k e. ( `' g " NN ) ) -> ( ( g ` k ) x. k ) e. NN0 )
21 12 20 fsumnn0cl 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) e. NN0 )
22 10 21 eqeltrrd 
 |-  ( g e. ( ( NN0 ^m NN ) i^i R ) -> sum_ k e. NN ( ( g ` k ) x. k ) e. NN0 )
23 7 22 vtoclga 
 |-  ( f e. ( ( NN0 ^m NN ) i^i R ) -> sum_ k e. NN ( ( f ` k ) x. k ) e. NN0 )
24 2 23 fmpti 
 |-  S : ( ( NN0 ^m NN ) i^i R ) --> NN0