Metamath Proof Explorer

Theorem tsmsmhm

Description: Apply a continuous group homomorphism to an infinite group sum. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses tsmsmhm.b 
|- B = ( Base ` G )
tsmsmhm.j 
|- J = ( TopOpen ` G )
tsmsmhm.k 
|- K = ( TopOpen ` H )
tsmsmhm.1 
|- ( ph -> G e. CMnd )
tsmsmhm.2 
|- ( ph -> G e. TopSp )
tsmsmhm.3 
|- ( ph -> H e. CMnd )
tsmsmhm.4 
|- ( ph -> H e. TopSp )
tsmsmhm.5 
|- ( ph -> C e. ( G MndHom H ) )
tsmsmhm.6 
|- ( ph -> C e. ( J Cn K ) )
tsmsmhm.a 
|- ( ph -> A e. V )
tsmsmhm.f 
|- ( ph -> F : A --> B )
tsmsmhm.x 
|- ( ph -> X e. ( G tsums F ) )
Assertion tsmsmhm 
|- ( ph -> ( C ` X ) e. ( H tsums ( C o. F ) ) )

Proof

Step Hyp Ref Expression
1 tsmsmhm.b 
 |-  B = ( Base ` G )
2 tsmsmhm.j 
 |-  J = ( TopOpen ` G )
3 tsmsmhm.k 
 |-  K = ( TopOpen ` H )
4 tsmsmhm.1 
 |-  ( ph -> G e. CMnd )
5 tsmsmhm.2 
 |-  ( ph -> G e. TopSp )
6 tsmsmhm.3 
 |-  ( ph -> H e. CMnd )
7 tsmsmhm.4 
 |-  ( ph -> H e. TopSp )
8 tsmsmhm.5 
 |-  ( ph -> C e. ( G MndHom H ) )
9 tsmsmhm.6 
 |-  ( ph -> C e. ( J Cn K ) )
10 tsmsmhm.a 
 |-  ( ph -> A e. V )
11 tsmsmhm.f 
 |-  ( ph -> F : A --> B )
12 tsmsmhm.x 
 |-  ( ph -> X e. ( G tsums F ) )
13 1 2 istps 
 |-  ( G e. TopSp <-> J e. ( TopOn ` B ) )
14 5 13 sylib 
 |-  ( ph -> J e. ( TopOn ` B ) )
15 eqid 
 |-  ( ~P A i^i Fin ) = ( ~P A i^i Fin )
16 eqid 
 |-  ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) = ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } )
17 eqid 
 |-  ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) = ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } )
18 15 16 17 10 tsmsfbas 
 |-  ( ph -> ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) e. ( fBas ` ( ~P A i^i Fin ) ) )
19 fgcl 
 |-  ( ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) e. ( fBas ` ( ~P A i^i Fin ) ) -> ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) )
20 18 19 syl 
 |-  ( ph -> ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) )
21 1 15 4 10 11 tsmslem1 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( G gsum ( F |` z ) ) e. B )
22 21 fmpttd 
 |-  ( ph -> ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) : ( ~P A i^i Fin ) --> B )
23 1 2 15 17 5 10 11 tsmsval 
 |-  ( ph -> ( G tsums F ) = ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) )
24 12 23 eleqtrd 
 |-  ( ph -> X e. ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) )
25 1 4 5 10 11 tsmscl 
 |-  ( ph -> ( G tsums F ) C_ B )
26 25 12 sseldd 
 |-  ( ph -> X e. B )
27 toponuni 
 |-  ( J e. ( TopOn ` B ) -> B = U. J )
28 14 27 syl 
 |-  ( ph -> B = U. J )
29 26 28 eleqtrd 
 |-  ( ph -> X e. U. J )
30 eqid 
 |-  U. J = U. J
31 30 cncnpi 
 |-  ( ( C e. ( J Cn K ) /\ X e. U. J ) -> C e. ( ( J CnP K ) ` X ) )
32 9 29 31 syl2anc 
 |-  ( ph -> C e. ( ( J CnP K ) ` X ) )
33 flfcnp 
 |-  ( ( ( J e. ( TopOn ` B ) /\ ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) e. ( Fil ` ( ~P A i^i Fin ) ) /\ ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) : ( ~P A i^i Fin ) --> B ) /\ ( X e. ( ( J fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) /\ C e. ( ( J CnP K ) ` X ) ) ) -> ( C ` X ) e. ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) )
34 14 20 22 24 32 33 syl32anc 
 |-  ( ph -> ( C ` X ) e. ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) )
