Theorem 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	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
	tgpmulg.t	⊢ · = ( .g ‘ 𝐺 )
Assertion	tgpmulg2	⊢ ( 𝐺 ∈ TopGrp → · ∈ ( ( 𝒫 ℤ ×t 𝐽 ) Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		tgpmulg.j	⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
2		tgpmulg.t	⊢ · = ( .g ‘ 𝐺 )
3		zex	⊢ ℤ ∈ V
4	3	a1i	⊢ ( 𝐺 ∈ TopGrp → ℤ ∈ V )
5		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
6	1 5	tgptopon	⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) )
7		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ ( Base ‘ 𝐺 ) ) → 𝐽 ∈ Top )
8	6 7	syl	⊢ ( 𝐺 ∈ TopGrp → 𝐽 ∈ Top )
9	5 2	mulgfn	⊢ · Fn ( ℤ × ( Base ‘ 𝐺 ) )
10	9	a1i	⊢ ( 𝐺 ∈ TopGrp → · Fn ( ℤ × ( Base ‘ 𝐺 ) ) )
11	1 2 5	tgpmulg	⊢ ( ( 𝐺 ∈ TopGrp ∧ 𝑛 ∈ ℤ ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑛 · 𝑥 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
12	4 6 8 10 11	txdis1cn	⊢ ( 𝐺 ∈ TopGrp → · ∈ ( ( 𝒫 ℤ ×t 𝐽 ) Cn 𝐽 ) )