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