Metamath Proof Explorer

Theorem tgpt0

Description: Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypothesis tgpt1.j 
|- J = ( TopOpen ` G )
Assertion tgpt0 
|- ( G e. TopGrp -> ( J e. Haus <-> J e. Kol2 ) )

Proof

Step Hyp Ref Expression
1 tgpt1.j 
 |-  J = ( TopOpen ` G )
2 1 tgpt1 
 |-  ( G e. TopGrp -> ( J e. Haus <-> J e. Fre ) )
3 t1t0 
 |-  ( J e. Fre -> J e. Kol2 )
4 eleq2 
 |-  ( w = z -> ( x e. w <-> x e. z ) )
5 eleq2 
 |-  ( w = z -> ( y e. w <-> y e. z ) )
6 4 5 imbi12d 
 |-  ( w = z -> ( ( x e. w -> y e. w ) <-> ( x e. z -> y e. z ) ) )
7 6 rspccva 
 |-  ( ( A. w e. J ( x e. w -> y e. w ) /\ z e. J ) -> ( x e. z -> y e. z ) )
8 7 adantll 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ z e. J ) -> ( x e. z -> y e. z ) )
9 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
10 9 ad3antrrr 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> G e. Grp )
11 simpllr 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) )
12 11 simprd 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> y e. ( Base ` G ) )
13 eqid 
 |-  ( Base ` G ) = ( Base ` G )
14 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
15 eqid 
 |-  ( -g ` G ) = ( -g ` G )
16 13 14 15 grpsubid 
 |-  ( ( G e. Grp /\ y e. ( Base ` G ) ) -> ( y ( -g ` G ) y ) = ( 0g ` G ) )
17 10 12 16 syl2anc 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( y ( -g ` G ) y ) = ( 0g ` G ) )
18 17 oveq1d 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( ( y ( -g ` G ) y ) ( +g ` G ) x ) = ( ( 0g ` G ) ( +g ` G ) x ) )
19 11 simpld 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> x e. ( Base ` G ) )
20 eqid 
 |-  ( +g ` G ) = ( +g ` G )
21 13 20 14 grplid 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) ) -> ( ( 0g ` G ) ( +g ` G ) x ) = x )
22 10 19 21 syl2anc 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( ( 0g ` G ) ( +g ` G ) x ) = x )
23 18 22 eqtrd 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( ( y ( -g ` G ) y ) ( +g ` G ) x ) = x )
24 13 20 15 grpnpcan 
 |-  ( ( G e. Grp /\ y e. ( Base ` G ) /\ x e. ( Base ` G ) ) -> ( ( y ( -g ` G ) x ) ( +g ` G ) x ) = y )
25 10 12 19 24 syl3anc 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( ( y ( -g ` G ) x ) ( +g ` G ) x ) = y )
26 simprr 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> y e. z )
27 25 26 eqeltrd 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( ( y ( -g ` G ) x ) ( +g ` G ) x ) e. z )
28 oveq2 
 |-  ( a = x -> ( y ( -g ` G ) a ) = ( y ( -g ` G ) x ) )
29 28 oveq1d 
 |-  ( a = x -> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) = ( ( y ( -g ` G ) x ) ( +g ` G ) x ) )
30 29 eleq1d 
 |-  ( a = x -> ( ( ( y ( -g ` G ) a ) ( +g ` G ) x ) e. z <-> ( ( y ( -g ` G ) x ) ( +g ` G ) x ) e. z ) )
31 eqid 
 |-  ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) = ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) )
32 31 mptpreima 
 |-  ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) = { a e. ( Base ` G ) | ( ( y ( -g ` G ) a ) ( +g ` G ) x ) e. z }
