Metamath Proof Explorer

Theorem tsmssubm

Description: Evaluate an infinite group sum in a submonoid. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses tsmssubm.a 
|- ( ph -> A e. V )
tsmssubm.1 
|- ( ph -> G e. CMnd )
tsmssubm.2 
|- ( ph -> G e. TopSp )
tsmssubm.s 
|- ( ph -> S e. ( SubMnd ` G ) )
tsmssubm.f 
|- ( ph -> F : A --> S )
tsmssubm.h 
|- H = ( G |`s S )
Assertion tsmssubm 
|- ( ph -> ( H tsums F ) = ( ( G tsums F ) i^i S ) )

Proof

Step Hyp Ref Expression
1 tsmssubm.a 
 |-  ( ph -> A e. V )
2 tsmssubm.1 
 |-  ( ph -> G e. CMnd )
3 tsmssubm.2 
 |-  ( ph -> G e. TopSp )
4 tsmssubm.s 
 |-  ( ph -> S e. ( SubMnd ` G ) )
5 tsmssubm.f 
 |-  ( ph -> F : A --> S )
6 tsmssubm.h 
 |-  H = ( G |`s S )
7 6 submbas 
 |-  ( S e. ( SubMnd ` G ) -> S = ( Base ` H ) )
8 4 7 syl 
 |-  ( ph -> S = ( Base ` H ) )
9 8 eleq2d 
 |-  ( ph -> ( x e. S <-> x e. ( Base ` H ) ) )
10 9 anbi1d 
 |-  ( ph -> ( ( x e. S /\ A. v e. ( TopOpen ` H ) ( x e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) ) ) <-> ( x e. ( Base ` H ) /\ A. v e. ( TopOpen ` H ) ( x e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) ) ) ) )
11 elin 
 |-  ( x e. ( ( G tsums F ) i^i S ) <-> ( x e. ( G tsums F ) /\ x e. S ) )
12 11 biancomi 
 |-  ( x e. ( ( G tsums F ) i^i S ) <-> ( x e. S /\ x e. ( G tsums F ) ) )
13 eqid 
 |-  ( Base ` G ) = ( Base ` G )
14 13 submss 
 |-  ( S e. ( SubMnd ` G ) -> S C_ ( Base ` G ) )
15 4 14 syl 
 |-  ( ph -> S C_ ( Base ` G ) )
16 15 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. ( Base ` G ) )
17 eqid 
 |-  ( TopOpen ` G ) = ( TopOpen ` G )
18 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
19 5 15 fssd 
 |-  ( ph -> F : A --> ( Base ` G ) )
20 13 17 18 2 3 1 19 eltsms 
 |-  ( ph -> ( x e. ( G tsums F ) <-> ( x e. ( Base ` G ) /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) ) )
21 20 baibd 
 |-  ( ( ph /\ x e. ( Base ` G ) ) -> ( x e. ( G tsums F ) <-> A. u e. ( TopOpen ` G ) ( x e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
22 16 21 syldan 
 |-  ( ( ph /\ x e. S ) -> ( x e. ( G tsums F ) <-> A. u e. ( TopOpen ` G ) ( x e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
23 vex 
 |-  u e. _V
24 23 inex1 
 |-  ( u i^i S ) e. _V
25 24 a1i 
 |-  ( ( ( ph /\ x e. S ) /\ u e. ( TopOpen ` G ) ) -> ( u i^i S ) e. _V )
26 6 17 resstopn 
 |-  ( ( TopOpen ` G ) |`t S ) = ( TopOpen ` H )
27 26 eleq2i 
 |-  ( v e. ( ( TopOpen ` G ) |`t S ) <-> v e. ( TopOpen ` H ) )
28 fvex 
 |-  ( TopOpen ` G ) e. _V
29 elrest 
 |-  ( ( ( TopOpen ` G ) e. _V /\ S e. ( SubMnd ` G ) ) -> ( v e. ( ( TopOpen ` G ) |`t S ) <-> E. u e. ( TopOpen ` G ) v = ( u i^i S ) ) )
30 28 4 29 sylancr 
 |-  ( ph -> ( v e. ( ( TopOpen ` G ) |`t S ) <-> E. u e. ( TopOpen ` G ) v = ( u i^i S ) ) )
31 30 adantr 
 |-  ( ( ph /\ x e. S ) -> ( v e. ( ( TopOpen ` G ) |`t S ) <-> E. u e. ( TopOpen ` G ) v = ( u i^i S ) ) )
32 27 31 bitr3id 
 |-  ( ( ph /\ x e. S ) -> ( v e. ( TopOpen ` H ) <-> E. u e. ( TopOpen ` G ) v = ( u i^i S ) ) )
33 eleq2 
 |-  ( v = ( u i^i S ) -> ( x e. v <-> x e. ( u i^i S ) ) )
34 elin 
 |-  ( x e. ( u i^i S ) <-> ( x e. u /\ x e. S ) )
35 34 rbaib 
 |-  ( x e. S -> ( x e. ( u i^i S ) <-> x e. u ) )
36 35 adantl 
 |-  ( ( ph /\ x e. S ) -> ( x e. ( u i^i S ) <-> x e. u ) )
37 33 36 sylan9bbr 
 |-  ( ( ( ph /\ x e. S ) /\ v = ( u i^i S ) ) -> ( x e. v <-> x e. u ) )
38 eleq2 
 |-  ( v = ( u i^i S ) -> ( ( H gsum ( F |` y ) ) e. v <-> ( H gsum ( F |` y ) ) e. ( u i^i S ) ) )
39 eqid 
 |-  ( Base ` H ) = ( Base ` H )
40 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
41 6 submmnd 
 |-  ( S e. ( SubMnd ` G ) -> H e. Mnd )
42 4 41 syl 
 |-  ( ph -> H e. Mnd )
43 6 subcmn 
 |-  ( ( G e. CMnd /\ H e. Mnd ) -> H e. CMnd )
44 2 42 43 syl2anc 
 |-  ( ph -> H e. CMnd )
45 44 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> H e. CMnd )
46 elinel2 
 |-  ( y e. ( ~P A i^i Fin ) -> y e. Fin )
47 46 adantl 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> y e. Fin )
48 5 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> F : A --> S )
49 elfpw 
 |-  ( y e. ( ~P A i^i Fin ) <-> ( y C_ A /\ y e. Fin ) )
50 49 simplbi 
 |-  ( y e. ( ~P A i^i Fin ) -> y C_ A )
51 50 adantl 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> y C_ A )
52 48 51 fssresd 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( F |` y ) : y --> S )
53 8 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> S = ( Base ` H ) )
54 53 feq3d 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( F |` y ) : y --> S <-> ( F |` y ) : y --> ( Base ` H ) ) )
55 52 54 mpbid 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( F |` y ) : y --> ( Base ` H ) )
56 fvex 
 |-  ( 0g ` H ) e. _V
57 56 a1i 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( 0g ` H ) e. _V )
58 52 47 57 fdmfifsupp 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( F |` y ) finSupp ( 0g ` H ) )
59 39 40 45 47 55 58 gsumcl 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( H gsum ( F |` y ) ) e. ( Base ` H ) )
60 59 53 eleqtrrd 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( H gsum ( F |` y ) ) e. S )
61 elin 
 |-  ( ( H gsum ( F |` y ) ) e. ( u i^i S ) <-> ( ( H gsum ( F |` y ) ) e. u /\ ( H gsum ( F |` y ) ) e. S ) )
62 61 rbaib 
 |-  ( ( H gsum ( F |` y ) ) e. S -> ( ( H gsum ( F |` y ) ) e. ( u i^i S ) <-> ( H gsum ( F |` y ) ) e. u ) )
63 60 62 syl 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( H gsum ( F |` y ) ) e. ( u i^i S ) <-> ( H gsum ( F |` y ) ) e. u ) )
64 4 ad2antrr 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> S e. ( SubMnd ` G ) )
65 47 64 52 6 gsumsubm 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` y ) ) = ( H gsum ( F |` y ) ) )
66 65 eleq1d 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( G gsum ( F |` y ) ) e. u <-> ( H gsum ( F |` y ) ) e. u ) )
67 63 66 bitr4d 
 |-  ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( H gsum ( F |` y ) ) e. ( u i^i S ) <-> ( G gsum ( F |` y ) ) e. u ) )
68 38 67 sylan9bbr 
 |-  ( ( ( ( ph /\ x e. S ) /\ y e. ( ~P A i^i Fin ) ) /\ v = ( u i^i S ) ) -> ( ( H gsum ( F |` y ) ) e. v <-> ( G gsum ( F |` y ) ) e. u ) )
69 68 an32s 
 |-  ( ( ( ( ph /\ x e. S ) /\ v = ( u i^i S ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( H gsum ( F |` y ) ) e. v <-> ( G gsum ( F |` y ) ) e. u ) )
70 69 imbi2d 
 |-  ( ( ( ( ph /\ x e. S ) /\ v = ( u i^i S ) ) /\ y e. ( ~P A i^i Fin ) ) -> ( ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) <-> ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) )
71 70 ralbidva 
 |-  ( ( ( ph /\ x e. S ) /\ v = ( u i^i S ) ) -> ( A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) <-> A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) )
72 71 rexbidv 
 |-  ( ( ( ph /\ x e. S ) /\ v = ( u i^i S ) ) -> ( E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) <-> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) )
73 37 72 imbi12d 
 |-  ( ( ( ph /\ x e. S ) /\ v = ( u i^i S ) ) -> ( ( x e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) ) <-> ( x e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
74 25 32 73 ralxfr2d 
 |-  ( ( ph /\ x e. S ) -> ( A. v e. ( TopOpen ` H ) ( x e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) ) <-> A. u e. ( TopOpen ` G ) ( x e. u -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( G gsum ( F |` y ) ) e. u ) ) ) )
