Metamath Proof Explorer

Theorem gsumpart

Description: Express a group sum as a double sum, grouping along a (possibly infinite) partition. (Contributed by Thierry Arnoux, 22-Jun-2024)

Ref Expression
Hypotheses gsumpart.b 
|- B = ( Base ` G )
gsumpart.z 
|- .0. = ( 0g ` G )
gsumpart.g 
|- ( ph -> G e. CMnd )
gsumpart.a 
|- ( ph -> A e. V )
gsumpart.x 
|- ( ph -> X e. W )
gsumpart.f 
|- ( ph -> F : A --> B )
gsumpart.w 
|- ( ph -> F finSupp .0. )
gsumpart.1 
|- ( ph -> Disj_ x e. X C )
gsumpart.2 
|- ( ph -> U_ x e. X C = A )
Assertion gsumpart 
|- ( ph -> ( G gsum F ) = ( G gsum ( x e. X |-> ( G gsum ( F |` C ) ) ) ) )

Proof

Step Hyp Ref Expression
1 gsumpart.b 
 |-  B = ( Base ` G )
2 gsumpart.z 
 |-  .0. = ( 0g ` G )
3 gsumpart.g 
 |-  ( ph -> G e. CMnd )
4 gsumpart.a 
 |-  ( ph -> A e. V )
5 gsumpart.x 
 |-  ( ph -> X e. W )
6 gsumpart.f 
 |-  ( ph -> F : A --> B )
7 gsumpart.w 
 |-  ( ph -> F finSupp .0. )
8 gsumpart.1 
 |-  ( ph -> Disj_ x e. X C )
9 gsumpart.2 
 |-  ( ph -> U_ x e. X C = A )
10 eqid 
 |-  U_ x e. X ( { x } X. C ) = U_ x e. X ( { x } X. C )
11 10 4 5 8 9 2ndresdjuf1o 
 |-  ( ph -> ( 2nd |` U_ x e. X ( { x } X. C ) ) : U_ x e. X ( { x } X. C ) -1-1-onto-> A )
12 1 2 3 4 6 7 11 gsumf1o 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) ) )
13 vsnex 
 |-  { x } e. _V
14 13 a1i 
 |-  ( ( ph /\ x e. X ) -> { x } e. _V )
15 4 adantr 
 |-  ( ( ph /\ x e. X ) -> A e. V )
16 ssidd 
 |-  ( ph -> A C_ A )
17 9 16 eqsstrd 
 |-  ( ph -> U_ x e. X C C_ A )
18 iunss 
 |-  ( U_ x e. X C C_ A <-> A. x e. X C C_ A )
19 17 18 sylib 
 |-  ( ph -> A. x e. X C C_ A )
20 19 r19.21bi 
 |-  ( ( ph /\ x e. X ) -> C C_ A )
21 15 20 ssexd 
 |-  ( ( ph /\ x e. X ) -> C e. _V )
22 14 21 xpexd 
 |-  ( ( ph /\ x e. X ) -> ( { x } X. C ) e. _V )
23 22 ralrimiva 
 |-  ( ph -> A. x e. X ( { x } X. C ) e. _V )
24 iunexg 
 |-  ( ( X e. W /\ A. x e. X ( { x } X. C ) e. _V ) -> U_ x e. X ( { x } X. C ) e. _V )
25 5 23 24 syl2anc 
 |-  ( ph -> U_ x e. X ( { x } X. C ) e. _V )
26 relxp 
 |-  Rel ( { x } X. C )
27 26 a1i 
 |-  ( ( ph /\ x e. X ) -> Rel ( { x } X. C ) )
28 27 ralrimiva 
 |-  ( ph -> A. x e. X Rel ( { x } X. C ) )
29 reliun 
 |-  ( Rel U_ x e. X ( { x } X. C ) <-> A. x e. X Rel ( { x } X. C ) )
30 28 29 sylibr 
 |-  ( ph -> Rel U_ x e. X ( { x } X. C ) )
31 dmiun 
 |-  dom U_ x e. X ( { x } X. C ) = U_ x e. X dom ( { x } X. C )
32 dmxpss 
 |-  dom ( { x } X. C ) C_ { x }
33 32 rgenw 
 |-  A. x e. X dom ( { x } X. C ) C_ { x }
34 ss2iun 
 |-  ( A. x e. X dom ( { x } X. C ) C_ { x } -> U_ x e. X dom ( { x } X. C ) C_ U_ x e. X { x } )
35 33 34 ax-mp 
 |-  U_ x e. X dom ( { x } X. C ) C_ U_ x e. X { x }
36 31 35 eqsstri 
 |-  dom U_ x e. X ( { x } X. C ) C_ U_ x e. X { x }
