tgpmulg2

Description: In a topological monoid, the group multiple function is jointly continuous (although this is not saying much as one of the factors is discrete). Use zdis to write the left topology as a subset of the complex numbers. (Contributed by Mario Carneiro, 19-Sep-2015)

	Ref	Expression
Hypotheses	tgpmulg.j	$⊢ J = TopOpen (G)$
	tgpmulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	tgpmulg2	$⊢ G \in TopGrp \to \underset{˙}{\cdot} \in ((𝒫 ℤ \times_{t} J) Cn J)$

Proof

Step	Hyp	Ref	Expression
1		tgpmulg.j	$⊢ J = TopOpen (G)$
2		tgpmulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		zex	$⊢ ℤ \in V$
4	3	a1i	$⊢ G \in TopGrp \to ℤ \in V$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6	1 5	tgptopon	$⊢ G \in TopGrp \to J \in TopOn ({Base}_{G})$
7		topontop	$⊢ J \in TopOn ({Base}_{G}) \to J \in Top$
8	6 7	syl	$⊢ G \in TopGrp \to J \in Top$
9	5 2	mulgfn	$⊢ \underset{˙}{\cdot} Fn (ℤ \times {Base}_{G})$
10	9	a1i	$⊢ G \in TopGrp \to \underset{˙}{\cdot} Fn (ℤ \times {Base}_{G})$
11	1 2 5	tgpmulg	$⊢ (G \in TopGrp \land n \in ℤ) \to (x \in {Base}_{G} ⟼ n \underset{˙}{\cdot} x) \in (J Cn J)$
12	4 6 8 10 11	txdis1cn	$⊢ G \in TopGrp \to \underset{˙}{\cdot} \in ((𝒫 ℤ \times_{t} J) Cn J)$

Metamath Proof Explorer

Theorem tgpmulg2

Proof