This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgpmulg

Description: In a topological group, 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 tgpmulg ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step Hyp Ref Expression
1 tgpmulg.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2 tgpmulg.t ⊢ · = ( .g ‘ 𝐺 )
3 tgpmulg.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
4 tgptmd ⊢ ( 𝐺 ∈ TopGrp → 𝐺 ∈ TopMnd )
5 1 2 3 tmdmulg ⊢ ( ( 𝐺 ∈ TopMnd ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
6 4 5 sylan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
7 6 adantlr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
8 simpllr ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ℤ )
9 8 zcnd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ℂ )
10 9 negnegd ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → - - 𝑁 = 𝑁 )
11 10 oveq1d ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( - - 𝑁 · 𝑥 ) = ( 𝑁 · 𝑥 ) )
12 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
13 3 2 12 mulgnegnn ⊢ ( ( - 𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐵 ) → ( - - 𝑁 · 𝑥 ) = ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑥 ) ) )
14 13 adantll ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( - - 𝑁 · 𝑥 ) = ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑥 ) ) )
15 11 14 eqtr3d ⊢ ( ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑁 · 𝑥 ) = ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑥 ) ) )
16 15 mpteq2dva ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑥 ) ) ) )
17 1 3 tgptopon ⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
18 17 ad2antrr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
19 4 adantr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) → 𝐺 ∈ TopMnd )
20 nnnn0 ⊢ ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℕ0 )
21 1 2 3 tmdmulg ⊢ ( ( 𝐺 ∈ TopMnd ∧ - 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ 𝐵 ↦ ( - 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
22 19 20 21 syl2an ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑥 ∈ 𝐵 ↦ ( - 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
23 1 12 tgpinv ⊢ ( 𝐺 ∈ TopGrp → ( invg ‘ 𝐺 ) ∈ ( 𝐽 Cn 𝐽 ) )
24 23 ad2antrr ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) → ( invg ‘ 𝐺 ) ∈ ( 𝐽 Cn 𝐽 ) )
25 18 22 24 cnmpt11f ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑥 ∈ 𝐵 ↦ ( ( invg ‘ 𝐺 ) ‘ ( - 𝑁 · 𝑥 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
26 16 25 eqeltrd ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
27 26 adantrl ⊢ ( ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
28 simpr ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
29 elznn0nn ⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
30 28 29 sylib ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
31 7 27 30 mpjaodan ⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑁 ∈ ℤ ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝑁 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )