Metamath Proof Explorer

Theorem istgp2

Description: A group with a topology is a topological group iff the subtraction operation is continuous. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses tgpsubcn.2 
|- J = ( TopOpen ` G )
tgpsubcn.3 
|- .- = ( -g ` G )
Assertion istgp2 
|- ( G e. TopGrp <-> ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) )

Proof

Step Hyp Ref Expression
1 tgpsubcn.2 
 |-  J = ( TopOpen ` G )
2 tgpsubcn.3 
 |-  .- = ( -g ` G )
3 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
4 tgptps 
 |-  ( G e. TopGrp -> G e. TopSp )
5 1 2 tgpsubcn 
 |-  ( G e. TopGrp -> .- e. ( ( J tX J ) Cn J ) )
6 3 4 5 3jca 
 |-  ( G e. TopGrp -> ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) )
7 simp1 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> G e. Grp )
8 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
9 8 3ad2ant1 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> G e. Mnd )
10 simp2 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> G e. TopSp )
11 eqid 
 |-  ( Base ` G ) = ( Base ` G )
12 eqid 
 |-  ( +g ` G ) = ( +g ` G )
13 eqid 
 |-  ( invg ` G ) = ( invg ` G )
14 7 3ad2ant1 
 |-  ( ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> G e. Grp )
15 simp2 
 |-  ( ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> x e. ( Base ` G ) )
16 simp3 
 |-  ( ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> y e. ( Base ` G ) )
17 11 12 2 13 14 15 16 grpsubinv 
 |-  ( ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x .- ( ( invg ` G ) ` y ) ) = ( x ( +g ` G ) y ) )
18 17 mpoeq3dva 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x .- ( ( invg ` G ) ` y ) ) ) = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` G ) y ) ) )
19 eqid 
 |-  ( +f ` G ) = ( +f ` G )
20 11 12 19 plusffval 
 |-  ( +f ` G ) = ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x ( +g ` G ) y ) )
21 18 20 eqtr4di 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x .- ( ( invg ` G ) ` y ) ) ) = ( +f ` G ) )
22 11 1 istps 
 |-  ( G e. TopSp <-> J e. ( TopOn ` ( Base ` G ) ) )
23 10 22 sylib 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> J e. ( TopOn ` ( Base ` G ) ) )
24 23 23 cnmpt1st 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> x ) e. ( ( J tX J ) Cn J ) )
25 23 23 cnmpt2nd 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> y ) e. ( ( J tX J ) Cn J ) )
26 11 13 grpinvf 
 |-  ( G e. Grp -> ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) )
27 26 3ad2ant1 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( invg ` G ) : ( Base ` G ) --> ( Base ` G ) )
28 27 feqmptd 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( invg ` G ) = ( x e. ( Base ` G ) |-> ( ( invg ` G ) ` x ) ) )
29 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
30 11 2 13 29 grpinvval2 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( ( invg ` G ) ` x ) = ( ( 0g ` G ) .- x ) )
31 7 30 sylan 
 |-  ( ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) /\ x e. ( Base ` G ) ) -> ( ( invg ` G ) ` x ) = ( ( 0g ` G ) .- x ) )
32 31 mpteq2dva 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) |-> ( ( invg ` G ) ` x ) ) = ( x e. ( Base ` G ) |-> ( ( 0g ` G ) .- x ) ) )
33 28 32 eqtrd 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( invg ` G ) = ( x e. ( Base ` G ) |-> ( ( 0g ` G ) .- x ) ) )
34 11 29 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. ( Base ` G ) )
35 34 3ad2ant1 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( 0g ` G ) e. ( Base ` G ) )
36 23 23 35 cnmptc 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) |-> ( 0g ` G ) ) e. ( J Cn J ) )
37 23 cnmptid 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) |-> x ) e. ( J Cn J ) )
38 simp3 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> .- e. ( ( J tX J ) Cn J ) )
39 23 36 37 38 cnmpt12f 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) |-> ( ( 0g ` G ) .- x ) ) e. ( J Cn J ) )
40 33 39 eqeltrd 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( invg ` G ) e. ( J Cn J ) )
41 23 23 25 40 cnmpt21f 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( ( invg ` G ) ` y ) ) e. ( ( J tX J ) Cn J ) )
42 23 23 24 41 38 cnmpt22f 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( x e. ( Base ` G ) , y e. ( Base ` G ) |-> ( x .- ( ( invg ` G ) ` y ) ) ) e. ( ( J tX J ) Cn J ) )
43 21 42 eqeltrrd 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> ( +f ` G ) e. ( ( J tX J ) Cn J ) )
44 19 1 istmd 
 |-  ( G e. TopMnd <-> ( G e. Mnd /\ G e. TopSp /\ ( +f ` G ) e. ( ( J tX J ) Cn J ) ) )
45 9 10 43 44 syl3anbrc 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> G e. TopMnd )
46 1 13 istgp 
 |-  ( G e. TopGrp <-> ( G e. Grp /\ G e. TopMnd /\ ( invg ` G ) e. ( J Cn J ) ) )
47 7 45 40 46 syl3anbrc 
 |-  ( ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) -> G e. TopGrp )
48 6 47 impbii 
 |-  ( G e. TopGrp <-> ( G e. Grp /\ G e. TopSp /\ .- e. ( ( J tX J ) Cn J ) ) )