Metamath Proof Explorer

Theorem tgphaus

Description: A topological group is Hausdorff iff the identity subgroup is closed. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses tgphaus.1 
|- .0. = ( 0g ` G )
tgphaus.j 
|- J = ( TopOpen ` G )
Assertion tgphaus 
|- ( G e. TopGrp -> ( J e. Haus <-> { .0. } e. ( Clsd ` J ) ) )

Proof

Step Hyp Ref Expression
1 tgphaus.1 
 |-  .0. = ( 0g ` G )
2 tgphaus.j 
 |-  J = ( TopOpen ` G )
3 tgpgrp 
 |-  ( G e. TopGrp -> G e. Grp )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 4 1 grpidcl 
 |-  ( G e. Grp -> .0. e. ( Base ` G ) )
6 3 5 syl 
 |-  ( G e. TopGrp -> .0. e. ( Base ` G ) )
7 2 4 tgptopon 
 |-  ( G e. TopGrp -> J e. ( TopOn ` ( Base ` G ) ) )
8 toponuni 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> ( Base ` G ) = U. J )
9 7 8 syl 
 |-  ( G e. TopGrp -> ( Base ` G ) = U. J )
10 6 9 eleqtrd 
 |-  ( G e. TopGrp -> .0. e. U. J )
11 eqid 
 |-  U. J = U. J
12 11 sncld 
 |-  ( ( J e. Haus /\ .0. e. U. J ) -> { .0. } e. ( Clsd ` J ) )
13 12 expcom 
 |-  ( .0. e. U. J -> ( J e. Haus -> { .0. } e. ( Clsd ` J ) ) )
14 10 13 syl 
 |-  ( G e. TopGrp -> ( J e. Haus -> { .0. } e. ( Clsd ` J ) ) )
15 eqid 
 |-  ( -g ` G ) = ( -g ` G )
16 2 15 tgpsubcn 
 |-  ( G e. TopGrp -> ( -g ` G ) e. ( ( J tX J ) Cn J ) )
17 cnclima 
 |-  ( ( ( -g ` G ) e. ( ( J tX J ) Cn J ) /\ { .0. } e. ( Clsd ` J ) ) -> ( `' ( -g ` G ) " { .0. } ) e. ( Clsd ` ( J tX J ) ) )
18 17 ex 
 |-  ( ( -g ` G ) e. ( ( J tX J ) Cn J ) -> ( { .0. } e. ( Clsd ` J ) -> ( `' ( -g ` G ) " { .0. } ) e. ( Clsd ` ( J tX J ) ) ) )
19 16 18 syl 
 |-  ( G e. TopGrp -> ( { .0. } e. ( Clsd ` J ) -> ( `' ( -g ` G ) " { .0. } ) e. ( Clsd ` ( J tX J ) ) ) )
20 cnvimass 
 |-  ( `' ( -g ` G ) " { .0. } ) C_ dom ( -g ` G )
21 4 15 grpsubf 
 |-  ( G e. Grp -> ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) )
22 3 21 syl 
 |-  ( G e. TopGrp -> ( -g ` G ) : ( ( Base ` G ) X. ( Base ` G ) ) --> ( Base ` G ) )
23 20 22 fssdm 
 |-  ( G e. TopGrp -> ( `' ( -g ` G ) " { .0. } ) C_ ( ( Base ` G ) X. ( Base ` G ) ) )
24 relxp 
 |-  Rel ( ( Base ` G ) X. ( Base ` G ) )
25 relss 
 |-  ( ( `' ( -g ` G ) " { .0. } ) C_ ( ( Base ` G ) X. ( Base ` G ) ) -> ( Rel ( ( Base ` G ) X. ( Base ` G ) ) -> Rel ( `' ( -g ` G ) " { .0. } ) ) )
26 23 24 25 mpisyl 
 |-  ( G e. TopGrp -> Rel ( `' ( -g ` G ) " { .0. } ) )
27 dfrel4v 
 |-  ( Rel ( `' ( -g ` G ) " { .0. } ) <-> ( `' ( -g ` G ) " { .0. } ) = { <. x , y >. | x ( `' ( -g ` G ) " { .0. } ) y } )
28 26 27 sylib 
 |-  ( G e. TopGrp -> ( `' ( -g ` G ) " { .0. } ) = { <. x , y >. | x ( `' ( -g ` G ) " { .0. } ) y } )
29 22 ffnd 
 |-  ( G e. TopGrp -> ( -g ` G ) Fn ( ( Base ` G ) X. ( Base ` G ) ) )
30 elpreima 
 |-  ( ( -g ` G ) Fn ( ( Base ` G ) X. ( Base ` G ) ) -> ( <. x , y >. e. ( `' ( -g ` G ) " { .0. } ) <-> ( <. x , y >. e. ( ( Base ` G ) X. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. { .0. } ) ) )
31 29 30 syl 
 |-  ( G e. TopGrp -> ( <. x , y >. e. ( `' ( -g ` G ) " { .0. } ) <-> ( <. x , y >. e. ( ( Base ` G ) X. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. { .0. } ) ) )
32 opelxp 
 |-  ( <. x , y >. e. ( ( Base ` G ) X. ( Base ` G ) ) <-> ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) )
33 32 anbi1i 
 |-  ( ( <. x , y >. e. ( ( Base ` G ) X. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. { .0. } ) <-> ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. { .0. } ) )
34 4 1 15 grpsubeq0 
 |-  ( ( G e. Grp /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( ( x ( -g ` G ) y ) = .0. <-> x = y ) )
35 34 3expb 
 |-  ( ( G e. Grp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) = .0. <-> x = y ) )
36 3 35 sylan 
 |-  ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( ( x ( -g ` G ) y ) = .0. <-> x = y ) )
37 df-ov 
 |-  ( x ( -g ` G ) y ) = ( ( -g ` G ) ` <. x , y >. )
38 37 eleq1i 
 |-  ( ( x ( -g ` G ) y ) e. { .0. } <-> ( ( -g ` G ) ` <. x , y >. ) e. { .0. } )
39 ovex 
 |-  ( x ( -g ` G ) y ) e. _V
40 39 elsn 
 |-  ( ( x ( -g ` G ) y ) e. { .0. } <-> ( x ( -g ` G ) y ) = .0. )
41 38 40 bitr3i 
 |-  ( ( ( -g ` G ) ` <. x , y >. ) e. { .0. } <-> ( x ( -g ` G ) y ) = .0. )
42 equcom 
 |-  ( y = x <-> x = y )
43 36 41 42 3bitr4g 
 |-  ( ( G e. TopGrp /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) ) -> ( ( ( -g ` G ) ` <. x , y >. ) e. { .0. } <-> y = x ) )
44 43 pm5.32da 
 |-  ( G e. TopGrp -> ( ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. { .0. } ) <-> ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ y = x ) ) )
45 33 44 syl5bb 
 |-  ( G e. TopGrp -> ( ( <. x , y >. e. ( ( Base ` G ) X. ( Base ` G ) ) /\ ( ( -g ` G ) ` <. x , y >. ) e. { .0. } ) <-> ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ y = x ) ) )
46 31 45 bitrd 
 |-  ( G e. TopGrp -> ( <. x , y >. e. ( `' ( -g ` G ) " { .0. } ) <-> ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ y = x ) ) )
47 df-br 
 |-  ( x ( `' ( -g ` G ) " { .0. } ) y <-> <. x , y >. e. ( `' ( -g ` G ) " { .0. } ) )
48 eleq1w 
 |-  ( y = x -> ( y e. ( Base ` G ) <-> x e. ( Base ` G ) ) )
49 48 biimparc 
 |-  ( ( x e. ( Base ` G ) /\ y = x ) -> y e. ( Base ` G ) )
50 49 pm4.71i 
 |-  ( ( x e. ( Base ` G ) /\ y = x ) <-> ( ( x e. ( Base ` G ) /\ y = x ) /\ y e. ( Base ` G ) ) )
51 an32 
 |-  ( ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ y = x ) <-> ( ( x e. ( Base ` G ) /\ y = x ) /\ y e. ( Base ` G ) ) )
52 50 51 bitr4i 
 |-  ( ( x e. ( Base ` G ) /\ y = x ) <-> ( ( x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ y = x ) )
53 46 47 52 3bitr4g 
 |-  ( G e. TopGrp -> ( x ( `' ( -g ` G ) " { .0. } ) y <-> ( x e. ( Base ` G ) /\ y = x ) ) )
54 53 opabbidv 
 |-  ( G e. TopGrp -> { <. x , y >. | x ( `' ( -g ` G ) " { .0. } ) y } = { <. x , y >. | ( x e. ( Base ` G ) /\ y = x ) } )
55 opabresid 
 |-  ( _I |` ( Base ` G ) ) = { <. x , y >. | ( x e. ( Base ` G ) /\ y = x ) }
56 54 55 eqtr4di 
 |-  ( G e. TopGrp -> { <. x , y >. | x ( `' ( -g ` G ) " { .0. } ) y } = ( _I |` ( Base ` G ) ) )
57 9 reseq2d 
 |-  ( G e. TopGrp -> ( _I |` ( Base ` G ) ) = ( _I |` U. J ) )
58 28 56 57 3eqtrd 
 |-  ( G e. TopGrp -> ( `' ( -g ` G ) " { .0. } ) = ( _I |` U. J ) )
59 58 eleq1d 
 |-  ( G e. TopGrp -> ( ( `' ( -g ` G ) " { .0. } ) e. ( Clsd ` ( J tX J ) ) <-> ( _I |` U. J ) e. ( Clsd ` ( J tX J ) ) ) )
60 19 59 sylibd 
 |-  ( G e. TopGrp -> ( { .0. } e. ( Clsd ` J ) -> ( _I |` U. J ) e. ( Clsd ` ( J tX J ) ) ) )
61 topontop 
 |-  ( J e. ( TopOn ` ( Base ` G ) ) -> J e. Top )
62 7 61 syl 
 |-  ( G e. TopGrp -> J e. Top )
63 11 hausdiag 
 |-  ( J e. Haus <-> ( J e. Top /\ ( _I |` U. J ) e. ( Clsd ` ( J tX J ) ) ) )
64 63 baib 
 |-  ( J e. Top -> ( J e. Haus <-> ( _I |` U. J ) e. ( Clsd ` ( J tX J ) ) ) )
65 62 64 syl 
 |-  ( G e. TopGrp -> ( J e. Haus <-> ( _I |` U. J ) e. ( Clsd ` ( J tX J ) ) ) )
66 60 65 sylibrd 
 |-  ( G e. TopGrp -> ( { .0. } e. ( Clsd ` J ) -> J e. Haus ) )
67 14 66 impbid 
 |-  ( G e. TopGrp -> ( J e. Haus <-> { .0. } e. ( Clsd ` J ) ) )