Metamath Proof Explorer

Theorem tsmsgsum

Description: The convergent points of a finite topological group sum are the closure of the finite group sum operation. (Contributed by Mario Carneiro, 19-Sep-2015) (Revised by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmsid.b 
|- B = ( Base ` G )
tsmsid.z 
|- .0. = ( 0g ` G )
tsmsid.1 
|- ( ph -> G e. CMnd )
tsmsid.2 
|- ( ph -> G e. TopSp )
tsmsid.a 
|- ( ph -> A e. V )
tsmsid.f 
|- ( ph -> F : A --> B )
tsmsid.w 
|- ( ph -> F finSupp .0. )
tsmsgsum.j 
|- J = ( TopOpen ` G )
Assertion tsmsgsum 
|- ( ph -> ( G tsums F ) = ( ( cls ` J ) ` { ( G gsum F ) } ) )

Proof

Step Hyp Ref Expression
1 tsmsid.b 
 |-  B = ( Base ` G )
2 tsmsid.z 
 |-  .0. = ( 0g ` G )
3 tsmsid.1 
 |-  ( ph -> G e. CMnd )
4 tsmsid.2 
 |-  ( ph -> G e. TopSp )
5 tsmsid.a 
 |-  ( ph -> A e. V )
6 tsmsid.f 
 |-  ( ph -> F : A --> B )
7 tsmsid.w 
 |-  ( ph -> F finSupp .0. )
8 tsmsgsum.j 
 |-  J = ( TopOpen ` G )
9 1 8 istps 
 |-  ( G e. TopSp <-> J e. ( TopOn ` B ) )
10 4 9 sylib 
 |-  ( ph -> J e. ( TopOn ` B ) )
11 toponuni 
 |-  ( J e. ( TopOn ` B ) -> B = U. J )
12 10 11 syl 
 |-  ( ph -> B = U. J )
13 12 eleq2d 
 |-  ( ph -> ( x e. B <-> x e. U. J ) )
14 elfpw 
 |-  ( y e. ( ~P A i^i Fin ) <-> ( y C_ A /\ y e. Fin ) )
15 14 simplbi 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
16 15 adantl 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
17 suppssdm 
 |-  ( F supp .0. ) C_ dom F
18 17 6 fssdm 
 |-  ( ph -> ( F supp .0. ) C_ A )
19 18 ad2antrr 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) C_ A )
20 16 19 unssd 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) C_ A )
21 elinel2 
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
22 21 adantl 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
23 7 ad2antrr 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> F finSupp .0. )
24 23 fsuppimpd 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) e. Fin )
25 unfi 
 |-  ( ( y e. Fin /\ ( F supp .0. ) e. Fin ) -> ( y u. ( F supp .0. ) ) e. Fin )
26 22 24 25 syl2anc 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) e. Fin )
27 elfpw 
 |-  ( ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) <-> ( ( y u. ( F supp .0. ) ) C_ A /\ ( y u. ( F supp .0. ) ) e. Fin ) )
28 20 26 27 sylanbrc 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) )
29 ssun1 
 |-  y C_ ( y u. ( F supp .0. ) )
30 id 
 |-  ( z = ( y u. ( F supp .0. ) ) -> z = ( y u. ( F supp .0. ) ) )
31 29 30 sseqtrrid 
 |-  ( z = ( y u. ( F supp .0. ) ) -> y C_ z )
32 pm5.5 
 |-  ( y C_ z -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) )
33 31 32 syl 
 |-  ( z = ( y u. ( F supp .0. ) ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` z ) ) e. u ) )
34 reseq2 
 |-  ( z = ( y u. ( F supp .0. ) ) -> ( F |` z ) = ( F |` ( y u. ( F supp .0. ) ) ) )
35 34 oveq2d 
 |-  ( z = ( y u. ( F supp .0. ) ) -> ( G gsum ( F |` z ) ) = ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) )
36 35 eleq1d 
 |-  ( z = ( y u. ( F supp .0. ) ) -> ( ( G gsum ( F |` z ) ) e. u <-> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) )
37 33 36 bitrd 
 |-  ( z = ( y u. ( F supp .0. ) ) -> ( ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) )
38 37 rspcv 
 |-  ( ( y u. ( F supp .0. ) ) e. ( ~P A i^i Fin ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) )
39 28 38 syl 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u ) )
40 3 ad2antrr 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> G e. CMnd )
41 5 ad2antrr 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> A e. V )
42 6 ad2antrr 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> F : A --> B )
43 ssun2 
 |-  ( F supp .0. ) C_ ( y u. ( F supp .0. ) )
