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 𝐵 = ( Base ‘ 𝐺 )
tsmsmhm.j 𝐽 = ( TopOpen ‘ 𝐺 )
tsmsmhm.k 𝐾 = ( TopOpen ‘ 𝐻 )
tsmsmhm.1 ( 𝜑𝐺 ∈ CMnd )
tsmsmhm.2 ( 𝜑𝐺 ∈ TopSp )
tsmsmhm.3 ( 𝜑𝐻 ∈ CMnd )
tsmsmhm.4 ( 𝜑𝐻 ∈ TopSp )
tsmsmhm.5 ( 𝜑𝐶 ∈ ( 𝐺 MndHom 𝐻 ) )
tsmsmhm.6 ( 𝜑𝐶 ∈ ( 𝐽 Cn 𝐾 ) )
tsmsmhm.a ( 𝜑𝐴𝑉 )
tsmsmhm.f ( 𝜑𝐹 : 𝐴𝐵 )
tsmsmhm.x ( 𝜑𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
Assertion tsmsmhm ( 𝜑 → ( 𝐶𝑋 ) ∈ ( 𝐻 tsums ( 𝐶𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 tsmsmhm.b 𝐵 = ( Base ‘ 𝐺 )
2 tsmsmhm.j 𝐽 = ( TopOpen ‘ 𝐺 )
3 tsmsmhm.k 𝐾 = ( TopOpen ‘ 𝐻 )
4 tsmsmhm.1 ( 𝜑𝐺 ∈ CMnd )
5 tsmsmhm.2 ( 𝜑𝐺 ∈ TopSp )
6 tsmsmhm.3 ( 𝜑𝐻 ∈ CMnd )
7 tsmsmhm.4 ( 𝜑𝐻 ∈ TopSp )
8 tsmsmhm.5 ( 𝜑𝐶 ∈ ( 𝐺 MndHom 𝐻 ) )
9 tsmsmhm.6 ( 𝜑𝐶 ∈ ( 𝐽 Cn 𝐾 ) )
10 tsmsmhm.a ( 𝜑𝐴𝑉 )
11 tsmsmhm.f ( 𝜑𝐹 : 𝐴𝐵 )
12 tsmsmhm.x ( 𝜑𝑋 ∈ ( 𝐺 tsums 𝐹 ) )
13 1 2 istps ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
14 5 13 sylib ( 𝜑𝐽 ∈ ( TopOn ‘ 𝐵 ) )
15 eqid ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin )
16 eqid ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) = ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } )
17 eqid ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) = ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } )
18 15 16 17 10 tsmsfbas ( 𝜑 → ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
19 fgcl ( ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ∈ ( fBas ‘ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
20 18 19 syl ( 𝜑 → ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) )
21 1 15 4 10 11 tsmslem1 ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹𝑧 ) ) ∈ 𝐵 )
22 21 fmpttd ( 𝜑 → ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ 𝐵 )
23 1 2 15 17 5 10 11 tsmsval ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) )
24 12 23 eleqtrd ( 𝜑𝑋 ∈ ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) )
25 1 4 5 10 11 tsmscl ( 𝜑 → ( 𝐺 tsums 𝐹 ) ⊆ 𝐵 )
26 25 12 sseldd ( 𝜑𝑋𝐵 )
27 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) → 𝐵 = 𝐽 )
28 14 27 syl ( 𝜑𝐵 = 𝐽 )
29 26 28 eleqtrd ( 𝜑𝑋 𝐽 )
30 eqid 𝐽 = 𝐽
31 30 cncnpi ( ( 𝐶 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑋 𝐽 ) → 𝐶 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑋 ) )
32 9 29 31 syl2anc ( 𝜑𝐶 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑋 ) )
33 flfcnp ( ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ∈ ( Fil ‘ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) : ( 𝒫 𝐴 ∩ Fin ) ⟶ 𝐵 ) ∧ ( 𝑋 ∈ ( ( 𝐽 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) ∧ 𝐶 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑋 ) ) ) → ( 𝐶𝑋 ) ∈ ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) ) )
34 14 20 22 24 32 33 syl32anc ( 𝜑 → ( 𝐶𝑋 ) ∈ ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) ) )
35 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
36 35 3 istps ( 𝐻 ∈ TopSp ↔ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) )
37 7 36 sylib ( 𝜑𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) )
38 cnf2 ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐾 ∈ ( TopOn ‘ ( Base ‘ 𝐻 ) ) ∧ 𝐶 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐶 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
39 14 37 9 38 syl3anc ( 𝜑𝐶 : 𝐵 ⟶ ( Base ‘ 𝐻 ) )
40 fco ( ( 𝐶 : 𝐵 ⟶ ( Base ‘ 𝐻 ) ∧ 𝐹 : 𝐴𝐵 ) → ( 𝐶𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝐻 ) )
41 39 11 40 syl2anc ( 𝜑 → ( 𝐶𝐹 ) : 𝐴 ⟶ ( Base ‘ 𝐻 ) )
42 35 3 15 17 6 10 41 tsmsval ( 𝜑 → ( 𝐻 tsums ( 𝐶𝐹 ) ) = ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐻 Σg ( ( 𝐶𝐹 ) ↾ 𝑧 ) ) ) ) )
43 39 21 cofmpt ( 𝜑 → ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐶 ‘ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) )
44 resco ( ( 𝐶𝐹 ) ↾ 𝑧 ) = ( 𝐶 ∘ ( 𝐹𝑧 ) )
45 44 oveq2i ( 𝐻 Σg ( ( 𝐶𝐹 ) ↾ 𝑧 ) ) = ( 𝐻 Σg ( 𝐶 ∘ ( 𝐹𝑧 ) ) )
46 eqid ( 0g𝐺 ) = ( 0g𝐺 )
47 4 adantr ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd )
48 6 adantr ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐻 ∈ CMnd )
49 cmnmnd ( 𝐻 ∈ CMnd → 𝐻 ∈ Mnd )
50 48 49 syl ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐻 ∈ Mnd )
51 elinel2 ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ∈ Fin )
52 51 adantl ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ∈ Fin )
53 8 adantr ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐶 ∈ ( 𝐺 MndHom 𝐻 ) )
54 elfpw ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑧𝐴𝑧 ∈ Fin ) )
55 54 simplbi ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧𝐴 )
56 fssres ( ( 𝐹 : 𝐴𝐵𝑧𝐴 ) → ( 𝐹𝑧 ) : 𝑧𝐵 )
57 11 55 56 syl2an ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑧 ) : 𝑧𝐵 )
58 fvexd ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 0g𝐺 ) ∈ V )
59 57 52 58 fdmfifsupp ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹𝑧 ) finSupp ( 0g𝐺 ) )
60 1 46 47 50 52 53 57 59 gsummhm ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻 Σg ( 𝐶 ∘ ( 𝐹𝑧 ) ) ) = ( 𝐶 ‘ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) )
61 45 60 syl5eq ( ( 𝜑𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐻 Σg ( ( 𝐶𝐹 ) ↾ 𝑧 ) ) = ( 𝐶 ‘ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) )
62 61 mpteq2dva ( 𝜑 → ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐻 Σg ( ( 𝐶𝐹 ) ↾ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐶 ‘ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) )
63 43 62 eqtr4d ( 𝜑 → ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) = ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐻 Σg ( ( 𝐶𝐹 ) ↾ 𝑧 ) ) ) )
64 63 fveq2d ( 𝜑 → ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) ) = ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐻 Σg ( ( 𝐶𝐹 ) ↾ 𝑧 ) ) ) ) )
65 42 64 eqtr4d ( 𝜑 → ( 𝐻 tsums ( 𝐶𝐹 ) ) = ( ( 𝐾 fLimf ( ( 𝒫 𝐴 ∩ Fin ) filGen ran ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ { 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ∣ 𝑦𝑧 } ) ) ) ‘ ( 𝐶 ∘ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝐺 Σg ( 𝐹𝑧 ) ) ) ) ) )
66 34 65 eleqtrrd ( 𝜑 → ( 𝐶𝑋 ) ∈ ( 𝐻 tsums ( 𝐶𝐹 ) ) )