Description: Closure of a finite group sum. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 1-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsumzcl.b | |- B = ( Base ` G ) |
|
gsumzcl.0 | |- .0. = ( 0g ` G ) |
||
gsumzcl.z | |- Z = ( Cntz ` G ) |
||
gsumzcl.g | |- ( ph -> G e. Mnd ) |
||
gsumzcl.a | |- ( ph -> A e. V ) |
||
gsumzcl.f | |- ( ph -> F : A --> B ) |
||
gsumzcl.c | |- ( ph -> ran F C_ ( Z ` ran F ) ) |
||
gsumzcl.w | |- ( ph -> F finSupp .0. ) |
||
Assertion | gsumzcl | |- ( ph -> ( G gsum F ) e. B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsumzcl.b | |- B = ( Base ` G ) |
|
2 | gsumzcl.0 | |- .0. = ( 0g ` G ) |
|
3 | gsumzcl.z | |- Z = ( Cntz ` G ) |
|
4 | gsumzcl.g | |- ( ph -> G e. Mnd ) |
|
5 | gsumzcl.a | |- ( ph -> A e. V ) |
|
6 | gsumzcl.f | |- ( ph -> F : A --> B ) |
|
7 | gsumzcl.c | |- ( ph -> ran F C_ ( Z ` ran F ) ) |
|
8 | gsumzcl.w | |- ( ph -> F finSupp .0. ) |
|
9 | 8 | fsuppimpd | |- ( ph -> ( F supp .0. ) e. Fin ) |
10 | 1 2 3 4 5 6 7 9 | gsumzcl2 | |- ( ph -> ( G gsum F ) e. B ) |