This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )