Metamath Proof Explorer

Theorem esumc

Description: Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017)

Ref Expression
Hypotheses esumc.0 
|- F/_ k D
esumc.1 
|- F/ k ph
esumc.2 
|- F/_ k A
esumc.3 
|- ( y = C -> D = B )
esumc.4 
|- ( ph -> A e. V )
esumc.5 
|- ( ph -> Fun `' ( k e. A |-> C ) )
esumc.6 
|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
esumc.7 
|- ( ( ph /\ k e. A ) -> C e. W )
Assertion esumc 
|- ( ph -> sum* k e. A B = sum* y e. { z | E. k e. A z = C } D )

Proof

Step Hyp Ref Expression
1 esumc.0 
 |-  F/_ k D
2 esumc.1 
 |-  F/ k ph
3 esumc.2 
 |-  F/_ k A
4 esumc.3 
 |-  ( y = C -> D = B )
5 esumc.4 
 |-  ( ph -> A e. V )
6 esumc.5 
 |-  ( ph -> Fun `' ( k e. A |-> C ) )
7 esumc.6 
 |-  ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
8 esumc.7 
 |-  ( ( ph /\ k e. A ) -> C e. W )
9 nfcv 
 |-  F/_ y B
10 nfre1 
 |-  F/ k E. k e. A z = C
11 10 nfab 
 |-  F/_ k { z | E. k e. A z = C }
12 nfmpt1 
 |-  F/_ k ( k e. A |-> C )
13 elex 
 |-  ( A e. V -> A e. _V )
14 5 13 syl 
 |-  ( ph -> A e. _V )
15 3 14 abrexexd 
 |-  ( ph -> { z | E. k e. A z = C } e. _V )
16 8 ex 
 |-  ( ph -> ( k e. A -> C e. W ) )
17 2 16 ralrimi 
 |-  ( ph -> A. k e. A C e. W )
18 3 fnmptf 
 |-  ( A. k e. A C e. W -> ( k e. A |-> C ) Fn A )
19 17 18 syl 
 |-  ( ph -> ( k e. A |-> C ) Fn A )
20 eqid 
 |-  ( k e. A |-> C ) = ( k e. A |-> C )
21 20 rnmpt 
 |-  ran ( k e. A |-> C ) = { z | E. k e. A z = C }
22 21 a1i 
 |-  ( ph -> ran ( k e. A |-> C ) = { z | E. k e. A z = C } )
23 dff1o2 
 |-  ( ( k e. A |-> C ) : A -1-1-onto-> { z | E. k e. A z = C } <-> ( ( k e. A |-> C ) Fn A /\ Fun `' ( k e. A |-> C ) /\ ran ( k e. A |-> C ) = { z | E. k e. A z = C } ) )
24 19 6 22 23 syl3anbrc 
 |-  ( ph -> ( k e. A |-> C ) : A -1-1-onto-> { z | E. k e. A z = C } )
25 simpr 
 |-  ( ( ph /\ k e. A ) -> k e. A )
26 3 fvmpt2f 
 |-  ( ( k e. A /\ C e. W ) -> ( ( k e. A |-> C ) ` k ) = C )
27 25 8 26 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( k e. A |-> C ) ` k ) = C )
28 vex 
 |-  y e. _V
29 eqeq1 
 |-  ( z = y -> ( z = C <-> y = C ) )
30 29 rexbidv 
 |-  ( z = y -> ( E. k e. A z = C <-> E. k e. A y = C ) )
31 28 30 elab 
 |-  ( y e. { z | E. k e. A z = C } <-> E. k e. A y = C )
32 4 reximi 
 |-  ( E. k e. A y = C -> E. k e. A D = B )
33 31 32 sylbi 
 |-  ( y e. { z | E. k e. A z = C } -> E. k e. A D = B )
34 nfcv 
 |-  F/_ k ( 0 [,] +oo )
35 1 34 nfel 
 |-  F/ k D e. ( 0 [,] +oo )
36 eleq1 
 |-  ( D = B -> ( D e. ( 0 [,] +oo ) <-> B e. ( 0 [,] +oo ) ) )
37 7 36 syl5ibrcom 
 |-  ( ( ph /\ k e. A ) -> ( D = B -> D e. ( 0 [,] +oo ) ) )
38 37 ex 
 |-  ( ph -> ( k e. A -> ( D = B -> D e. ( 0 [,] +oo ) ) ) )
39 2 35 38 rexlimd 
 |-  ( ph -> ( E. k e. A D = B -> D e. ( 0 [,] +oo ) ) )
40 39 imp 
 |-  ( ( ph /\ E. k e. A D = B ) -> D e. ( 0 [,] +oo ) )
41 33 40 sylan2 
 |-  ( ( ph /\ y e. { z | E. k e. A z = C } ) -> D e. ( 0 [,] +oo ) )
42 2 1 9 11 3 12 4 15 24 27 41 esumf1o 
 |-  ( ph -> sum* y e. { z | E. k e. A z = C } D = sum* k e. A B )
43 42 eqcomd 
 |-  ( ph -> sum* k e. A B = sum* y e. { z | E. k e. A z = C } D )