Metamath Proof Explorer

Theorem eulerpartleme

Description: Lemma for eulerpart . (Contributed by Mario Carneiro, 26-Jan-2015)

Ref Expression
Hypothesis eulerpart.p 
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
Assertion eulerpartleme 
|- ( A e. P <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) )

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 nn0ex 
 |-  NN0 e. _V
3 nnex 
 |-  NN e. _V
4 2 3 elmap 
 |-  ( A e. ( NN0 ^m NN ) <-> A : NN --> NN0 )
5 4 anbi1i 
 |-  ( ( A e. ( NN0 ^m NN ) /\ ( ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) ) <-> ( A : NN --> NN0 /\ ( ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) ) )
6 cnveq 
 |-  ( f = A -> `' f = `' A )
7 6 imaeq1d 
 |-  ( f = A -> ( `' f " NN ) = ( `' A " NN ) )
8 7 eleq1d 
 |-  ( f = A -> ( ( `' f " NN ) e. Fin <-> ( `' A " NN ) e. Fin ) )
9 fveq1 
 |-  ( f = A -> ( f ` k ) = ( A ` k ) )
10 9 oveq1d 
 |-  ( f = A -> ( ( f ` k ) x. k ) = ( ( A ` k ) x. k ) )
11 10 sumeq2sdv 
 |-  ( f = A -> sum_ k e. NN ( ( f ` k ) x. k ) = sum_ k e. NN ( ( A ` k ) x. k ) )
12 11 eqeq1d 
 |-  ( f = A -> ( sum_ k e. NN ( ( f ` k ) x. k ) = N <-> sum_ k e. NN ( ( A ` k ) x. k ) = N ) )
13 8 12 anbi12d 
 |-  ( f = A -> ( ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) <-> ( ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) ) )
14 13 1 elrab2 
 |-  ( A e. P <-> ( A e. ( NN0 ^m NN ) /\ ( ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) ) )
15 3anass 
 |-  ( ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) <-> ( A : NN --> NN0 /\ ( ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) ) )
16 5 14 15 3bitr4i 
 |-  ( A e. P <-> ( A : NN --> NN0 /\ ( `' A " NN ) e. Fin /\ sum_ k e. NN ( ( A ` k ) x. k ) = N ) )