75 22 74 bitr4d 
 |-  ( ( ph /\ x e. S ) -> ( x e. ( G tsums F ) <-> A. v e. ( TopOpen ` H ) ( x e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) ) ) )
76 75 pm5.32da 
 |-  ( ph -> ( ( x e. S /\ x e. ( G tsums F ) ) <-> ( x e. S /\ A. v e. ( TopOpen ` H ) ( x e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) ) ) ) )
77 12 76 syl5bb 
 |-  ( ph -> ( x e. ( ( G tsums F ) i^i S ) <-> ( x e. S /\ A. v e. ( TopOpen ` H ) ( x e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) ) ) ) )
78 eqid 
 |-  ( TopOpen ` H ) = ( TopOpen ` H )
79 resstps 
 |-  ( ( G e. TopSp /\ S e. ( SubMnd ` G ) ) -> ( G |`s S ) e. TopSp )
80 3 4 79 syl2anc 
 |-  ( ph -> ( G |`s S ) e. TopSp )
81 6 80 eqeltrid 
 |-  ( ph -> H e. TopSp )
82 8 feq3d 
 |-  ( ph -> ( F : A --> S <-> F : A --> ( Base ` H ) ) )
83 5 82 mpbid 
 |-  ( ph -> F : A --> ( Base ` H ) )
84 39 78 18 44 81 1 83 eltsms 
 |-  ( ph -> ( x e. ( H tsums F ) <-> ( x e. ( Base ` H ) /\ A. v e. ( TopOpen ` H ) ( x e. v -> E. z e. ( ~P A i^i Fin ) A. y e. ( ~P A i^i Fin ) ( z C_ y -> ( H gsum ( F |` y ) ) e. v ) ) ) ) )
85 10 77 84 3bitr4rd 
 |-  ( ph -> ( x e. ( H tsums F ) <-> x e. ( ( G tsums F ) i^i S ) ) )
86 85 eqrdv 
 |-  ( ph -> ( H tsums F ) = ( ( G tsums F ) i^i S ) )