Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgpmulg Structured version   Unicode version

Theorem tgpmulg 18115
 Description: In a topological group, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.)
Hypotheses
Ref Expression
tgpmulg.j
tgpmulg.t .g
tgpmulg.b
Assertion
Ref Expression
tgpmulg
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem tgpmulg
StepHypRef Expression
1 tgptmd 18101 . . . 4 TopMnd
2 tgpmulg.j . . . . 5
3 tgpmulg.t . . . . 5 .g
4 tgpmulg.b . . . . 5
52, 3, 4tmdmulg 18114 . . . 4 TopMnd
61, 5sylan 458 . . 3
8 simpllr 736 . . . . . . . . 9
98zcnd 10368 . . . . . . . 8
109negnegd 9394 . . . . . . 7
1110oveq1d 6088 . . . . . 6
12 eqid 2435 . . . . . . . 8
134, 3, 12mulgnegnn 14892 . . . . . . 7
1413adantll 695 . . . . . 6
1511, 14eqtr3d 2469 . . . . 5
1615mpteq2dva 4287 . . . 4
172, 4tgptopon 18104 . . . . . 6 TopOn
1817ad2antrr 707 . . . . 5 TopOn
191adantr 452 . . . . . 6 TopMnd
20 nnnn0 10220 . . . . . 6
212, 3, 4tmdmulg 18114 . . . . . 6 TopMnd
2219, 20, 21syl2an 464 . . . . 5
232, 12tgpinv 18107 . . . . . 6
2423ad2antrr 707 . . . . 5
2518, 22, 24cnmpt11f 17688 . . . 4
2616, 25eqeltrd 2509 . . 3