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 ⊢ J = TopOpen ⁡ G
tgpmulg.t ⊢ · ˙ = ⋅ G
Assertion tgpmulg2 ⊢ G ∈ TopGrp → · ˙ ∈ 𝒫 ℤ × t J Cn J

Proof

Step Hyp Ref Expression
1 tgpmulg.j ⊢ J = TopOpen ⁡ G
2 tgpmulg.t ⊢ · ˙ = ⋅ G
3 zex ⊢ ℤ ∈ V
4 3 a1i ⊢ G ∈ TopGrp → ℤ ∈ V
5 eqid ⊢ Base G = Base G
6 1 5 tgptopon ⊢ G ∈ TopGrp → J ∈ TopOn ⁡ Base G
7 topontop ⊢ J ∈ TopOn ⁡ Base G → J ∈ Top
8 6 7 syl ⊢ G ∈ TopGrp → J ∈ Top
9 5 2 mulgfn ⊢ · ˙ Fn ℤ × Base G
10 9 a1i ⊢ G ∈ TopGrp → · ˙ Fn ℤ × Base G
11 1 2 5 tgpmulg ⊢ G ∈ TopGrp ∧ n ∈ ℤ → x ∈ Base G ⟼ n · ˙ x ∈ J Cn J
12 4 6 8 10 11 txdis1cn ⊢ G ∈ TopGrp → · ˙ ∈ 𝒫 ℤ × t J Cn J