44 43 a1i 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( F supp .0. ) C_ ( y u. ( F supp .0. ) ) )
45 1 2 40 41 42 44 23 gsumres 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) = ( G gsum F ) )
46 45 eleq1d 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( G gsum ( F |` ( y u. ( F supp .0. ) ) ) ) e. u <-> ( G gsum F ) e. u ) )
47 39 46 sylibd 
 |-  ( ( ( ph /\ u e. J ) /\ y e. ( ~P A i^i Fin ) ) -> ( A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum F ) e. u ) )
48 47 rexlimdva 
 |-  ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) -> ( G gsum F ) e. u ) )
49 7 fsuppimpd 
 |-  ( ph -> ( F supp .0. ) e. Fin )
50 elfpw 
 |-  ( ( F supp .0. ) e. ( ~P A i^i Fin ) <-> ( ( F supp .0. ) C_ A /\ ( F supp .0. ) e. Fin ) )
51 18 49 50 sylanbrc 
 |-  ( ph -> ( F supp .0. ) e. ( ~P A i^i Fin ) )
52 3 ad2antrr 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> G e. CMnd )
53 5 ad2antrr 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> A e. V )
54 6 ad2antrr 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> F : A --> B )
55 simprr 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( F supp .0. ) C_ z )
56 7 ad2antrr 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> F finSupp .0. )
57 1 2 52 53 54 55 56 gsumres 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsum ( F |` z ) ) = ( G gsum F ) )
58 simplrr 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsum F ) e. u )
59 57 58 eqeltrd 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ ( z e. ( ~P A i^i Fin ) /\ ( F supp .0. ) C_ z ) ) -> ( G gsum ( F |` z ) ) e. u )
60 59 expr 
 |-  ( ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) /\ z e. ( ~P A i^i Fin ) ) -> ( ( F supp .0. ) C_ z -> ( G gsum ( F |` z ) ) e. u ) )
61 60 ralrimiva 
 |-  ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) -> A. z e. ( ~P A i^i Fin ) ( ( F supp .0. ) C_ z -> ( G gsum ( F |` z ) ) e. u ) )
62 sseq1 
 |-  ( y = ( F supp .0. ) -> ( y C_ z <-> ( F supp .0. ) C_ z ) )
63 62 rspceaimv 
 |-  ( ( ( F supp .0. ) e. ( ~P A i^i Fin ) /\ A. z e. ( ~P A i^i Fin ) ( ( F supp .0. ) C_ z -> ( G gsum ( F |` z ) ) e. u ) ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) )
64 51 61 63 syl2an2r 
 |-  ( ( ph /\ ( u e. J /\ ( G gsum F ) e. u ) ) -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) )
65 64 expr 
 |-  ( ( ph /\ u e. J ) -> ( ( G gsum F ) e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) )
66 48 65 impbid 
 |-  ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( G gsum F ) e. u ) )
67 disjsn 
 |-  ( ( u i^i { ( G gsum F ) } ) = (/) <-> -. ( G gsum F ) e. u )
68 67 necon2abii 
 |-  ( ( G gsum F ) e. u <-> ( u i^i { ( G gsum F ) } ) =/= (/) )
69 66 68 bitrdi 
 |-  ( ( ph /\ u e. J ) -> ( E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) <-> ( u i^i { ( G gsum F ) } ) =/= (/) ) )
70 69 imbi2d 
 |-  ( ( ph /\ u e. J ) -> ( ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) <-> ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) )
71 70 ralbidva 
 |-  ( ph -> ( A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) <-> A. u e. J ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) )
72 13 71 anbi12d 
 |-  ( ph -> ( ( x e. B /\ A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) ) )
73 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
74 1 8 73 3 4 5 6 eltsms 
 |-  ( ph -> ( x e. ( G tsums F ) <-> ( x e. B /\ A. u e. J ( x e. u -> E. y e. ( ~P A i^i Fin ) A. z e. ( ~P A i^i Fin ) ( y C_ z -> ( G gsum ( F |` z ) ) e. u ) ) ) ) )
75 topontop 
 |-  ( J e. ( TopOn ` B ) -> J e. Top )
76 10 75 syl 
 |-  ( ph -> J e. Top )
77 1 2 3 5 6 7 gsumcl 
 |-  ( ph -> ( G gsum F ) e. B )
78 77 snssd 
 |-  ( ph -> { ( G gsum F ) } C_ B )
79 78 12 sseqtrd 
 |-  ( ph -> { ( G gsum F ) } C_ U. J )
80 eqid 
 |-  U. J = U. J
81 80 elcls2 
 |-  ( ( J e. Top /\ { ( G gsum F ) } C_ U. J ) -> ( x e. ( ( cls ` J ) ` { ( G gsum F ) } ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) ) )
82 76 79 81 syl2anc 
 |-  ( ph -> ( x e. ( ( cls ` J ) ` { ( G gsum F ) } ) <-> ( x e. U. J /\ A. u e. J ( x e. u -> ( u i^i { ( G gsum F ) } ) =/= (/) ) ) ) )
83 72 74 82 3bitr4d 
 |-  ( ph -> ( x e. ( G tsums F ) <-> x e. ( ( cls ` J ) ` { ( G gsum F ) } ) ) )
84 83 eqrdv 
 |-  ( ph -> ( G tsums F ) = ( ( cls ` J ) ` { ( G gsum F ) } ) )