Metamath Proof Explorer

Theorem tmdmulg

Description: In a topological monoid, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses tgpmulg.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
tgpmulg.t ⊢ · = ( .g ‘ 𝐺 )
tgpmulg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion tmdmulg ( ( 𝐺 ∈ TopMnd ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 tgpmulg.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 tgpmulg.t ⊢ · = ( .g ‘ 𝐺 )
3 tgpmulg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 oveq1 ⊢ ( 𝑛 = 0 → ( 𝑛 · 𝑥 ) = ( 0 · 𝑥 ) )
5 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
6 3 5 2 mulg0 ⊢ ( 𝑥 ∈ 𝐵 → ( 0 · 𝑥 ) = ( 0g ‘ 𝐺 ) )
7 4 6 sylan9eq ⊢ ( ( 𝑛 = 0 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑛 · 𝑥 ) = ( 0g ‘ 𝐺 ) )
8 7 mpteq2dva ⊢ ( 𝑛 = 0 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 0g ‘ 𝐺 ) ) )
9 8 eleq1d ⊢ ( 𝑛 = 0 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑥 ∈ 𝐵 ↦ ( 0g ‘ 𝐺 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
10 oveq1 ⊢ ( 𝑛 = 𝑘 → ( 𝑛 · 𝑥 ) = ( 𝑘 · 𝑥 ) )
11 10 mpteq2dv ⊢ ( 𝑛 = 𝑘 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) )
12 11 eleq1d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
13 oveq1 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑛 · 𝑥 ) = ( ( 𝑘 + 1 ) · 𝑥 ) )
14 13 mpteq2dv ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑘 + 1 ) · 𝑥 ) ) )
15 14 eleq1d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑘 + 1 ) · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
16 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 · 𝑥 ) = ( 𝑁 · 𝑥 ) )
17 16 mpteq2dv ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∈ 𝐵 ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) )
18 17 eleq1d ⊢ ( 𝑛 = 𝑁 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ↔ ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) )
19 1 3 tmdtopon ⊢ ( 𝐺 ∈ TopMnd → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
20 tmdmnd ⊢ ( 𝐺 ∈ TopMnd → 𝐺 ∈ Mnd )
21 3 5 mndidcl ⊢ ( 𝐺 ∈ Mnd → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
22 20 21 syl ⊢ ( 𝐺 ∈ TopMnd → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
23 19 19 22 cnmptc ⊢ ( 𝐺 ∈ TopMnd → ( 𝑥 ∈ 𝐵 ↦ ( 0g ‘ 𝐺 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
24 oveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝑘 + 1 ) · 𝑥 ) = ( ( 𝑘 + 1 ) · 𝑦 ) )
25 24 cbvmptv ⊢ ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑘 + 1 ) · 𝑥 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝑘 + 1 ) · 𝑦 ) )
26 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
27 3 2 26 mulgnn0p1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑘 + 1 ) · 𝑦 ) = ( ( 𝑘 · 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) )
28 20 27 syl3an1 ⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑘 + 1 ) · 𝑦 ) = ( ( 𝑘 · 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) )
29 28 ad4ant124 ⊢ ( ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑘 + 1 ) · 𝑦 ) = ( ( 𝑘 · 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) )
30 29 mpteq2dva ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑦 ∈ 𝐵 ↦ ( ( 𝑘 + 1 ) · 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝑘 · 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ) )
31 25 30 syl5eq ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑘 + 1 ) · 𝑥 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( ( 𝑘 · 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ) )
32 simpll ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → 𝐺 ∈ TopMnd )
33 32 19 syl ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
34 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑘 · 𝑥 ) = ( 𝑘 · 𝑦 ) )
35 34 cbvmptv ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝑘 · 𝑦 ) )
36 simpr ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
37 35 36 eqeltrrid ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑦 ∈ 𝐵 ↦ ( 𝑘 · 𝑦 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
38 33 cnmptid ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑦 ∈ 𝐵 ↦ 𝑦 ) ∈ ( 𝐽 Cn 𝐽 ) )
39 1 26 32 33 37 38 cnmpt1plusg ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑦 ∈ 𝐵 ↦ ( ( 𝑘 · 𝑦 ) ( +g ‘ 𝐺 ) 𝑦 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
40 31 39 eqeltrd ⊢ ( ( ( 𝐺 ∈ TopMnd ∧ 𝑘 ∈ ℕ0 ) ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝑘 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) ) → ( 𝑥 ∈ 𝐵 ↦ ( ( 𝑘 + 1 ) · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
41 9 12 15 18 23 40 nn0indd ⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )