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

Metamath Proof Explorer

Theorem gsumzsubmcl

Description: Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 24-Apr-2016) (Revised by AV, 3-Jun-2019)

Ref Expression
Hypotheses gsumzsubmcl.0 
|- .0. = ( 0g ` G )
gsumzsubmcl.z 
|- Z = ( Cntz ` G )
gsumzsubmcl.g 
|- ( ph -> G e. Mnd )
gsumzsubmcl.a 
|- ( ph -> A e. V )
gsumzsubmcl.s 
|- ( ph -> S e. ( SubMnd ` G ) )
gsumzsubmcl.f 
|- ( ph -> F : A --> S )
gsumzsubmcl.c 
|- ( ph -> ran F C_ ( Z ` ran F ) )
gsumzsubmcl.w 
|- ( ph -> F finSupp .0. )
Assertion gsumzsubmcl 
|- ( ph -> ( G gsum F ) e. S )

Proof

Step Hyp Ref Expression
1 gsumzsubmcl.0 
 |-  .0. = ( 0g ` G )
2 gsumzsubmcl.z 
 |-  Z = ( Cntz ` G )
3 gsumzsubmcl.g 
 |-  ( ph -> G e. Mnd )
4 gsumzsubmcl.a 
 |-  ( ph -> A e. V )
5 gsumzsubmcl.s 
 |-  ( ph -> S e. ( SubMnd ` G ) )
6 gsumzsubmcl.f 
 |-  ( ph -> F : A --> S )
7 gsumzsubmcl.c 
 |-  ( ph -> ran F C_ ( Z ` ran F ) )
8 gsumzsubmcl.w 
 |-  ( ph -> F finSupp .0. )
9 eqid 
 |-  ( Base ` ( G |`s S ) ) = ( Base ` ( G |`s S ) )
10 eqid 
 |-  ( 0g ` ( G |`s S ) ) = ( 0g ` ( G |`s S ) )
11 eqid 
 |-  ( Cntz ` ( G |`s S ) ) = ( Cntz ` ( G |`s S ) )
12 eqid 
 |-  ( G |`s S ) = ( G |`s S )
13 12 submmnd 
 |-  ( S e. ( SubMnd ` G ) -> ( G |`s S ) e. Mnd )
14 5 13 syl 
 |-  ( ph -> ( G |`s S ) e. Mnd )
15 12 submbas 
 |-  ( S e. ( SubMnd ` G ) -> S = ( Base ` ( G |`s S ) ) )
16 5 15 syl 
 |-  ( ph -> S = ( Base ` ( G |`s S ) ) )
17 16 feq3d 
 |-  ( ph -> ( F : A --> S <-> F : A --> ( Base ` ( G |`s S ) ) ) )
18 6 17 mpbid 
 |-  ( ph -> F : A --> ( Base ` ( G |`s S ) ) )
19 6 frnd 
 |-  ( ph -> ran F C_ S )
20 7 19 ssind 
 |-  ( ph -> ran F C_ ( ( Z ` ran F ) i^i S ) )
21 12 2 11 resscntz 
 |-  ( ( S e. ( SubMnd ` G ) /\ ran F C_ S ) -> ( ( Cntz ` ( G |`s S ) ) ` ran F ) = ( ( Z ` ran F ) i^i S ) )
22 5 19 21 syl2anc 
 |-  ( ph -> ( ( Cntz ` ( G |`s S ) ) ` ran F ) = ( ( Z ` ran F ) i^i S ) )
23 20 22 sseqtrrd 
 |-  ( ph -> ran F C_ ( ( Cntz ` ( G |`s S ) ) ` ran F ) )
24 12 1 subm0 
 |-  ( S e. ( SubMnd ` G ) -> .0. = ( 0g ` ( G |`s S ) ) )
25 5 24 syl 
 |-  ( ph -> .0. = ( 0g ` ( G |`s S ) ) )
26 8 25 breqtrd 
 |-  ( ph -> F finSupp ( 0g ` ( G |`s S ) ) )
27 9 10 11 14 4 18 23 26 gsumzcl 
 |-  ( ph -> ( ( G |`s S ) gsum F ) e. ( Base ` ( G |`s S ) ) )
28 4 5 6 12 gsumsubm 
 |-  ( ph -> ( G gsum F ) = ( ( G |`s S ) gsum F ) )
29 27 28 16 3eltr4d 
 |-  ( ph -> ( G gsum F ) e. S )