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 𝐽 ) )