Metamath Proof Explorer

Theorem gsummpt2co

Description: Split a finite sum into a sum of a collection of sums over disjoint subsets. (Contributed by Thierry Arnoux, 27-Mar-2018)

Ref Expression
Hypotheses gsummpt2co.b 
|- B = ( Base ` W )
gsummpt2co.z 
|- .0. = ( 0g ` W )
gsummpt2co.w 
|- ( ph -> W e. CMnd )
gsummpt2co.a 
|- ( ph -> A e. Fin )
gsummpt2co.e 
|- ( ph -> E e. V )
gsummpt2co.1 
|- ( ( ph /\ x e. A ) -> C e. B )
gsummpt2co.2 
|- ( ( ph /\ x e. A ) -> D e. E )
gsummpt2co.3 
|- F = ( x e. A |-> D )
Assertion gsummpt2co 
|- ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( y e. E |-> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsummpt2co.b 
 |-  B = ( Base ` W )
2 gsummpt2co.z 
 |-  .0. = ( 0g ` W )
3 gsummpt2co.w 
 |-  ( ph -> W e. CMnd )
4 gsummpt2co.a 
 |-  ( ph -> A e. Fin )
5 gsummpt2co.e 
 |-  ( ph -> E e. V )
6 gsummpt2co.1 
 |-  ( ( ph /\ x e. A ) -> C e. B )
7 gsummpt2co.2 
 |-  ( ( ph /\ x e. A ) -> D e. E )
8 gsummpt2co.3 
 |-  F = ( x e. A |-> D )
9 nfcsb1v 
 |-  F/_ x [_ ( 2nd ` p ) / x ]_ C
10 csbeq1a 
 |-  ( x = ( 2nd ` p ) -> C = [_ ( 2nd ` p ) / x ]_ C )
11 ssidd 
 |-  ( ph -> B C_ B )
12 elcnv 
 |-  ( p e. `' F <-> E. z E. x ( p = <. z , x >. /\ x F z ) )
13 vex 
 |-  z e. _V
14 vex 
 |-  x e. _V
15 13 14 op2ndd 
 |-  ( p = <. z , x >. -> ( 2nd ` p ) = x )
16 15 adantr 
 |-  ( ( p = <. z , x >. /\ x F z ) -> ( 2nd ` p ) = x )
17 8 dmmptss 
 |-  dom F C_ A
18 14 13 breldm 
 |-  ( x F z -> x e. dom F )
19 17 18 sselid 
 |-  ( x F z -> x e. A )
20 19 adantl 
 |-  ( ( p = <. z , x >. /\ x F z ) -> x e. A )
21 16 20 eqeltrd 
 |-  ( ( p = <. z , x >. /\ x F z ) -> ( 2nd ` p ) e. A )
22 21 exlimivv 
 |-  ( E. z E. x ( p = <. z , x >. /\ x F z ) -> ( 2nd ` p ) e. A )
23 12 22 sylbi 
 |-  ( p e. `' F -> ( 2nd ` p ) e. A )
24 23 adantl 
 |-  ( ( ph /\ p e. `' F ) -> ( 2nd ` p ) e. A )
25 8 funmpt2 
 |-  Fun F
26 funcnvcnv 
 |-  ( Fun F -> Fun `' `' F )
27 25 26 ax-mp 
 |-  Fun `' `' F
28 27 a1i 
 |-  ( ( ph /\ x e. A ) -> Fun `' `' F )
29 dfdm4 
 |-  dom F = ran `' F
30 8 dmeqi 
 |-  dom F = dom ( x e. A |-> D )
31 7 ralrimiva 
 |-  ( ph -> A. x e. A D e. E )
32 dmmptg 
 |-  ( A. x e. A D e. E -> dom ( x e. A |-> D ) = A )
33 31 32 syl 
 |-  ( ph -> dom ( x e. A |-> D ) = A )
34 30 33 syl5eq 
 |-  ( ph -> dom F = A )
35 29 34 eqtr3id 
 |-  ( ph -> ran `' F = A )
36 35 eleq2d 
 |-  ( ph -> ( x e. ran `' F <-> x e. A ) )
37 36 biimpar 
 |-  ( ( ph /\ x e. A ) -> x e. ran `' F )
38 relcnv 
 |-  Rel `' F
39 fcnvgreu 
 |-  ( ( ( Rel `' F /\ Fun `' `' F ) /\ x e. ran `' F ) -> E! p e. `' F x = ( 2nd ` p ) )
40 38 39 mpanl1 
 |-  ( ( Fun `' `' F /\ x e. ran `' F ) -> E! p e. `' F x = ( 2nd ` p ) )
41 28 37 40 syl2anc 
 |-  ( ( ph /\ x e. A ) -> E! p e. `' F x = ( 2nd ` p ) )
42 9 1 2 10 3 4 11 6 24 41 gsummptf1o 
 |-  ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( p e. `' F |-> [_ ( 2nd ` p ) / x ]_ C ) ) )
43 8 rnmptss 
 |-  ( A. x e. A D e. E -> ran F C_ E )
44 31 43 syl 
 |-  ( ph -> ran F C_ E )
45 dfcnv2 
 |-  ( ran F C_ E -> `' F = U_ z e. E ( { z } X. ( `' F " { z } ) ) )
46 44 45 syl 
 |-  ( ph -> `' F = U_ z e. E ( { z } X. ( `' F " { z } ) ) )
47 46 mpteq1d 
 |-  ( ph -> ( p e. `' F |-> [_ ( 2nd ` p ) / x ]_ C ) = ( p e. U_ z e. E ( { z } X. ( `' F " { z } ) ) |-> [_ ( 2nd ` p ) / x ]_ C ) )
48 nfcv 
 |-  F/_ z [_ ( 2nd ` p ) / x ]_ C
49 csbeq1 
 |-  ( ( 2nd ` p ) = x -> [_ ( 2nd ` p ) / x ]_ C = [_ x / x ]_ C )
50 15 49 syl 
 |-  ( p = <. z , x >. -> [_ ( 2nd ` p ) / x ]_ C = [_ x / x ]_ C )
51 csbid 
 |-  [_ x / x ]_ C = C
52 50 51 eqtrdi 
 |-  ( p = <. z , x >. -> [_ ( 2nd ` p ) / x ]_ C = C )
53 48 9 52 mpomptxf 
 |-  ( p e. U_ z e. E ( { z } X. ( `' F " { z } ) ) |-> [_ ( 2nd ` p ) / x ]_ C ) = ( z e. E , x e. ( `' F " { z } ) |-> C )
54 47 53 eqtrdi 
 |-  ( ph -> ( p e. `' F |-> [_ ( 2nd ` p ) / x ]_ C ) = ( z e. E , x e. ( `' F " { z } ) |-> C ) )
55 54 oveq2d 
 |-  ( ph -> ( W gsum ( p e. `' F |-> [_ ( 2nd ` p ) / x ]_ C ) ) = ( W gsum ( z e. E , x e. ( `' F " { z } ) |-> C ) ) )
56 mptfi 
 |-  ( A e. Fin -> ( x e. A |-> D ) e. Fin )
57 8 56 eqeltrid 
 |-  ( A e. Fin -> F e. Fin )
58 cnvfi 
 |-  ( F e. Fin -> `' F e. Fin )
59 4 57 58 3syl 
 |-  ( ph -> `' F e. Fin )
60 imaexg 
 |-  ( `' F e. Fin -> ( `' F " { z } ) e. _V )
61 59 60 syl 
 |-  ( ph -> ( `' F " { z } ) e. _V )
62 61 adantr 
 |-  ( ( ph /\ z e. E ) -> ( `' F " { z } ) e. _V )
63 simpll 
 |-  ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> ph )
64 imassrn 
 |-  ( `' F " { z } ) C_ ran `' F
65 64 29 sseqtrri 
 |-  ( `' F " { z } ) C_ dom F
66 65 17 sstri 
 |-  ( `' F " { z } ) C_ A
67 13 14 elimasn 
 |-  ( x e. ( `' F " { z } ) <-> <. z , x >. e. `' F )
68 67 biimpi 
 |-  ( x e. ( `' F " { z } ) -> <. z , x >. e. `' F )
69 68 adantl 
 |-  ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> <. z , x >. e. `' F )
70 69 67 sylibr 
 |-  ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> x e. ( `' F " { z } ) )
71 66 70 sselid 
 |-  ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> x e. A )
72 63 71 6 syl2anc 
 |-  ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> C e. B )
73 72 anasss 
 |-  ( ( ph /\ ( z e. E /\ x e. ( `' F " { z } ) ) ) -> C e. B )
74 df-br 
 |-  ( z `' F x <-> <. z , x >. e. `' F )
75 69 74 sylibr 
 |-  ( ( ( ph /\ z e. E ) /\ x e. ( `' F " { z } ) ) -> z `' F x )
76 75 anasss 
 |-  ( ( ph /\ ( z e. E /\ x e. ( `' F " { z } ) ) ) -> z `' F x )
77 76 pm2.24d 
 |-  ( ( ph /\ ( z e. E /\ x e. ( `' F " { z } ) ) ) -> ( -. z `' F x -> C = .0. ) )
78 77 imp 
 |-  ( ( ( ph /\ ( z e. E /\ x e. ( `' F " { z } ) ) ) /\ -. z `' F x ) -> C = .0. )
79 78 anasss 
 |-  ( ( ph /\ ( ( z e. E /\ x e. ( `' F " { z } ) ) /\ -. z `' F x ) ) -> C = .0. )
80 1 2 3 5 62 73 59 79 gsum2d2 
 |-  ( ph -> ( W gsum ( z e. E , x e. ( `' F " { z } ) |-> C ) ) = ( W gsum ( z e. E |-> ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) ) ) )
81 42 55 80 3eqtrd 
 |-  ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( z e. E |-> ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) ) ) )
82 nfcv 
 |-  F/_ z ( W gsum ( x e. ( `' F " { y } ) |-> C ) )
83 nfcv 
 |-  F/_ y ( W gsum ( x e. ( `' F " { z } ) |-> C ) )
84 sneq 
 |-  ( y = z -> { y } = { z } )
85 84 imaeq2d 
 |-  ( y = z -> ( `' F " { y } ) = ( `' F " { z } ) )
86 85 mpteq1d 
 |-  ( y = z -> ( x e. ( `' F " { y } ) |-> C ) = ( x e. ( `' F " { z } ) |-> C ) )
87 86 oveq2d 
 |-  ( y = z -> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) = ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) )
88 82 83 87 cbvmpt 
 |-  ( y e. E |-> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) ) = ( z e. E |-> ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) )
89 88 oveq2i 
 |-  ( W gsum ( y e. E |-> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) ) ) = ( W gsum ( z e. E |-> ( W gsum ( x e. ( `' F " { z } ) |-> C ) ) ) )
90 81 89 eqtr4di 
 |-  ( ph -> ( W gsum ( x e. A |-> C ) ) = ( W gsum ( y e. E |-> ( W gsum ( x e. ( `' F " { y } ) |-> C ) ) ) ) )