Description: The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsummptfidmadd.b | |- B = ( Base ` G ) |
|
gsummptfidmadd.p | |- .+ = ( +g ` G ) |
||
gsummptfidmadd.g | |- ( ph -> G e. CMnd ) |
||
gsummptfidmadd.a | |- ( ph -> A e. Fin ) |
||
gsummptfidmadd.c | |- ( ( ph /\ x e. A ) -> C e. B ) |
||
gsummptfidmadd.d | |- ( ( ph /\ x e. A ) -> D e. B ) |
||
gsummptfidmadd.f | |- F = ( x e. A |-> C ) |
||
gsummptfidmadd.h | |- H = ( x e. A |-> D ) |
||
Assertion | gsummptfidmadd | |- ( ph -> ( G gsum ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsummptfidmadd.b | |- B = ( Base ` G ) |
|
2 | gsummptfidmadd.p | |- .+ = ( +g ` G ) |
|
3 | gsummptfidmadd.g | |- ( ph -> G e. CMnd ) |
|
4 | gsummptfidmadd.a | |- ( ph -> A e. Fin ) |
|
5 | gsummptfidmadd.c | |- ( ( ph /\ x e. A ) -> C e. B ) |
|
6 | gsummptfidmadd.d | |- ( ( ph /\ x e. A ) -> D e. B ) |
|
7 | gsummptfidmadd.f | |- F = ( x e. A |-> C ) |
|
8 | gsummptfidmadd.h | |- H = ( x e. A |-> D ) |
|
9 | eqid | |- ( 0g ` G ) = ( 0g ` G ) |
|
10 | 7 | a1i | |- ( ph -> F = ( x e. A |-> C ) ) |
11 | 8 | a1i | |- ( ph -> H = ( x e. A |-> D ) ) |
12 | fvexd | |- ( ph -> ( 0g ` G ) e. _V ) |
|
13 | 7 4 5 12 | fsuppmptdm | |- ( ph -> F finSupp ( 0g ` G ) ) |
14 | 8 4 6 12 | fsuppmptdm | |- ( ph -> H finSupp ( 0g ` G ) ) |
15 | 1 9 2 3 4 5 6 10 11 13 14 | gsummptfsadd | |- ( ph -> ( G gsum ( x e. A |-> ( C .+ D ) ) ) = ( ( G gsum F ) .+ ( G gsum H ) ) ) |