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 
|- F/_ x H
gsummptf1o.b 
|- B = ( Base ` G )
gsummptf1o.z 
|- .0. = ( 0g ` G )
gsummptf1o.i 
|- ( x = E -> C = H )
gsummptf1o.g 
|- ( ph -> G e. CMnd )
gsummptf1o.a 
|- ( ph -> A e. Fin )
gsummptf1o.d 
|- ( ph -> F C_ B )
gsummptf1o.f 
|- ( ( ph /\ x e. A ) -> C e. F )
gsummptf1o.e 
|- ( ( ph /\ y e. D ) -> E e. A )
gsummptf1o.h 
|- ( ( ph /\ x e. A ) -> E! y e. D x = E )
Assertion gsummptf1o 
|- ( ph -> ( G gsum ( x e. A |-> C ) ) = ( G gsum ( y e. D |-> H ) ) )

Proof

Step Hyp Ref Expression
1 gsummptf1o.x 
 |-  F/_ x H
2 gsummptf1o.b 
 |-  B = ( Base ` G )
3 gsummptf1o.z 
 |-  .0. = ( 0g ` G )
4 gsummptf1o.i 
 |-  ( x = E -> C = H )
5 gsummptf1o.g 
 |-  ( ph -> G e. CMnd )
6 gsummptf1o.a 
 |-  ( ph -> A e. Fin )
7 gsummptf1o.d 
 |-  ( ph -> F C_ B )
8 gsummptf1o.f 
 |-  ( ( ph /\ x e. A ) -> C e. F )
9 gsummptf1o.e 
 |-  ( ( ph /\ y e. D ) -> E e. A )
10 gsummptf1o.h 
 |-  ( ( ph /\ x e. A ) -> E! y e. D x = E )
11 7 adantr 
 |-  ( ( ph /\ x e. A ) -> F C_ B )
12 11 8 sseldd 
 |-  ( ( ph /\ x e. A ) -> C e. B )
13 12 fmpttd 
 |-  ( ph -> ( x e. A |-> C ) : A --> B )
14 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
15 3 fvexi 
 |-  .0. e. _V
16 15 a1i 
 |-  ( ph -> .0. e. _V )
17 14 6 12 16 fsuppmptdm 
 |-  ( ph -> ( x e. A |-> C ) finSupp .0. )
18 9 ralrimiva 
 |-  ( ph -> A. y e. D E e. A )
19 10 ralrimiva 
 |-  ( ph -> A. x e. A E! y e. D x = E )
20 eqid 
 |-  ( y e. D |-> E ) = ( y e. D |-> E )
21 20 f1ompt 
 |-  ( ( y e. D |-> E ) : D -1-1-onto-> A <-> ( A. y e. D E e. A /\ A. x e. A E! y e. D x = E ) )
22 18 19 21 sylanbrc 
 |-  ( ph -> ( y e. D |-> E ) : D -1-1-onto-> A )
23 2 3 5 6 13 17 22 gsumf1o 
 |-  ( ph -> ( G gsum ( x e. A |-> C ) ) = ( G gsum ( ( x e. A |-> C ) o. ( y e. D |-> E ) ) ) )
24 eqidd 
 |-  ( ph -> ( y e. D |-> E ) = ( y e. D |-> E ) )
25 eqidd 
 |-  ( ph -> ( x e. A |-> C ) = ( x e. A |-> C ) )
26 18 24 25 fmptcos 
 |-  ( ph -> ( ( x e. A |-> C ) o. ( y e. D |-> E ) ) = ( y e. D |-> [_ E / x ]_ C ) )
27 nfv 
 |-  F/ x ( ph /\ y e. D )
28 1 a1i 
 |-  ( ( ph /\ y e. D ) -> F/_ x H )
29 4 adantl 
 |-  ( ( ( ph /\ y e. D ) /\ x = E ) -> C = H )
30 27 28 9 29 csbiedf 
 |-  ( ( ph /\ y e. D ) -> [_ E / x ]_ C = H )
31 30 mpteq2dva 
 |-  ( ph -> ( y e. D |-> [_ E / x ]_ C ) = ( y e. D |-> H ) )
32 26 31 eqtrd 
 |-  ( ph -> ( ( x e. A |-> C ) o. ( y e. D |-> E ) ) = ( y e. D |-> H ) )
33 32 oveq2d 
 |-  ( ph -> ( G gsum ( ( x e. A |-> C ) o. ( y e. D |-> E ) ) ) = ( G gsum ( y e. D |-> H ) ) )
34 23 33 eqtrd 
 |-  ( ph -> ( G gsum ( x e. A |-> C ) ) = ( G gsum ( y e. D |-> H ) ) )