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 ) } ) )