Metamath Proof Explorer

Theorem gsummptfsf1o

Description: Re-index a finite group sum using a bijection. A version of gsummptf1o expressed using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses gsummptfsf1o.x 
|- F/_ x H
gsummptfsf1o.b 
|- B = ( Base ` G )
gsummptfsf1o.z 
|- .0. = ( 0g ` G )
gsummptfsf1o.i 
|- ( x = E -> C = H )
gsummptfsf1o.g 
|- ( ph -> G e. CMnd )
gsummptfsf1o.1 
|- ( ph -> A e. V )
gsummptfsf1o.a 
|- ( ph -> ( x e. A |-> C ) finSupp .0. )
gsummptfsf1o.d 
|- ( ph -> F C_ B )
gsummptfsf1o.f 
|- ( ( ph /\ x e. A ) -> C e. F )
gsummptfsf1o.e 
|- ( ( ph /\ y e. D ) -> E e. A )
gsummptfsf1o.h 
|- ( ( ph /\ x e. A ) -> E! y e. D x = E )
Assertion gsummptfsf1o 
|- ( ph -> ( G gsum ( x e. A |-> C ) ) = ( G gsum ( y e. D |-> H ) ) )

Proof

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