35 eqid 
 |-  ( Base ` H ) = ( Base ` H )
36 35 3 istps 
 |-  ( H e. TopSp <-> K e. ( TopOn ` ( Base ` H ) ) )
37 7 36 sylib 
 |-  ( ph -> K e. ( TopOn ` ( Base ` H ) ) )
38 cnf2 
 |-  ( ( J e. ( TopOn ` B ) /\ K e. ( TopOn ` ( Base ` H ) ) /\ C e. ( J Cn K ) ) -> C : B --> ( Base ` H ) )
39 14 37 9 38 syl3anc 
 |-  ( ph -> C : B --> ( Base ` H ) )
40 fco 
 |-  ( ( C : B --> ( Base ` H ) /\ F : A --> B ) -> ( C o. F ) : A --> ( Base ` H ) )
41 39 11 40 syl2anc 
 |-  ( ph -> ( C o. F ) : A --> ( Base ` H ) )
42 35 3 15 17 6 10 41 tsmsval 
 |-  ( ph -> ( H tsums ( C o. F ) ) = ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( H gsum ( ( C o. F ) |` z ) ) ) ) )
43 39 21 cofmpt 
 |-  ( ph -> ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) = ( z e. ( ~P A i^i Fin ) |-> ( C ` ( G gsum ( F |` z ) ) ) ) )
44 resco 
 |-  ( ( C o. F ) |` z ) = ( C o. ( F |` z ) )
45 44 oveq2i 
 |-  ( H gsum ( ( C o. F ) |` z ) ) = ( H gsum ( C o. ( F |` z ) ) )
46 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
47 4 adantr 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> G e. CMnd )
48 6 adantr 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> H e. CMnd )
49 cmnmnd 
 |-  ( H e. CMnd -> H e. Mnd )
50 48 49 syl 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> H e. Mnd )
51 elinel2 
 |-  ( z e. ( ~P A i^i Fin ) -> z e. Fin )
52 51 adantl 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> z e. Fin )
53 8 adantr 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> C e. ( G MndHom H ) )
54 elfpw 
 |-  ( z e. ( ~P A i^i Fin ) <-> ( z C_ A /\ z e. Fin ) )
55 54 simplbi 
 |-  ( z e. ( ~P A i^i Fin ) -> z C_ A )
56 fssres 
 |-  ( ( F : A --> B /\ z C_ A ) -> ( F |` z ) : z --> B )
57 11 55 56 syl2an 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) : z --> B )
58 fvexd 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( 0g ` G ) e. _V )
59 57 52 58 fdmfifsupp 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( F |` z ) finSupp ( 0g ` G ) )
60 1 46 47 50 52 53 57 59 gsummhm 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( H gsum ( C o. ( F |` z ) ) ) = ( C ` ( G gsum ( F |` z ) ) ) )
61 45 60 syl5eq 
 |-  ( ( ph /\ z e. ( ~P A i^i Fin ) ) -> ( H gsum ( ( C o. F ) |` z ) ) = ( C ` ( G gsum ( F |` z ) ) ) )
62 61 mpteq2dva 
 |-  ( ph -> ( z e. ( ~P A i^i Fin ) |-> ( H gsum ( ( C o. F ) |` z ) ) ) = ( z e. ( ~P A i^i Fin ) |-> ( C ` ( G gsum ( F |` z ) ) ) ) )
63 43 62 eqtr4d 
 |-  ( ph -> ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) = ( z e. ( ~P A i^i Fin ) |-> ( H gsum ( ( C o. F ) |` z ) ) ) )
64 63 fveq2d 
 |-  ( ph -> ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) = ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( z e. ( ~P A i^i Fin ) |-> ( H gsum ( ( C o. F ) |` z ) ) ) ) )
65 42 64 eqtr4d 
 |-  ( ph -> ( H tsums ( C o. F ) ) = ( ( K fLimf ( ( ~P A i^i Fin ) filGen ran ( y e. ( ~P A i^i Fin ) |-> { z e. ( ~P A i^i Fin ) | y C_ z } ) ) ) ` ( C o. ( z e. ( ~P A i^i Fin ) |-> ( G gsum ( F |` z ) ) ) ) ) )
66 34 65 eleqtrrd 
 |-  ( ph -> ( C ` X ) e. ( H tsums ( C o. F ) ) )