37 iunid 
 |-  U_ x e. X { x } = X
38 36 37 sseqtri 
 |-  dom U_ x e. X ( { x } X. C ) C_ X
39 38 a1i 
 |-  ( ph -> dom U_ x e. X ( { x } X. C ) C_ X )
40 fo2nd 
 |-  2nd : _V -onto-> _V
41 fof 
 |-  ( 2nd : _V -onto-> _V -> 2nd : _V --> _V )
42 40 41 ax-mp 
 |-  2nd : _V --> _V
43 ssv 
 |-  U_ x e. X ( { x } X. C ) C_ _V
44 fssres 
 |-  ( ( 2nd : _V --> _V /\ U_ x e. X ( { x } X. C ) C_ _V ) -> ( 2nd |` U_ x e. X ( { x } X. C ) ) : U_ x e. X ( { x } X. C ) --> _V )
45 42 43 44 mp2an 
 |-  ( 2nd |` U_ x e. X ( { x } X. C ) ) : U_ x e. X ( { x } X. C ) --> _V
46 ffn 
 |-  ( ( 2nd |` U_ x e. X ( { x } X. C ) ) : U_ x e. X ( { x } X. C ) --> _V -> ( 2nd |` U_ x e. X ( { x } X. C ) ) Fn U_ x e. X ( { x } X. C ) )
47 45 46 mp1i 
 |-  ( ph -> ( 2nd |` U_ x e. X ( { x } X. C ) ) Fn U_ x e. X ( { x } X. C ) )
48 djussxp2 
 |-  U_ x e. X ( { x } X. C ) C_ ( X X. U_ x e. X C )
49 imass2 
 |-  ( U_ x e. X ( { x } X. C ) C_ ( X X. U_ x e. X C ) -> ( 2nd " U_ x e. X ( { x } X. C ) ) C_ ( 2nd " ( X X. U_ x e. X C ) ) )
50 48 49 ax-mp 
 |-  ( 2nd " U_ x e. X ( { x } X. C ) ) C_ ( 2nd " ( X X. U_ x e. X C ) )
51 ima0 
 |-  ( 2nd " (/) ) = (/)
52 xpeq1 
 |-  ( X = (/) -> ( X X. U_ x e. X C ) = ( (/) X. U_ x e. X C ) )
53 0xp 
 |-  ( (/) X. U_ x e. X C ) = (/)
54 52 53 eqtrdi 
 |-  ( X = (/) -> ( X X. U_ x e. X C ) = (/) )
55 54 imaeq2d 
 |-  ( X = (/) -> ( 2nd " ( X X. U_ x e. X C ) ) = ( 2nd " (/) ) )
56 iuneq1 
 |-  ( X = (/) -> U_ x e. X C = U_ x e. (/) C )
57 0iun 
 |-  U_ x e. (/) C = (/)
58 56 57 eqtrdi 
 |-  ( X = (/) -> U_ x e. X C = (/) )
59 51 55 58 3eqtr4a 
 |-  ( X = (/) -> ( 2nd " ( X X. U_ x e. X C ) ) = U_ x e. X C )
60 59 adantl 
 |-  ( ( ph /\ X = (/) ) -> ( 2nd " ( X X. U_ x e. X C ) ) = U_ x e. X C )
61 2ndimaxp 
 |-  ( X =/= (/) -> ( 2nd " ( X X. U_ x e. X C ) ) = U_ x e. X C )
62 61 adantl 
 |-  ( ( ph /\ X =/= (/) ) -> ( 2nd " ( X X. U_ x e. X C ) ) = U_ x e. X C )
63 60 62 pm2.61dane 
 |-  ( ph -> ( 2nd " ( X X. U_ x e. X C ) ) = U_ x e. X C )
64 63 9 eqtrd 
 |-  ( ph -> ( 2nd " ( X X. U_ x e. X C ) ) = A )
65 50 64 sseqtrid 
 |-  ( ph -> ( 2nd " U_ x e. X ( { x } X. C ) ) C_ A )
66 resssxp 
 |-  ( ( 2nd " U_ x e. X ( { x } X. C ) ) C_ A <-> ( 2nd |` U_ x e. X ( { x } X. C ) ) C_ ( U_ x e. X ( { x } X. C ) X. A ) )
67 65 66 sylib 
 |-  ( ph -> ( 2nd |` U_ x e. X ( { x } X. C ) ) C_ ( U_ x e. X ( { x } X. C ) X. A ) )
68 dff2 
 |-  ( ( 2nd |` U_ x e. X ( { x } X. C ) ) : U_ x e. X ( { x } X. C ) --> A <-> ( ( 2nd |` U_ x e. X ( { x } X. C ) ) Fn U_ x e. X ( { x } X. C ) /\ ( 2nd |` U_ x e. X ( { x } X. C ) ) C_ ( U_ x e. X ( { x } X. C ) X. A ) ) )
69 47 67 68 sylanbrc 
 |-  ( ph -> ( 2nd |` U_ x e. X ( { x } X. C ) ) : U_ x e. X ( { x } X. C ) --> A )
70 6 69 fcod 
 |-  ( ph -> ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) : U_ x e. X ( { x } X. C ) --> B )
71 10 4 5 8 9 2ndresdju 
 |-  ( ph -> ( 2nd |` U_ x e. X ( { x } X. C ) ) : U_ x e. X ( { x } X. C ) -1-1-> A )
72 2 fvexi 
 |-  .0. e. _V
73 72 a1i 
 |-  ( ph -> .0. e. _V )
74 6 4 fexd 
 |-  ( ph -> F e. _V )
75 7 71 73 74 fsuppco 
 |-  ( ph -> ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) finSupp .0. )
