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 ( 𝐶 ∘ 𝐹 ) ) )