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	$⊢ J = TopOpen (G)$
	tgpmulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	tgpmulg.b	$⊢ B = {Base}_{G}$
Assertion	tmdmulg	$⊢ (G \in TopMnd \land N \in ℕ_{0}) \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		oveq1	$⊢ n = 0 \to n \underset{˙}{\cdot} x = 0 \underset{˙}{\cdot} x$
5		eqid	$⊢ 0_{G} = 0_{G}$
6	3 5 2	mulg0	$⊢ x \in B \to 0 \underset{˙}{\cdot} x = 0_{G}$
7	4 6	sylan9eq	$⊢ (n = 0 \land x \in B) \to n \underset{˙}{\cdot} x = 0_{G}$
8	7	mpteq2dva	$⊢ n = 0 \to (x \in B ⟼ n \underset{˙}{\cdot} x) = (x \in B ⟼ 0_{G})$
9	8	eleq1d	$⊢ n = 0 \to ((x \in B ⟼ n \underset{˙}{\cdot} x) \in (J Cn J) \leftrightarrow (x \in B ⟼ 0_{G}) \in (J Cn J))$
10		oveq1	$⊢ n = k \to n \underset{˙}{\cdot} x = k \underset{˙}{\cdot} x$
11	10	mpteq2dv	$⊢ n = k \to (x \in B ⟼ n \underset{˙}{\cdot} x) = (x \in B ⟼ k \underset{˙}{\cdot} x)$
12	11	eleq1d	$⊢ n = k \to ((x \in B ⟼ n \underset{˙}{\cdot} x) \in (J Cn J) \leftrightarrow (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J))$
13		oveq1	$⊢ n = k + 1 \to n \underset{˙}{\cdot} x = (k + 1) \underset{˙}{\cdot} x$
14	13	mpteq2dv	$⊢ n = k + 1 \to (x \in B ⟼ n \underset{˙}{\cdot} x) = (x \in B ⟼ (k + 1) \underset{˙}{\cdot} x)$
15	14	eleq1d	$⊢ n = k + 1 \to ((x \in B ⟼ n \underset{˙}{\cdot} x) \in (J Cn J) \leftrightarrow (x \in B ⟼ (k + 1) \underset{˙}{\cdot} x) \in (J Cn J))$
16		oveq1	$⊢ n = N \to n \underset{˙}{\cdot} x = N \underset{˙}{\cdot} x$
17	16	mpteq2dv	$⊢ n = N \to (x \in B ⟼ n \underset{˙}{\cdot} x) = (x \in B ⟼ N \underset{˙}{\cdot} x)$
18	17	eleq1d	$⊢ n = N \to ((x \in B ⟼ n \underset{˙}{\cdot} x) \in (J Cn J) \leftrightarrow (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J))$
19	1 3	tmdtopon	$⊢ G \in TopMnd \to J \in TopOn (B)$
20		tmdmnd	$⊢ G \in TopMnd \to G \in Mnd$
21	3 5	mndidcl	$⊢ G \in Mnd \to 0_{G} \in B$
22	20 21	syl	$⊢ G \in TopMnd \to 0_{G} \in B$
23	19 19 22	cnmptc	$⊢ G \in TopMnd \to (x \in B ⟼ 0_{G}) \in (J Cn J)$
24		oveq2	$⊢ x = y \to (k + 1) \underset{˙}{\cdot} x = (k + 1) \underset{˙}{\cdot} y$
25	24	cbvmptv	$⊢ (x \in B ⟼ (k + 1) \underset{˙}{\cdot} x) = (y \in B ⟼ (k + 1) \underset{˙}{\cdot} y)$
26		eqid	$⊢ +_{G} = +_{G}$
27	3 2 26	mulgnn0p1	$⊢ (G \in Mnd \land k \in ℕ_{0} \land y \in B) \to (k + 1) \underset{˙}{\cdot} y = (k \underset{˙}{\cdot} y) +_{G} y$
28	20 27	syl3an1	$⊢ (G \in TopMnd \land k \in ℕ_{0} \land y \in B) \to (k + 1) \underset{˙}{\cdot} y = (k \underset{˙}{\cdot} y) +_{G} y$
29	28	ad4ant124	$⊢ (((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \land y \in B) \to (k + 1) \underset{˙}{\cdot} y = (k \underset{˙}{\cdot} y) +_{G} y$
30	29	mpteq2dva	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to (y \in B ⟼ (k + 1) \underset{˙}{\cdot} y) = (y \in B ⟼ (k \underset{˙}{\cdot} y) +_{G} y)$
31	25 30	syl5eq	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to (x \in B ⟼ (k + 1) \underset{˙}{\cdot} x) = (y \in B ⟼ (k \underset{˙}{\cdot} y) +_{G} y)$
32		simpll	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to G \in TopMnd$
33	32 19	syl	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to J \in TopOn (B)$
34		oveq2	$⊢ x = y \to k \underset{˙}{\cdot} x = k \underset{˙}{\cdot} y$
35	34	cbvmptv	$⊢ (x \in B ⟼ k \underset{˙}{\cdot} x) = (y \in B ⟼ k \underset{˙}{\cdot} y)$
36		simpr	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)$
37	35 36	eqeltrrid	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to (y \in B ⟼ k \underset{˙}{\cdot} y) \in (J Cn J)$
38	33	cnmptid	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to (y \in B ⟼ y) \in (J Cn J)$
39	1 26 32 33 37 38	cnmpt1plusg	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to (y \in B ⟼ (k \underset{˙}{\cdot} y) +_{G} y) \in (J Cn J)$
40	31 39	eqeltrd	$⊢ ((G \in TopMnd \land k \in ℕ_{0}) \land (x \in B ⟼ k \underset{˙}{\cdot} x) \in (J Cn J)) \to (x \in B ⟼ (k + 1) \underset{˙}{\cdot} x) \in (J Cn J)$
41	9 12 15 18 23 40	nn0indd	$⊢ (G \in TopMnd \land N \in ℕ_{0}) \to (x \in B ⟼ N \underset{˙}{\cdot} x) \in (J Cn J)$

Metamath Proof Explorer

Theorem tmdmulg

Proof