76 1 2 3 25 30 5 39 70 75 gsum2d 
 |-  ( ph -> ( G gsum ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) ) = ( G gsum ( y e. X |-> ( G gsum ( z e. ( U_ x e. X ( { x } X. C ) " { y } ) |-> ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) ) ) ) ) )
77 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
78 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
79 5 21 77 78 iunsnima2 
 |-  ( ( ph /\ y e. X ) -> ( U_ x e. X ( { x } X. C ) " { y } ) = [_ y / x ]_ C )
80 df-ov 
 |-  ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) = ( ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) ` <. y , z >. )
81 69 ad2antrr 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> ( 2nd |` U_ x e. X ( { x } X. C ) ) : U_ x e. X ( { x } X. C ) --> A )
82 simplr 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> y e. X )
83 vsnid 
 |-  y e. { y }
84 83 a1i 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> y e. { y } )
85 79 eleq2d 
 |-  ( ( ph /\ y e. X ) -> ( z e. ( U_ x e. X ( { x } X. C ) " { y } ) <-> z e. [_ y / x ]_ C ) )
86 85 biimpa 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> z e. [_ y / x ]_ C )
87 84 86 opelxpd 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> <. y , z >. e. ( { y } X. [_ y / x ]_ C ) )
88 nfcv 
 |-  F/_ x { y }
89 88 77 nfxp 
 |-  F/_ x ( { y } X. [_ y / x ]_ C )
90 89 nfel2 
 |-  F/ x <. y , z >. e. ( { y } X. [_ y / x ]_ C )
91 sneq 
 |-  ( x = y -> { x } = { y } )
92 91 78 xpeq12d 
 |-  ( x = y -> ( { x } X. C ) = ( { y } X. [_ y / x ]_ C ) )
93 92 eleq2d 
 |-  ( x = y -> ( <. y , z >. e. ( { x } X. C ) <-> <. y , z >. e. ( { y } X. [_ y / x ]_ C ) ) )
94 90 93 rspce 
 |-  ( ( y e. X /\ <. y , z >. e. ( { y } X. [_ y / x ]_ C ) ) -> E. x e. X <. y , z >. e. ( { x } X. C ) )
95 82 87 94 syl2anc 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> E. x e. X <. y , z >. e. ( { x } X. C ) )
96 eliun 
 |-  ( <. y , z >. e. U_ x e. X ( { x } X. C ) <-> E. x e. X <. y , z >. e. ( { x } X. C ) )
97 95 96 sylibr 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> <. y , z >. e. U_ x e. X ( { x } X. C ) )
98 81 97 fvco3d 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> ( ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) ` <. y , z >. ) = ( F ` ( ( 2nd |` U_ x e. X ( { x } X. C ) ) ` <. y , z >. ) ) )
99 97 fvresd 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> ( ( 2nd |` U_ x e. X ( { x } X. C ) ) ` <. y , z >. ) = ( 2nd ` <. y , z >. ) )
100 vex 
 |-  y e. _V
101 vex 
 |-  z e. _V
102 100 101 op2nd 
 |-  ( 2nd ` <. y , z >. ) = z
103 99 102 eqtrdi 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> ( ( 2nd |` U_ x e. X ( { x } X. C ) ) ` <. y , z >. ) = z )
104 103 fveq2d 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> ( F ` ( ( 2nd |` U_ x e. X ( { x } X. C ) ) ` <. y , z >. ) ) = ( F ` z ) )
105 98 104 eqtrd 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> ( ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) ` <. y , z >. ) = ( F ` z ) )
106 80 105 eqtrid 
 |-  ( ( ( ph /\ y e. X ) /\ z e. ( U_ x e. X ( { x } X. C ) " { y } ) ) -> ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) = ( F ` z ) )
107 79 106 mpteq12dva 
 |-  ( ( ph /\ y e. X ) -> ( z e. ( U_ x e. X ( { x } X. C ) " { y } ) |-> ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) ) = ( z e. [_ y / x ]_ C |-> ( F ` z ) ) )
108 6 adantr 
 |-  ( ( ph /\ y e. X ) -> F : A --> B )
109 imassrn 
 |-  ( U_ x e. X ( { x } X. C ) " { y } ) C_ ran U_ x e. X ( { x } X. C )
110 9 xpeq2d 
 |-  ( ph -> ( X X. U_ x e. X C ) = ( X X. A ) )
111 48 110 sseqtrid 
 |-  ( ph -> U_ x e. X ( { x } X. C ) C_ ( X X. A ) )
112 rnss 
 |-  ( U_ x e. X ( { x } X. C ) C_ ( X X. A ) -> ran U_ x e. X ( { x } X. C ) C_ ran ( X X. A ) )
113 111 112 syl 
 |-  ( ph -> ran U_ x e. X ( { x } X. C ) C_ ran ( X X. A ) )
114 113 adantr 
 |-  ( ( ph /\ y e. X ) -> ran U_ x e. X ( { x } X. C ) C_ ran ( X X. A ) )
115 rnxpss 
 |-  ran ( X X. A ) C_ A
116 114 115 sstrdi 
 |-  ( ( ph /\ y e. X ) -> ran U_ x e. X ( { x } X. C ) C_ A )
117 109 116 sstrid 
 |-  ( ( ph /\ y e. X ) -> ( U_ x e. X ( { x } X. C ) " { y } ) C_ A )
118 79 117 eqsstrrd 
 |-  ( ( ph /\ y e. X ) -> [_ y / x ]_ C C_ A )
119 108 118 feqresmpt 
 |-  ( ( ph /\ y e. X ) -> ( F |` [_ y / x ]_ C ) = ( z e. [_ y / x ]_ C |-> ( F ` z ) ) )
120 107 119 eqtr4d 
 |-  ( ( ph /\ y e. X ) -> ( z e. ( U_ x e. X ( { x } X. C ) " { y } ) |-> ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) ) = ( F |` [_ y / x ]_ C ) )
121 120 oveq2d 
 |-  ( ( ph /\ y e. X ) -> ( G gsum ( z e. ( U_ x e. X ( { x } X. C ) " { y } ) |-> ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) ) ) = ( G gsum ( F |` [_ y / x ]_ C ) ) )
122 121 mpteq2dva 
 |-  ( ph -> ( y e. X |-> ( G gsum ( z e. ( U_ x e. X ( { x } X. C ) " { y } ) |-> ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) ) ) ) = ( y e. X |-> ( G gsum ( F |` [_ y / x ]_ C ) ) ) )
123 nfcv 
 |-  F/_ y ( G gsum ( F |` C ) )
124 nfcv 
 |-  F/_ x G
125 nfcv 
 |-  F/_ x gsum
126 nfcv 
 |-  F/_ x F
127 126 77 nfres 
 |-  F/_ x ( F |` [_ y / x ]_ C )
128 124 125 127 nfov 
 |-  F/_ x ( G gsum ( F |` [_ y / x ]_ C ) )
129 78 reseq2d 
 |-  ( x = y -> ( F |` C ) = ( F |` [_ y / x ]_ C ) )
130 129 oveq2d 
 |-  ( x = y -> ( G gsum ( F |` C ) ) = ( G gsum ( F |` [_ y / x ]_ C ) ) )
131 123 128 130 cbvmpt 
 |-  ( x e. X |-> ( G gsum ( F |` C ) ) ) = ( y e. X |-> ( G gsum ( F |` [_ y / x ]_ C ) ) )
132 122 131 eqtr4di 
 |-  ( ph -> ( y e. X |-> ( G gsum ( z e. ( U_ x e. X ( { x } X. C ) " { y } ) |-> ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) ) ) ) = ( x e. X |-> ( G gsum ( F |` C ) ) ) )
133 132 oveq2d 
 |-  ( ph -> ( G gsum ( y e. X |-> ( G gsum ( z e. ( U_ x e. X ( { x } X. C ) " { y } ) |-> ( y ( F o. ( 2nd |` U_ x e. X ( { x } X. C ) ) ) z ) ) ) ) ) = ( G gsum ( x e. X |-> ( G gsum ( F |` C ) ) ) ) )
134 12 76 133 3eqtrd 
 |-  ( ph -> ( G gsum F ) = ( G gsum ( x e. X |-> ( G gsum ( F |` C ) ) ) ) )