Metamath Proof Explorer

Theorem tmdmulg

Description: In a topological monoid, 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 tmdmulg 
|- ( ( G e. TopMnd /\ N e. NN0 ) -> ( 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 oveq1 
 |-  ( n = 0 -> ( n .x. x ) = ( 0 .x. x ) )
5 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
6 3 5 2 mulg0 
 |-  ( x e. B -> ( 0 .x. x ) = ( 0g ` G ) )
7 4 6 sylan9eq 
 |-  ( ( n = 0 /\ x e. B ) -> ( n .x. x ) = ( 0g ` G ) )
8 7 mpteq2dva 
 |-  ( n = 0 -> ( x e. B |-> ( n .x. x ) ) = ( x e. B |-> ( 0g ` G ) ) )
9 8 eleq1d 
 |-  ( n = 0 -> ( ( x e. B |-> ( n .x. x ) ) e. ( J Cn J ) <-> ( x e. B |-> ( 0g ` G ) ) e. ( J Cn J ) ) )
10 oveq1 
 |-  ( n = k -> ( n .x. x ) = ( k .x. x ) )
11 10 mpteq2dv 
 |-  ( n = k -> ( x e. B |-> ( n .x. x ) ) = ( x e. B |-> ( k .x. x ) ) )
12 11 eleq1d 
 |-  ( n = k -> ( ( x e. B |-> ( n .x. x ) ) e. ( J Cn J ) <-> ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) )
13 oveq1 
 |-  ( n = ( k + 1 ) -> ( n .x. x ) = ( ( k + 1 ) .x. x ) )
14 13 mpteq2dv 
 |-  ( n = ( k + 1 ) -> ( x e. B |-> ( n .x. x ) ) = ( x e. B |-> ( ( k + 1 ) .x. x ) ) )
15 14 eleq1d 
 |-  ( n = ( k + 1 ) -> ( ( x e. B |-> ( n .x. x ) ) e. ( J Cn J ) <-> ( x e. B |-> ( ( k + 1 ) .x. x ) ) e. ( J Cn J ) ) )
16 oveq1 
 |-  ( n = N -> ( n .x. x ) = ( N .x. x ) )
17 16 mpteq2dv 
 |-  ( n = N -> ( x e. B |-> ( n .x. x ) ) = ( x e. B |-> ( N .x. x ) ) )
18 17 eleq1d 
 |-  ( n = N -> ( ( x e. B |-> ( n .x. x ) ) e. ( J Cn J ) <-> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) ) )
19 1 3 tmdtopon 
 |-  ( G e. TopMnd -> J e. ( TopOn ` B ) )
20 tmdmnd 
 |-  ( G e. TopMnd -> G e. Mnd )
21 3 5 mndidcl 
 |-  ( G e. Mnd -> ( 0g ` G ) e. B )
22 20 21 syl 
 |-  ( G e. TopMnd -> ( 0g ` G ) e. B )
23 19 19 22 cnmptc 
 |-  ( G e. TopMnd -> ( x e. B |-> ( 0g ` G ) ) e. ( J Cn J ) )
24 oveq2 
 |-  ( x = y -> ( ( k + 1 ) .x. x ) = ( ( k + 1 ) .x. y ) )
25 24 cbvmptv 
 |-  ( x e. B |-> ( ( k + 1 ) .x. x ) ) = ( y e. B |-> ( ( k + 1 ) .x. y ) )
26 eqid 
 |-  ( +g ` G ) = ( +g ` G )
27 3 2 26 mulgnn0p1 
 |-  ( ( G e. Mnd /\ k e. NN0 /\ y e. B ) -> ( ( k + 1 ) .x. y ) = ( ( k .x. y ) ( +g ` G ) y ) )
28 20 27 syl3an1 
 |-  ( ( G e. TopMnd /\ k e. NN0 /\ y e. B ) -> ( ( k + 1 ) .x. y ) = ( ( k .x. y ) ( +g ` G ) y ) )
29 28 ad4ant124 
 |-  ( ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) /\ y e. B ) -> ( ( k + 1 ) .x. y ) = ( ( k .x. y ) ( +g ` G ) y ) )
30 29 mpteq2dva 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> ( y e. B |-> ( ( k + 1 ) .x. y ) ) = ( y e. B |-> ( ( k .x. y ) ( +g ` G ) y ) ) )
31 25 30 syl5eq 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> ( x e. B |-> ( ( k + 1 ) .x. x ) ) = ( y e. B |-> ( ( k .x. y ) ( +g ` G ) y ) ) )
32 simpll 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> G e. TopMnd )
33 32 19 syl 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> J e. ( TopOn ` B ) )
34 oveq2 
 |-  ( x = y -> ( k .x. x ) = ( k .x. y ) )
35 34 cbvmptv 
 |-  ( x e. B |-> ( k .x. x ) ) = ( y e. B |-> ( k .x. y ) )
36 simpr 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) )
37 35 36 eqeltrrid 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> ( y e. B |-> ( k .x. y ) ) e. ( J Cn J ) )
38 33 cnmptid 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> ( y e. B |-> y ) e. ( J Cn J ) )
39 1 26 32 33 37 38 cnmpt1plusg 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> ( y e. B |-> ( ( k .x. y ) ( +g ` G ) y ) ) e. ( J Cn J ) )
40 31 39 eqeltrd 
 |-  ( ( ( G e. TopMnd /\ k e. NN0 ) /\ ( x e. B |-> ( k .x. x ) ) e. ( J Cn J ) ) -> ( x e. B |-> ( ( k + 1 ) .x. x ) ) e. ( J Cn J ) )
41 9 12 15 18 23 40 nn0indd 
 |-  ( ( G e. TopMnd /\ N e. NN0 ) -> ( x e. B |-> ( N .x. x ) ) e. ( J Cn J ) )