Metamath Proof Explorer


Theorem tgpmulg

Description: In a topological group, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses tgpmulg.j
|- J = ( TopOpen ` G )
tgpmulg.t
|- .x. = ( .g ` G )
tgpmulg.b
|- B = ( Base ` G )
Assertion tgpmulg
|- ( ( G e. TopGrp /\ N e. ZZ ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )

Proof

Step Hyp Ref Expression
1 tgpmulg.j
 |-  J = ( TopOpen ` G )
2 tgpmulg.t
 |-  .x. = ( .g ` G )
3 tgpmulg.b
 |-  B = ( Base ` G )
4 tgptmd
 |-  ( G e. TopGrp -> G e. TopMnd )
5 1 2 3 tmdmulg
 |-  ( ( G e. TopMnd /\ N e. NN0 ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )
6 4 5 sylan
 |-  ( ( G e. TopGrp /\ N e. NN0 ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )
7 6 adantlr
 |-  ( ( ( G e. TopGrp /\ N e. ZZ ) /\ N e. NN0 ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )
8 simpllr
 |-  ( ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) /\ x e. B ) -> N e. ZZ )
9 8 zcnd
 |-  ( ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) /\ x e. B ) -> N e. CC )
10 9 negnegd
 |-  ( ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) /\ x e. B ) -> -u -u N = N )
11 10 oveq1d
 |-  ( ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) /\ x e. B ) -> ( -u -u N .x. x ) = ( N .x. x ) )
12 eqid
 |-  ( invg ` G ) = ( invg ` G )
13 3 2 12 mulgnegnn
 |-  ( ( -u N e. NN /\ x e. B ) -> ( -u -u N .x. x ) = ( ( invg ` G ) ` ( -u N .x. x ) ) )
14 13 adantll
 |-  ( ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) /\ x e. B ) -> ( -u -u N .x. x ) = ( ( invg ` G ) ` ( -u N .x. x ) ) )
15 11 14 eqtr3d
 |-  ( ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) /\ x e. B ) -> ( N .x. x ) = ( ( invg ` G ) ` ( -u N .x. x ) ) )
16 15 mpteq2dva
 |-  ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) -> ( x e. B |-> ( N .x. x ) ) = ( x e. B |-> ( ( invg ` G ) ` ( -u N .x. x ) ) ) )
17 1 3 tgptopon
 |-  ( G e. TopGrp -> J e. ( TopOn ` B ) )
18 17 ad2antrr
 |-  ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) -> J e. ( TopOn ` B ) )
19 4 adantr
 |-  ( ( G e. TopGrp /\ N e. ZZ ) -> G e. TopMnd )
20 nnnn0
 |-  ( -u N e. NN -> -u N e. NN0 )
21 1 2 3 tmdmulg
 |-  ( ( G e. TopMnd /\ -u N e. NN0 ) -> ( x e. B |-> ( -u N .x. x ) ) e. ( J Cn J ) )
22 19 20 21 syl2an
 |-  ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) -> ( x e. B |-> ( -u N .x. x ) ) e. ( J Cn J ) )
23 1 12 tgpinv
 |-  ( G e. TopGrp -> ( invg ` G ) e. ( J Cn J ) )
24 23 ad2antrr
 |-  ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) -> ( invg ` G ) e. ( J Cn J ) )
25 18 22 24 cnmpt11f
 |-  ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) -> ( x e. B |-> ( ( invg ` G ) ` ( -u N .x. x ) ) ) e. ( J Cn J ) )
26 16 25 eqeltrd
 |-  ( ( ( G e. TopGrp /\ N e. ZZ ) /\ -u N e. NN ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )
27 26 adantrl
 |-  ( ( ( G e. TopGrp /\ N e. ZZ ) /\ ( N e. RR /\ -u N e. NN ) ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )
28 simpr
 |-  ( ( G e. TopGrp /\ N e. ZZ ) -> N e. ZZ )
29 elznn0nn
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
30 28 29 sylib
 |-  ( ( G e. TopGrp /\ N e. ZZ ) -> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
31 7 27 30 mpjaodan
 |-  ( ( G e. TopGrp /\ N e. ZZ ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )