Metamath Proof Explorer

Theorem ballotlemfval

Description: The value of F . (Contributed by Thierry Arnoux, 23-Nov-2016)

Ref Expression
Hypotheses ballotth.m 
|- M e. NN
ballotth.n 
|- N e. NN
ballotth.o 
|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
ballotth.p 
|- P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
ballotth.f 
|- F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
ballotlemfval.c 
|- ( ph -> C e. O )
ballotlemfval.j 
|- ( ph -> J e. ZZ )
Assertion ballotlemfval 
|- ( ph -> ( ( F ` C ) ` J ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )

Proof

Step Hyp Ref Expression
1 ballotth.m 
 |-  M e. NN
2 ballotth.n 
 |-  N e. NN
3 ballotth.o 
 |-  O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4 ballotth.p 
 |-  P = ( x e. ~P O |-> ( ( # ` x ) / ( # ` O ) ) )
5 ballotth.f 
 |-  F = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
6 ballotlemfval.c 
 |-  ( ph -> C e. O )
7 ballotlemfval.j 
 |-  ( ph -> J e. ZZ )
8 simpl 
 |-  ( ( b = C /\ i e. ZZ ) -> b = C )
9 8 ineq2d 
 |-  ( ( b = C /\ i e. ZZ ) -> ( ( 1 ... i ) i^i b ) = ( ( 1 ... i ) i^i C ) )
10 9 fveq2d 
 |-  ( ( b = C /\ i e. ZZ ) -> ( # ` ( ( 1 ... i ) i^i b ) ) = ( # ` ( ( 1 ... i ) i^i C ) ) )
11 8 difeq2d 
 |-  ( ( b = C /\ i e. ZZ ) -> ( ( 1 ... i ) \ b ) = ( ( 1 ... i ) \ C ) )
12 11 fveq2d 
 |-  ( ( b = C /\ i e. ZZ ) -> ( # ` ( ( 1 ... i ) \ b ) ) = ( # ` ( ( 1 ... i ) \ C ) ) )
13 10 12 oveq12d 
 |-  ( ( b = C /\ i e. ZZ ) -> ( ( # ` ( ( 1 ... i ) i^i b ) ) - ( # ` ( ( 1 ... i ) \ b ) ) ) = ( ( # ` ( ( 1 ... i ) i^i C ) ) - ( # ` ( ( 1 ... i ) \ C ) ) ) )
14 13 mpteq2dva 
 |-  ( b = C -> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i b ) ) - ( # ` ( ( 1 ... i ) \ b ) ) ) ) = ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i C ) ) - ( # ` ( ( 1 ... i ) \ C ) ) ) ) )
15 ineq2 
 |-  ( b = c -> ( ( 1 ... i ) i^i b ) = ( ( 1 ... i ) i^i c ) )
16 15 fveq2d 
 |-  ( b = c -> ( # ` ( ( 1 ... i ) i^i b ) ) = ( # ` ( ( 1 ... i ) i^i c ) ) )
17 difeq2 
 |-  ( b = c -> ( ( 1 ... i ) \ b ) = ( ( 1 ... i ) \ c ) )
18 17 fveq2d 
 |-  ( b = c -> ( # ` ( ( 1 ... i ) \ b ) ) = ( # ` ( ( 1 ... i ) \ c ) ) )
19 16 18 oveq12d 
 |-  ( b = c -> ( ( # ` ( ( 1 ... i ) i^i b ) ) - ( # ` ( ( 1 ... i ) \ b ) ) ) = ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) )
20 19 mpteq2dv 
 |-  ( b = c -> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i b ) ) - ( # ` ( ( 1 ... i ) \ b ) ) ) ) = ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
21 20 cbvmptv 
 |-  ( b e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i b ) ) - ( # ` ( ( 1 ... i ) \ b ) ) ) ) ) = ( c e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i c ) ) - ( # ` ( ( 1 ... i ) \ c ) ) ) ) )
22 5 21 eqtr4i 
 |-  F = ( b e. O |-> ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i b ) ) - ( # ` ( ( 1 ... i ) \ b ) ) ) ) )
23 zex 
 |-  ZZ e. _V
24 23 mptex 
 |-  ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i C ) ) - ( # ` ( ( 1 ... i ) \ C ) ) ) ) e. _V
25 14 22 24 fvmpt 
 |-  ( C e. O -> ( F ` C ) = ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i C ) ) - ( # ` ( ( 1 ... i ) \ C ) ) ) ) )
26 6 25 syl 
 |-  ( ph -> ( F ` C ) = ( i e. ZZ |-> ( ( # ` ( ( 1 ... i ) i^i C ) ) - ( # ` ( ( 1 ... i ) \ C ) ) ) ) )
27 oveq2 
 |-  ( i = J -> ( 1 ... i ) = ( 1 ... J ) )
28 27 ineq1d 
 |-  ( i = J -> ( ( 1 ... i ) i^i C ) = ( ( 1 ... J ) i^i C ) )
29 28 fveq2d 
 |-  ( i = J -> ( # ` ( ( 1 ... i ) i^i C ) ) = ( # ` ( ( 1 ... J ) i^i C ) ) )
30 27 difeq1d 
 |-  ( i = J -> ( ( 1 ... i ) \ C ) = ( ( 1 ... J ) \ C ) )
31 30 fveq2d 
 |-  ( i = J -> ( # ` ( ( 1 ... i ) \ C ) ) = ( # ` ( ( 1 ... J ) \ C ) ) )
32 29 31 oveq12d 
 |-  ( i = J -> ( ( # ` ( ( 1 ... i ) i^i C ) ) - ( # ` ( ( 1 ... i ) \ C ) ) ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )
33 32 adantl 
 |-  ( ( ph /\ i = J ) -> ( ( # ` ( ( 1 ... i ) i^i C ) ) - ( # ` ( ( 1 ... i ) \ C ) ) ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )
34 ovexd 
 |-  ( ph -> ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) e. _V )
35 26 33 7 34 fvmptd 
 |-  ( ph -> ( ( F ` C ) ` J ) = ( ( # ` ( ( 1 ... J ) i^i C ) ) - ( # ` ( ( 1 ... J ) \ C ) ) ) )