This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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