33 30 32 elrab2 
 |-  ( x e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) <-> ( x e. ( Base ` G ) /\ ( ( y ( -g ` G ) x ) ( +g ` G ) x ) e. z ) )
34 19 27 33 sylanbrc 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> x e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) )
35 eleq2 
 |-  ( w = ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) -> ( x e. w <-> x e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) ) )
36 eleq2 
 |-  ( w = ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) -> ( y e. w <-> y e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) ) )
37 35 36 imbi12d 
 |-  ( w = ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) -> ( ( x e. w -> y e. w ) <-> ( x e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) -> y e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) ) ) )
38 simplr 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> A. w e. J ( x e. w -> y e. w ) )
39 tgptmd 
 |-  ( G e. TopGrp -> G e. TopMnd )
40 39 ad3antrrr 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> G e. TopMnd )
41 1 13 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` ( Base ` G ) ) )
42 41 ad3antrrr 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> J e. ( TopOn ` ( Base ` G ) ) )
43 42 42 12 cnmptc 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( a e. ( Base ` G ) |-> y ) e. ( J Cn J ) )
44 42 cnmptid 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( a e. ( Base ` G ) |-> a ) e. ( J Cn J ) )
45 1 15 tgpsubcn 
 |-  ( G e. TopGrp -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
46 45 ad3antrrr 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
47 42 43 44 46 cnmpt12f 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( a e. ( Base ` G ) |-> ( y ( -g ` G ) a ) ) e. ( J Cn J ) )
48 42 42 19 cnmptc 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( a e. ( Base ` G ) |-> x ) e. ( J Cn J ) )
49 1 20 40 42 47 48 cnmpt1plusg 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) e. ( J Cn J ) )
50 simprl 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> z e. J )
51 cnima 
 |-  ( ( ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) e. ( J Cn J ) /\ z e. J ) -> ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) e. J )
52 49 50 51 syl2anc 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) e. J )
53 37 38 52 rspcdva 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( x e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) -> y e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) ) )
54 34 53 mpd 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> y e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) )
55 oveq2 
 |-  ( a = y -> ( y ( -g ` G ) a ) = ( y ( -g ` G ) y ) )
56 55 oveq1d 
 |-  ( a = y -> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) = ( ( y ( -g ` G ) y ) ( +g ` G ) x ) )
57 56 eleq1d 
 |-  ( a = y -> ( ( ( y ( -g ` G ) a ) ( +g ` G ) x ) e. z <-> ( ( y ( -g ` G ) y ) ( +g ` G ) x ) e. z ) )
58 57 32 elrab2 
 |-  ( y e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) <-> ( y e. ( Base ` G ) /\ ( ( y ( -g ` G ) y ) ( +g ` G ) x ) e. z ) )
59 58 simprbi 
 |-  ( y e. ( `' ( a e. ( Base ` G ) |-> ( ( y ( -g ` G ) a ) ( +g ` G ) x ) ) " z ) -> ( ( y ( -g ` G ) y ) ( +g ` G ) x ) e. z )
60 54 59 syl 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> ( ( y ( -g ` G ) y ) ( +g ` G ) x ) e. z )
61 23 60 eqeltrrd 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ ( z e. J /\ y e. z ) ) -> x e. z )
62 61 expr 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ z e. J ) -> ( y e. z -> x e. z ) )
63 8 62 impbid 
 |-  ( ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) /\ z e. J ) -> ( x e. z <-> y e. z ) )
64 63 ralrimiva 
 |-  ( ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) /\ A. w e. J ( x e. w -> y e. w ) ) -> A. z e. J ( x e. z <-> y e. z ) )
65 64 ex 
 |-  ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( A. w e. J ( x e. w -> y e. w ) -> A. z e. J ( x e. z <-> y e. z ) ) )
66 65 imim1d 
 |-  ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( ( A. z e. J ( x e. z <-> y e. z ) -> x = y ) -> ( A. w e. J ( x e. w -> y e. w ) -> x = y ) ) )
67 66 ralimdvva 
 |-  ( G e. TopGrp -> ( A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( A. z e. J ( x e. z <-> y e. z ) -> x = y ) -> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( A. w e. J ( x e. w -> y e. w ) -> x = y ) ) )
68 ist0-2 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> ( J e. Kol2 <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( A. z e. J ( x e. z <-> y e. z ) -> x = y ) ) )
69 41 68 syl 
 |-  ( G e. TopGrp -> ( J e. Kol2 <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( A. z e. J ( x e. z <-> y e. z ) -> x = y ) ) )
70 ist1-2 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> ( J e. Fre <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( A. w e. J ( x e. w -> y e. w ) -> x = y ) ) )
71 41 70 syl 
 |-  ( G e. TopGrp -> ( J e. Fre <-> A. x e. ( Base ` G ) A. y e. ( Base ` G ) ( A. w e. J ( x e. w -> y e. w ) -> x = y ) ) )
72 67 69 71 3imtr4d 
 |-  ( G e. TopGrp -> ( J e. Kol2 -> J e. Fre ) )
73 3 72 impbid2 
 |-  ( G e. TopGrp -> ( J e. Fre <-> J e. Kol2 ) )
74 2 73 bitrd 
 |-  ( G e. TopGrp -> ( J e. Haus <-> J e. Kol2 ) )