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