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	$⊢ J = TopOpen (G)$
	tgpmulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	tgpmulg.b	$⊢ B = {Base}_{G}$
Assertion	tgpmulg	$⊢ (G \in TopGrp \land N \in ℤ) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J)$

Proof

Step	Hyp	Ref	Expression
1		tgpmulg.j	$⊢ J = TopOpen (G)$
2		tgpmulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		tgpmulg.b	$⊢ B = {Base}_{G}$
4		tgptmd	$⊢ G \in TopGrp \to G \in TopMnd$
5	1 2 3	tmdmulg	$⊢ (G \in TopMnd \land N \in ℕ_{0}) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J)$
6	4 5	sylan	$⊢ (G \in TopGrp \land N \in ℕ_{0}) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J)$
7	6	adantlr	$⊢ ((G \in TopGrp \land N \in ℤ) \land N \in ℕ_{0}) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J)$
8		simpllr	$⊢ (((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \land x \in B) \to N \in ℤ$
9	8	zcnd	$⊢ (((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \land x \in B) \to N \in ℂ$
10	9	negnegd	$⊢ (((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \land x \in B) \to - -N = N$
11	10	oveq1d	$⊢ (((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \land x \in B) \to (- -N) \underset{˙}{\cdot} x = N \underset{˙}{\cdot} x$
12		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
13	3 2 12	mulgnegnn	$⊢ (- N \in ℕ \land x \in B) \to (- -N) \underset{˙}{\cdot} x = {inv}_{g} (G) (-N \underset{˙}{\cdot} x)$
14	13	adantll	$⊢ (((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \land x \in B) \to (- -N) \underset{˙}{\cdot} x = {inv}_{g} (G) (-N \underset{˙}{\cdot} x)$
15	11 14	eqtr3d	$⊢ (((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \land x \in B) \to N \underset{˙}{\cdot} x = {inv}_{g} (G) (-N \underset{˙}{\cdot} x)$
16	15	mpteq2dva	$⊢ ((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \to (x \in B ⟼ N \underset{˙}{\cdot} x) = (x \in B ⟼ {inv}_{g} (G) (-N \underset{˙}{\cdot} x))$
17	1 3	tgptopon	$⊢ G \in TopGrp \to J \in TopOn (B)$
18	17	ad2antrr	$⊢ ((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \to J \in TopOn (B)$
19	4	adantr	$⊢ (G \in TopGrp \land N \in ℤ) \to G \in TopMnd$
20		nnnn0	$⊢ - N \in ℕ \to - N \in ℕ_{0}$
21	1 2 3	tmdmulg	$⊢ (G \in TopMnd \land - N \in ℕ_{0}) \to (x \in B ⟼ -N \underset{˙}{\cdot} x) \in (J Cn J)$
22	19 20 21	syl2an	$⊢ ((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \to (x \in B ⟼ -N \underset{˙}{\cdot} x) \in (J Cn J)$
23	1 12	tgpinv	$⊢ G \in TopGrp \to {inv}_{g} (G) \in (J Cn J)$
24	23	ad2antrr	$⊢ ((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \to {inv}_{g} (G) \in (J Cn J)$
25	18 22 24	cnmpt11f	$⊢ ((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \to (x \in B ⟼ {inv}_{g} (G) (-N \underset{˙}{\cdot} x)) \in (J Cn J)$
26	16 25	eqeltrd	$⊢ ((G \in TopGrp \land N \in ℤ) \land - N \in ℕ) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J)$
27	26	adantrl	$⊢ ((G \in TopGrp \land N \in ℤ) \land (N \in ℝ \land - N \in ℕ)) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J)$
28		simpr	$⊢ (G \in TopGrp \land N \in ℤ) \to N \in ℤ$
29		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
30	28 29	sylib	$⊢ (G \in TopGrp \land N \in ℤ) \to (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
31	7 27 30	mpjaodan	$⊢ (G \in TopGrp \land N \in ℤ) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J)$

Metamath Proof Explorer

Theorem tgpmulg

Proof