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