Metamath Proof Explorer

Theorem gsumsub

Description: The difference of two group sums. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsumsub.b 
|- B = ( Base ` G )
gsumsub.z 
|- .0. = ( 0g ` G )
gsumsub.m 
|- .- = ( -g ` G )
gsumsub.g 
|- ( ph -> G e. Abel )
gsumsub.a 
|- ( ph -> A e. V )
gsumsub.f 
|- ( ph -> F : A --> B )
gsumsub.h 
|- ( ph -> H : A --> B )
gsumsub.fn 
|- ( ph -> F finSupp .0. )
gsumsub.hn 
|- ( ph -> H finSupp .0. )
Assertion gsumsub 
|- ( ph -> ( G gsum ( F oF .- H ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )

Proof

Step Hyp Ref Expression
1 gsumsub.b 
 |-  B = ( Base ` G )
2 gsumsub.z 
 |-  .0. = ( 0g ` G )
3 gsumsub.m 
 |-  .- = ( -g ` G )
4 gsumsub.g 
 |-  ( ph -> G e. Abel )
5 gsumsub.a 
 |-  ( ph -> A e. V )
6 gsumsub.f 
 |-  ( ph -> F : A --> B )
7 gsumsub.h 
 |-  ( ph -> H : A --> B )
8 gsumsub.fn 
 |-  ( ph -> F finSupp .0. )
9 gsumsub.hn 
 |-  ( ph -> H finSupp .0. )
10 eqid 
 |-  ( +g ` G ) = ( +g ` G )
11 ablcmn 
 |-  ( G e. Abel -> G e. CMnd )
12 4 11 syl 
 |-  ( ph -> G e. CMnd )
13 eqid 
 |-  ( invg ` G ) = ( invg ` G )
14 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
15 4 14 syl 
 |-  ( ph -> G e. Grp )
16 1 13 15 grpinvf1o 
 |-  ( ph -> ( invg ` G ) : B -1-1-onto-> B )
17 f1of 
 |-  ( ( invg ` G ) : B -1-1-onto-> B -> ( invg ` G ) : B --> B )
18 16 17 syl 
 |-  ( ph -> ( invg ` G ) : B --> B )
19 fco 
 |-  ( ( ( invg ` G ) : B --> B /\ H : A --> B ) -> ( ( invg ` G ) o. H ) : A --> B )
20 18 7 19 syl2anc 
 |-  ( ph -> ( ( invg ` G ) o. H ) : A --> B )
21 2 fvexi 
 |-  .0. e. _V
22 21 a1i 
 |-  ( ph -> .0. e. _V )
23 1 fvexi 
 |-  B e. _V
24 23 a1i 
 |-  ( ph -> B e. _V )
25 2 13 grpinvid 
 |-  ( G e. Grp -> ( ( invg ` G ) ` .0. ) = .0. )
26 15 25 syl 
 |-  ( ph -> ( ( invg ` G ) ` .0. ) = .0. )
27 22 7 18 5 24 9 26 fsuppco2 
 |-  ( ph -> ( ( invg ` G ) o. H ) finSupp .0. )
28 1 2 10 12 5 6 20 8 27 gsumadd 
 |-  ( ph -> ( G gsum ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) ) = ( ( G gsum F ) ( +g ` G ) ( G gsum ( ( invg ` G ) o. H ) ) ) )
29 1 2 13 4 5 7 9 gsuminv 
 |-  ( ph -> ( G gsum ( ( invg ` G ) o. H ) ) = ( ( invg ` G ) ` ( G gsum H ) ) )
30 29 oveq2d 
 |-  ( ph -> ( ( G gsum F ) ( +g ` G ) ( G gsum ( ( invg ` G ) o. H ) ) ) = ( ( G gsum F ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum H ) ) ) )
31 28 30 eqtrd 
 |-  ( ph -> ( G gsum ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) ) = ( ( G gsum F ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum H ) ) ) )
32 6 ffvelcdmda 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. B )
33 7 ffvelcdmda 
 |-  ( ( ph /\ k e. A ) -> ( H ` k ) e. B )
34 1 10 13 3 grpsubval 
 |-  ( ( ( F ` k ) e. B /\ ( H ` k ) e. B ) -> ( ( F ` k ) .- ( H ` k ) ) = ( ( F ` k ) ( +g ` G ) ( ( invg ` G ) ` ( H ` k ) ) ) )
35 32 33 34 syl2anc 
 |-  ( ( ph /\ k e. A ) -> ( ( F ` k ) .- ( H ` k ) ) = ( ( F ` k ) ( +g ` G ) ( ( invg ` G ) ` ( H ` k ) ) ) )
36 35 mpteq2dva 
 |-  ( ph -> ( k e. A |-> ( ( F ` k ) .- ( H ` k ) ) ) = ( k e. A |-> ( ( F ` k ) ( +g ` G ) ( ( invg ` G ) ` ( H ` k ) ) ) ) )
37 6 feqmptd 
 |-  ( ph -> F = ( k e. A |-> ( F ` k ) ) )
38 7 feqmptd 
 |-  ( ph -> H = ( k e. A |-> ( H ` k ) ) )
39 5 32 33 37 38 offval2 
 |-  ( ph -> ( F oF .- H ) = ( k e. A |-> ( ( F ` k ) .- ( H ` k ) ) ) )
40 fvexd 
 |-  ( ( ph /\ k e. A ) -> ( ( invg ` G ) ` ( H ` k ) ) e. _V )
41 18 feqmptd 
 |-  ( ph -> ( invg ` G ) = ( x e. B |-> ( ( invg ` G ) ` x ) ) )
42 fveq2 
 |-  ( x = ( H ` k ) -> ( ( invg ` G ) ` x ) = ( ( invg ` G ) ` ( H ` k ) ) )
43 33 38 41 42 fmptco 
 |-  ( ph -> ( ( invg ` G ) o. H ) = ( k e. A |-> ( ( invg ` G ) ` ( H ` k ) ) ) )
44 5 32 40 37 43 offval2 
 |-  ( ph -> ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) = ( k e. A |-> ( ( F ` k ) ( +g ` G ) ( ( invg ` G ) ` ( H ` k ) ) ) ) )
45 36 39 44 3eqtr4d 
 |-  ( ph -> ( F oF .- H ) = ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) )
46 45 oveq2d 
 |-  ( ph -> ( G gsum ( F oF .- H ) ) = ( G gsum ( F oF ( +g ` G ) ( ( invg ` G ) o. H ) ) ) )
47 1 2 12 5 6 8 gsumcl 
 |-  ( ph -> ( G gsum F ) e. B )
48 1 2 12 5 7 9 gsumcl 
 |-  ( ph -> ( G gsum H ) e. B )
49 1 10 13 3 grpsubval 
 |-  ( ( ( G gsum F ) e. B /\ ( G gsum H ) e. B ) -> ( ( G gsum F ) .- ( G gsum H ) ) = ( ( G gsum F ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum H ) ) ) )
50 47 48 49 syl2anc 
 |-  ( ph -> ( ( G gsum F ) .- ( G gsum H ) ) = ( ( G gsum F ) ( +g ` G ) ( ( invg ` G ) ` ( G gsum H ) ) ) )
51 31 46 50 3eqtr4d 
 |-  ( ph -> ( G gsum ( F oF .- H ) ) = ( ( G gsum F ) .- ( G gsum H ) ) )