MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tsmsxp Structured version   Visualization version   Unicode version
Theorem tsmsxp 21958
Description: Write a sum over a two-dimensional region as a double sum. This infinite group sum version of gsumxp 18375 is also known as Fubini's theorem. The converse is not necessarily true without additional assumptions. See tsmsxplem1 21956 for the main proof; this part mostly sets up the local assumptions. (Contributed by Mario Carneiro, 21-Sep-2015.)
Hypotheses
Ref Expression
tsmsxp.b |- B = ( Base ` G )
tsmsxp.g |- ( ph -> G e. CMnd )
tsmsxp.2 |- ( ph -> G e. TopGrp )
tsmsxp.a |- ( ph -> A e. V )
tsmsxp.c |- ( ph -> C e. W )
tsmsxp.f |- ( ph -> F : ( A X. C ) --> B )
tsmsxp.h |- ( ph -> H : A --> B )
tsmsxp.1 |- ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
Assertion
Ref Expression
tsmsxp |- ( ph -> ( G tsums F ) C_ ( G tsums H ) )
Distinct variable groups:   j, k, G   B, k   A, j, k   j, H, k   C, j, k   j, F, k   ph, j, k
Allowed substitution hints:   B( j)   V( j, k)   W( j, k)
Proof of Theorem tsmsxp
Dummy variables g y z a b c d h n s t u v x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tsmsxp.2 . . . . . . . . . . 11 |- ( ph -> G e. TopGrp )
2 tgptmd 21883 . . . . . . . . . . 11 |- ( G e. TopGrp -> G e. TopMnd )
31, 2syl 17 . . . . . . . . . 10 |- ( ph -> G e. TopMnd )
433ad2ant1 1082 . . . . . . . . 9 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> G e. TopMnd )
5 simp2 1062 . . . . . . . . 9 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> u e. ( TopOpen ` G ) )
6 eqid 2622 . . . . . . . . . . . . 13 |- ( TopOpen ` G ) = ( TopOpen ` G )
7 tsmsxp.b . . . . . . . . . . . . 13 |- B = ( Base ` G )
86, 7tmdtopon 21885 . . . . . . . . . . . 12 |- ( G e. TopMnd -> ( TopOpen ` G ) e. (TopOn ` B ) )
94, 8syl 17 . . . . . . . . . . 11 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( TopOpen ` G ) e. (TopOn ` B ) )
10 toponss 20731 . . . . . . . . . . 11 |- ( ( ( TopOpen ` G ) e. (TopOn ` B ) /\ u e. ( TopOpen ` G ) ) -> u C_ B )
119, 5, 10syl2anc 693 . . . . . . . . . 10 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> u C_ B )
12 simp3 1063 . . . . . . . . . 10 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> x e. u )
1311, 12sseldd 3604 . . . . . . . . 9 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> x e. B )
14 tmdmnd 21879 . . . . . . . . . . 11 |- ( G e. TopMnd -> G e. Mnd )
154, 14syl 17 . . . . . . . . . 10 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> G e. Mnd )
16 eqid 2622 . . . . . . . . . . 11 |- ( 0g ` G ) = ( 0g ` G )
177, 16mndidcl 17308 . . . . . . . . . 10 |- ( G e. Mnd -> ( 0g ` G ) e. B )
1815, 17syl 17 . . . . . . . . 9 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( 0g ` G ) e. B )
19 eqid 2622 . . . . . . . . . . . 12 |- ( +g ` G ) = ( +g ` G )
207, 19, 16mndrid 17312 . . . . . . . . . . 11 |- ( ( G e. Mnd /\ x e. B ) -> ( x ( +g ` G ) ( 0g ` G ) ) = x )
2115, 13, 20syl2anc 693 . . . . . . . . . 10 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( x ( +g ` G ) ( 0g ` G ) ) = x )
2221, 12eqeltrd 2701 . . . . . . . . 9 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( x ( +g ` G ) ( 0g ` G ) ) e. u )
237, 6, 19tmdcn2 21893 . . . . . . . . 9 |- ( ( ( G e. TopMnd /\ u e. ( TopOpen ` G ) ) /\ ( x e. B /\ ( 0g ` G ) e. B /\ ( x ( +g ` G ) ( 0g ` G ) ) e. u ) ) -> E. v e. ( TopOpen ` G ) E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) )
244, 5, 13, 18, 22, 23syl23anc 1333 . . . . . . . 8 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> E. v e. ( TopOpen ` G ) E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) )
25 r19.29 3072 . . . . . . . . 9 |- ( ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ E. v e. ( TopOpen ` G ) E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> E. v e. ( TopOpen ` G ) ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) )
26 simp31 1097 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> x e. v )
27 elfpw 8268 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ~P ( A X. C ) i^i Fin ) <-> ( y C_ ( A X. C ) /\ y e. Fin ) )
2827simplbi 476 . . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ~P ( A X. C ) i^i Fin ) -> y C_ ( A X. C ) )
2928ad2antrl 764 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> y C_ ( A X. C ) )
30 dmss 5323 . . . . . . . . . . . . . . . . . . . . 21 |- ( y C_ ( A X. C ) -> dom y C_ dom ( A X. C ) )
3129, 30syl 17 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> dom y C_ dom ( A X. C ) )
32 dmxpss 5565 . . . . . . . . . . . . . . . . . . . 20 |- dom ( A X. C ) C_ A
3331, 32syl6ss 3615 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> dom y C_ A )
3427simprbi 480 . . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ~P ( A X. C ) i^i Fin ) -> y e. Fin )
3534ad2antrl 764 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> y e. Fin )
36 dmfi 8244 . . . . . . . . . . . . . . . . . . . 20 |- ( y e. Fin -> dom y e. Fin )
3735, 36syl 17 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> dom y e. Fin )
38 elfpw 8268 . . . . . . . . . . . . . . . . . . 19 |- ( dom y e. ( ~P A i^i Fin ) <-> ( dom y C_ A /\ dom y e. Fin ) )
3933, 37, 38sylanbrc 698 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> dom y e. ( ~P A i^i Fin ) )
40 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . 23 |- (.g ` G ) = (.g ` G )
41 simpl11 1136 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ph )
42 tsmsxp.g . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> G e. CMnd )
4341, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> G e. CMnd )
4441, 3syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> G e. TopMnd )
45 simprrl 804 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> b e. ( ~P A i^i Fin ) )
46 elfpw 8268 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( b e. ( ~P A i^i Fin ) <-> ( b C_ A /\ b e. Fin ) )
4746simprbi 480 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( b e. ( ~P A i^i Fin ) -> b e. Fin )
4845, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> b e. Fin )
49 simpl2r 1115 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> t e. ( TopOpen ` G ) )
5044, 14syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> G e. Mnd )
5150, 17syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( 0g ` G ) e. B )
52 hashcl 13147 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( b e. Fin -> ( # ` b ) e. NN0 )
5348, 52syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( # ` b ) e. NN0 )
547, 40, 16mulgnn0z 17567 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( G e. Mnd /\ ( # ` b ) e. NN0 ) -> ( ( # ` b ) (.g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
5550, 53, 54syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( ( # ` b ) (.g ` G ) ( 0g ` G ) ) = ( 0g ` G ) )
56 simpl32 1143 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( 0g ` G ) e. t )
5755, 56eqeltrd 2701 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( ( # ` b ) (.g ` G ) ( 0g ` G ) ) e. t )
586, 7, 40, 43, 44, 48, 49, 51, 57tmdgsum2 21900 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> E. s e. ( TopOpen ` G ) ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) )
59 simp111 1190 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> ph )
6059, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> G e. CMnd )
6159, 1syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> G e. TopGrp )
62 tsmsxp.a . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> A e. V )
6359, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> A e. V )
64 tsmsxp.c . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> C e. W )
6559, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> C e. W )
66 tsmsxp.f . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> F : ( A X. C ) --> B )
6759, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> F : ( A X. C ) --> B )
68 tsmsxp.h . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> H : A --> B )
6959, 68syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> H : A --> B )
70 tsmsxp.1 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
7159, 70sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
72 eqid 2622 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -g ` G ) = ( -g ` G )
73 simp3l 1089 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> s e. ( TopOpen ` G ) )
74 simp3rl 1134 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> ( 0g ` G ) e. s )
75 simp2rl 1130 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> b e. ( ~P A i^i Fin ) )
76 simp2rr 1131 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> dom y C_ b )
77 simp2ll 1128 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> y e. ( ~P ( A X. C ) i^i Fin ) )
787, 60, 61, 63, 65, 67, 69, 71, 6, 16, 19, 72, 73, 74, 75, 76, 77tsmsxplem1 21956 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> E. n e. ( ~P C i^i Fin ) ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) )
79433adant3 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> G e. CMnd )
80613adant3r 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> G e. TopGrp )
81633adant3r 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A e. V )
82653adant3r 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> C e. W )
83673adant3r 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> F : ( A X. C ) --> B )
84693adant3r 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> H : A --> B )
85413adant3 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ph )
8685, 70sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) /\ j e. A ) -> ( H ` j ) e. ( G tsums ( k e. C |-> ( j F k ) ) ) )
87 simp3ll 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> s e. ( TopOpen ` G ) )
88743adant3r 1323 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( 0g ` G ) e. s )
89 simp2rl 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> b e. ( ~P A i^i Fin ) )
90 simp133 1198 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u )
91 simp3rl 1134 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> n e. ( ~P C i^i Fin ) )
92 simp2ll 1128 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> y e. ( ~P ( A X. C ) i^i Fin ) )
93 simp2rr 1131 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> dom y C_ b )
94 simp3rr 1135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) )
9594simpld 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ran y C_ n )
96 relxp 5227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- Rel ( A X. C )
97 relss 5206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( y C_ ( A X. C ) -> ( Rel ( A X. C ) -> Rel y ) )
9828, 96, 97mpisyl 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( y e. ( ~P ( A X. C ) i^i Fin ) -> Rel y )
99 relssdmrn 5656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( Rel y -> y C_ ( dom y X. ran y ) )
10098, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( y e. ( ~P ( A X. C ) i^i Fin ) -> y C_ ( dom y X. ran y ) )
101 xpss12 5225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( dom y C_ b /\ ran y C_ n ) -> ( dom y X. ran y ) C_ ( b X. n ) )
102100, 101sylan9ss 3616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ ( dom y C_ b /\ ran y C_ n ) ) -> y C_ ( b X. n ) )
10392, 93, 95, 102syl12anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> y C_ ( b X. n ) )
10494simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s )
105 elfpw 8268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( n e. ( ~P C i^i Fin ) <-> ( n C_ C /\ n e. Fin ) )
106 xpss12 5225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( b C_ A /\ n C_ C ) -> ( b X. n ) C_ ( A X. C ) )
107 xpfi 8231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( b e. Fin /\ n e. Fin ) -> ( b X. n ) e. Fin )
108106, 107anim12i 590 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( b C_ A /\ n C_ C ) /\ ( b e. Fin /\ n e. Fin ) ) -> ( ( b X. n ) C_ ( A X. C ) /\ ( b X. n ) e. Fin ) )
109108an4s 869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( b C_ A /\ b e. Fin ) /\ ( n C_ C /\ n e. Fin ) ) -> ( ( b X. n ) C_ ( A X. C ) /\ ( b X. n ) e. Fin ) )
11046, 105, 109syl2anb 496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( b e. ( ~P A i^i Fin ) /\ n e. ( ~P C i^i Fin ) ) -> ( ( b X. n ) C_ ( A X. C ) /\ ( b X. n ) e. Fin ) )
111 elfpw 8268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( b X. n ) e. ( ~P ( A X. C ) i^i Fin ) <-> ( ( b X. n ) C_ ( A X. C ) /\ ( b X. n ) e. Fin ) )
112110, 111sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( b e. ( ~P A i^i Fin ) /\ n e. ( ~P C i^i Fin ) ) -> ( b X. n ) e. ( ~P ( A X. C ) i^i Fin ) )
11389, 91, 112syl2anc 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( b X. n ) e. ( ~P ( A X. C ) i^i Fin ) )
114 simp2lr 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) )
115 sseq2 3627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z = ( b X. n ) -> ( y C_ z <-> y C_ ( b X. n ) ) )
116 reseq2 5391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( z = ( b X. n ) -> ( F |` z ) = ( F |` ( b X. n ) ) )
117116oveq2d 6666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( z = ( b X. n ) -> ( G gsumg ( F |` z ) ) = ( G gsumg ( F |` ( b X. n ) ) ) )
118117eleq1d 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( z = ( b X. n ) -> ( ( G gsumg ( F |` z ) ) e. v <-> ( G gsumg ( F |` ( b X. n ) ) ) e. v ) )
119115, 118imbi12d 334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( z = ( b X. n ) -> ( ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) <-> ( y C_ ( b X. n ) -> ( G gsumg ( F |` ( b X. n ) ) ) e. v ) ) )
120119rspcv 3305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( b X. n ) e. ( ~P ( A X. C ) i^i Fin ) -> ( A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) -> ( y C_ ( b X. n ) -> ( G gsumg ( F |` ( b X. n ) ) ) e. v ) ) )
121113, 114, 103, 120syl3c 66 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( G gsumg ( F |` ( b X. n ) ) ) e. v )
122 simp3lr 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) )
123122simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. g e. ( s ^m b ) ( G gsumg g ) e. t )
124 oveq2 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( g = h -> ( G gsumg g ) = ( G gsumg h ) )
125124eleq1d 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( g = h -> ( ( G gsumg g ) e. t <-> ( G gsumg h ) e. t ) )
126125cbvralv 3171 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( A. g e. ( s ^m b ) ( G gsumg g ) e. t <-> A. h e. ( s ^m b ) ( G gsumg h ) e. t )
127123, 126sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> A. h e. ( s ^m b ) ( G gsumg h ) e. t )
1287, 79, 80, 81, 82, 83, 84, 86, 6, 16, 19, 72, 87, 88, 89, 90, 91, 103, 104, 121, 127tsmsxplem2 21957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) ) -> ( G gsumg ( H |` b ) ) e. u )
1291283exp 1264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> ( ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) -> ( ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) -> ( G gsumg ( H |` b ) ) e. u ) ) )
130129exp4a 633 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> ( ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) -> ( ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) -> ( ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) -> ( G gsumg ( H |` b ) ) e. u ) ) ) )
1311303imp1 1280 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) /\ ( n e. ( ~P C i^i Fin ) /\ ( ran y C_ n /\ A. x e. b ( ( H ` x ) ( -g ` G ) ( G gsumg ( F |` ( { x } X. n ) ) ) ) e. s ) ) ) -> ( G gsumg ( H |` b ) ) e. u )
13278, 131rexlimddv 3035 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> ( G gsumg ( H |` b ) ) e. u )
1331323expa 1265 . . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) /\ ( s e. ( TopOpen ` G ) /\ ( ( 0g ` G ) e. s /\ A. g e. ( s ^m b ) ( G gsumg g ) e. t ) ) ) -> ( G gsumg ( H |` b ) ) e. u )
13458, 133rexlimddv 3035 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) ) -> ( G gsumg ( H |` b ) ) e. u )
135134anassrs 680 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) /\ ( b e. ( ~P A i^i Fin ) /\ dom y C_ b ) ) -> ( G gsumg ( H |` b ) ) e. u )
136135expr 643 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) /\ b e. ( ~P A i^i Fin ) ) -> ( dom y C_ b -> ( G gsumg ( H |` b ) ) e. u ) )
137136ralrimiva 2966 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> A. b e. ( ~P A i^i Fin ) ( dom y C_ b -> ( G gsumg ( H |` b ) ) e. u ) )
138 sseq1 3626 . . . . . . . . . . . . . . . . . . . . 21 |- ( a = dom y -> ( a C_ b <-> dom y C_ b ) )
139138imbi1d 331 . . . . . . . . . . . . . . . . . . . 20 |- ( a = dom y -> ( ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) <-> ( dom y C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) )
140139ralbidv 2986 . . . . . . . . . . . . . . . . . . 19 |- ( a = dom y -> ( A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) <-> A. b e. ( ~P A i^i Fin ) ( dom y C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) )
141140rspcev 3309 . . . . . . . . . . . . . . . . . 18 |- ( ( dom y e. ( ~P A i^i Fin ) /\ A. b e. ( ~P A i^i Fin ) ( dom y C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) )
14239, 137, 141syl2anc 693 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) /\ ( y e. ( ~P ( A X. C ) i^i Fin ) /\ A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) )
143142rexlimdvaa 3032 . . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> ( E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) )
14426, 143embantd 59 . . . . . . . . . . . . . . 15 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) /\ ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) )
1451443expia 1267 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ ( v e. ( TopOpen ` G ) /\ t e. ( TopOpen ` G ) ) ) -> ( ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) )
146145anassrs 680 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ v e. ( TopOpen ` G ) ) /\ t e. ( TopOpen ` G ) ) -> ( ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) )
147146rexlimdva 3031 . . . . . . . . . . . 12 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ v e. ( TopOpen ` G ) ) -> ( E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) )
148147com23 86 . . . . . . . . . . 11 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ v e. ( TopOpen ` G ) ) -> ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> ( E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) )
149148impd 447 . . . . . . . . . 10 |- ( ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) /\ v e. ( TopOpen ` G ) ) -> ( ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) )
150149rexlimdva 3031 . . . . . . . . 9 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( E. v e. ( TopOpen ` G ) ( ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) )
15125, 150syl5 34 . . . . . . . 8 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) /\ E. v e. ( TopOpen ` G ) E. t e. ( TopOpen ` G ) ( x e. v /\ ( 0g ` G ) e. t /\ A. c e. v A. d e. t ( c ( +g ` G ) d ) e. u ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) )
15224, 151mpan2d 710 . . . . . . 7 |- ( ( ph /\ u e. ( TopOpen ` G ) /\ x e. u ) -> ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) )
1531523expia 1267 . . . . . 6 |- ( ( ph /\ u e. ( TopOpen ` G ) ) -> ( x e. u -> ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) )
154153com23 86 . . . . 5 |- ( ( ph /\ u e. ( TopOpen ` G ) ) -> ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> ( x e. u -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) )
155154ralrimdva 2969 . . . 4 |- ( ph -> ( A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) -> A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) )
156155anim2d 589 . . 3 |- ( ph -> ( ( x e. B /\ A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) -> ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) ) )
157 eqid 2622 . . . 4 |- ( ~P ( A X. C ) i^i Fin ) = ( ~P ( A X. C ) i^i Fin )
158 tgptps 21884 . . . . 5 |- ( G e. TopGrp -> G e. TopSp )
1591, 158syl 17 . . . 4 |- ( ph -> G e. TopSp )
160 xpexg 6960 . . . . 5 |- ( ( A e. V /\ C e. W ) -> ( A X. C ) e. _V )
16162, 64, 160syl2anc 693 . . . 4 |- ( ph -> ( A X. C ) e. _V )
1627, 6, 157, 42, 159, 161, 66eltsms 21936 . . 3 |- ( ph -> ( x e. ( G tsums F ) <-> ( x e. B /\ A. v e. ( TopOpen ` G ) ( x e. v -> E. y e. ( ~P ( A X. C ) i^i Fin ) A. z e. ( ~P ( A X. C ) i^i Fin ) ( y C_ z -> ( G gsumg ( F |` z ) ) e. v ) ) ) ) )
163 eqid 2622 . . . 4 |- ( ~P A i^i Fin ) = ( ~P A i^i Fin )
1647, 6, 163, 42, 159, 62, 68eltsms 21936 . . 3 |- ( ph -> ( x e. ( G tsums H ) <-> ( x e. B /\ A. u e. ( TopOpen ` G ) ( x e. u -> E. a e. ( ~P A i^i Fin ) A. b e. ( ~P A i^i Fin ) ( a C_ b -> ( G gsumg ( H |` b ) ) e. u ) ) ) ) )
165156, 162, 1643imtr4d 283 . 2 |- ( ph -> ( x e. ( G tsums F ) -> x e. ( G tsums H ) ) )
166165ssrdv 3609 1 |- ( ph -> ( G tsums F ) C_ ( G tsums H ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   _Vcvv 3200   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   {csn 4177   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   ran crn 5115   |` cres 5116   Rel wrel 5119   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Fincfn 7955   NN0cn0 11292   #chash 13117   Basecbs 15857   +g cplusg 15941   TopOpenctopn 16082   0gc0g 16100   gsumg cgsu 16101   Mndcmnd 17294   -gcsg 17424  .gcmg 17540  CMndccmn 18193  TopOnctopon 20715   TopSpctps 20736  TopMndctmd 21874   TopGrpctgp 21875   tsums ctsu 21929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-rest 16083  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-mre 16246  df-mrc 16247  df-acs 16249  df-plusf 17241  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-ghm 17658  df-cntz 17750  df-cmn 18195  df-abl 18196  df-fbas 19743  df-fg 19744  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-ntr 20824  df-nei 20902  df-cn 21031  df-cnp 21032  df-cmp 21190  df-tx 21365  df-xko 21366  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-tmd 21876  df-tgp 21877  df-tsms 21930
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator