Step |
Hyp |
Ref |
Expression |
1 |
|
gsummptfsadd.b |
|- B = ( Base ` G ) |
2 |
|
gsummptfsadd.z |
|- .0. = ( 0g ` G ) |
3 |
|
gsummptfsadd.p |
|- .+ = ( +g ` G ) |
4 |
|
gsummptfsadd.g |
|- ( ph -> G e. CMnd ) |
5 |
|
gsummptfsadd.a |
|- ( ph -> A e. V ) |
6 |
|
gsummptfsadd.c |
|- ( ( ph /\ x e. A ) -> C e. B ) |
7 |
|
gsummptfsadd.d |
|- ( ( ph /\ x e. A ) -> D e. B ) |
8 |
|
gsummptfsadd.f |
|- ( ph -> F = ( x e. A |-> C ) ) |
9 |
|
gsummptfsadd.h |
|- ( ph -> H = ( x e. A |-> D ) ) |
10 |
|
gsummptfsadd.w |
|- ( ph -> F finSupp .0. ) |
11 |
|
gsummptfsadd.v |
|- ( ph -> H finSupp .0. ) |
12 |
5 6 7 8 9
|
offval2 |
|- ( ph -> ( F oF .+ H ) = ( x e. A |-> ( C .+ D ) ) ) |
13 |
12
|
eqcomd |
|- ( ph -> ( x e. A |-> ( C .+ D ) ) = ( F oF .+ H ) ) |
14 |
13
|
oveq2d |
|- ( ph -> ( G gsum ( x e. A |-> ( C .+ D ) ) ) = ( G gsum ( F oF .+ H ) ) ) |
15 |
8 6
|
fmpt3d |
|- ( ph -> F : A --> B ) |
16 |
9 7
|
fmpt3d |
|- ( ph -> H : A --> B ) |
17 |
1 2 3 4 5 15 16 10 11
|
gsumadd |
|- ( ph -> ( G gsum ( F oF .+ H ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) |
18 |
14 17
|
eqtrd |
|- ( ph -> ( G gsum ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) |