Metamath Proof Explorer


Theorem gsumadd

Description: The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Mario Carneiro, 25-Apr-2016) (Revised by AV, 5-Jun-2019)

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

Proof

Step Hyp Ref Expression
1 gsumadd.b
 |-  B = ( Base ` G )
2 gsumadd.z
 |-  .0. = ( 0g ` G )
3 gsumadd.p
 |-  .+ = ( +g ` G )
4 gsumadd.g
 |-  ( ph -> G e. CMnd )
5 gsumadd.a
 |-  ( ph -> A e. V )
6 gsumadd.f
 |-  ( ph -> F : A --> B )
7 gsumadd.h
 |-  ( ph -> H : A --> B )
8 gsumadd.fn
 |-  ( ph -> F finSupp .0. )
9 gsumadd.hn
 |-  ( ph -> H finSupp .0. )
10 eqid
 |-  ( Cntz ` G ) = ( Cntz ` G )
11 cmnmnd
 |-  ( G e. CMnd -> G e. Mnd )
12 4 11 syl
 |-  ( ph -> G e. Mnd )
13 1 submid
 |-  ( G e. Mnd -> B e. ( SubMnd ` G ) )
14 12 13 syl
 |-  ( ph -> B e. ( SubMnd ` G ) )
15 ssid
 |-  B C_ B
16 1 10 cntzcmn
 |-  ( ( G e. CMnd /\ B C_ B ) -> ( ( Cntz ` G ) ` B ) = B )
17 4 15 16 sylancl
 |-  ( ph -> ( ( Cntz ` G ) ` B ) = B )
18 15 17 sseqtrrid
 |-  ( ph -> B C_ ( ( Cntz ` G ) ` B ) )
19 1 2 3 10 12 5 8 9 14 18 6 7 gsumzadd
 |-  ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) )