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