# Metamath Proof Explorer

## Theorem gsummptf1o

Description: Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018)

Ref Expression
Hypotheses gsummptf1o.x ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{H}$
gsummptf1o.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
gsummptf1o.z
gsummptf1o.i ${⊢}{x}={E}\to {C}={H}$
gsummptf1o.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
gsummptf1o.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
gsummptf1o.d ${⊢}{\phi }\to {F}\subseteq {B}$
gsummptf1o.f ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {F}$
gsummptf1o.e ${⊢}\left({\phi }\wedge {y}\in {D}\right)\to {E}\in {A}$
gsummptf1o.h ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}{x}={E}$
Assertion gsummptf1o ${⊢}{\phi }\to \underset{{x}\in {A}}{{\sum }_{{G}}}{C}=\underset{{y}\in {D}}{{\sum }_{{G}}}{H}$

### Proof

Step Hyp Ref Expression
1 gsummptf1o.x ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{H}$
2 gsummptf1o.b ${⊢}{B}={\mathrm{Base}}_{{G}}$
3 gsummptf1o.z
4 gsummptf1o.i ${⊢}{x}={E}\to {C}={H}$
5 gsummptf1o.g ${⊢}{\phi }\to {G}\in \mathrm{CMnd}$
6 gsummptf1o.a ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
7 gsummptf1o.d ${⊢}{\phi }\to {F}\subseteq {B}$
8 gsummptf1o.f ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {F}$
9 gsummptf1o.e ${⊢}\left({\phi }\wedge {y}\in {D}\right)\to {E}\in {A}$
10 gsummptf1o.h ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}{x}={E}$
11 7 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\subseteq {B}$
12 11 8 sseldd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {B}$
13 12 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right):{A}⟶{B}$
14 eqid ${⊢}\left({x}\in {A}⟼{C}\right)=\left({x}\in {A}⟼{C}\right)$
15 3 fvexi
16 15 a1i
17 14 6 12 16 fsuppmptdm
18 9 ralrimiva ${⊢}{\phi }\to \forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{E}\in {A}$
19 10 ralrimiva ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}{x}={E}$
20 eqid ${⊢}\left({y}\in {D}⟼{E}\right)=\left({y}\in {D}⟼{E}\right)$
21 20 f1ompt ${⊢}\left({y}\in {D}⟼{E}\right):{D}\underset{1-1 onto}{⟶}{A}↔\left(\forall {y}\in {D}\phantom{\rule{.4em}{0ex}}{E}\in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists !{y}\in {D}\phantom{\rule{.4em}{0ex}}{x}={E}\right)$
22 18 19 21 sylanbrc ${⊢}{\phi }\to \left({y}\in {D}⟼{E}\right):{D}\underset{1-1 onto}{⟶}{A}$
23 2 3 5 6 13 17 22 gsumf1o ${⊢}{\phi }\to \underset{{x}\in {A}}{{\sum }_{{G}}}{C}={\sum }_{{G}}\left(\left({x}\in {A}⟼{C}\right)\circ \left({y}\in {D}⟼{E}\right)\right)$
24 eqidd ${⊢}{\phi }\to \left({y}\in {D}⟼{E}\right)=\left({y}\in {D}⟼{E}\right)$
25 eqidd ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)=\left({x}\in {A}⟼{C}\right)$
26 18 24 25 fmptcos
27 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {y}\in {D}\right)$
28 1 a1i ${⊢}\left({\phi }\wedge {y}\in {D}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{H}$
29 4 adantl ${⊢}\left(\left({\phi }\wedge {y}\in {D}\right)\wedge {x}={E}\right)\to {C}={H}$
30 27 28 9 29 csbiedf
31 30 mpteq2dva
32 26 31 eqtrd ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)\circ \left({y}\in {D}⟼{E}\right)=\left({y}\in {D}⟼{H}\right)$
33 32 oveq2d ${⊢}{\phi }\to {\sum }_{{G}}\left(\left({x}\in {A}⟼{C}\right)\circ \left({y}\in {D}⟼{E}\right)\right)=\underset{{y}\in {D}}{{\sum }_{{G}}}{H}$
34 23 33 eqtrd ${⊢}{\phi }\to \underset{{x}\in {A}}{{\sum }_{{G}}}{C}=\underset{{y}\in {D}}{{\sum }_{{G}}}{H}$