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