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=TopOpenG
Assertion tgpt0 GTopGrpJHausJKol2

Proof

Step Hyp Ref Expression
1 tgpt1.j J=TopOpenG
2 1 tgpt1 GTopGrpJHausJFre
3 t1t0 JFreJKol2
4 eleq2 w=zxwxz
5 eleq2 w=zywyz
6 4 5 imbi12d w=zxwywxzyz
7 6 rspccva wJxwywzJxzyz
8 7 adantll GTopGrpxBaseGyBaseGwJxwywzJxzyz
9 tgpgrp GTopGrpGGrp
10 9 ad3antrrr GTopGrpxBaseGyBaseGwJxwywzJyzGGrp
11 simpllr GTopGrpxBaseGyBaseGwJxwywzJyzxBaseGyBaseG
12 11 simprd GTopGrpxBaseGyBaseGwJxwywzJyzyBaseG
13 eqid BaseG=BaseG
14 eqid 0G=0G
15 eqid -G=-G
16 13 14 15 grpsubid GGrpyBaseGy-Gy=0G
17 10 12 16 syl2anc GTopGrpxBaseGyBaseGwJxwywzJyzy-Gy=0G
18 17 oveq1d GTopGrpxBaseGyBaseGwJxwywzJyzy-Gy+Gx=0G+Gx
19 11 simpld GTopGrpxBaseGyBaseGwJxwywzJyzxBaseG
20 eqid +G=+G
21 13 20 14 grplid GGrpxBaseG0G+Gx=x
22 10 19 21 syl2anc GTopGrpxBaseGyBaseGwJxwywzJyz0G+Gx=x
23 18 22 eqtrd GTopGrpxBaseGyBaseGwJxwywzJyzy-Gy+Gx=x
24 13 20 15 grpnpcan GGrpyBaseGxBaseGy-Gx+Gx=y
25 10 12 19 24 syl3anc GTopGrpxBaseGyBaseGwJxwywzJyzy-Gx+Gx=y
26 simprr GTopGrpxBaseGyBaseGwJxwywzJyzyz
27 25 26 eqeltrd GTopGrpxBaseGyBaseGwJxwywzJyzy-Gx+Gxz
28 oveq2 a=xy-Ga=y-Gx
29 28 oveq1d a=xy-Ga+Gx=y-Gx+Gx
30 29 eleq1d a=xy-Ga+Gxzy-Gx+Gxz
31 eqid aBaseGy-Ga+Gx=aBaseGy-Ga+Gx
32 31 mptpreima aBaseGy-Ga+Gx-1z=aBaseG|y-Ga+Gxz
33 30 32 elrab2 xaBaseGy-Ga+Gx-1zxBaseGy-Gx+Gxz
34 19 27 33 sylanbrc GTopGrpxBaseGyBaseGwJxwywzJyzxaBaseGy-Ga+Gx-1z
35 eleq2 w=aBaseGy-Ga+Gx-1zxwxaBaseGy-Ga+Gx-1z
36 eleq2 w=aBaseGy-Ga+Gx-1zywyaBaseGy-Ga+Gx-1z
37 35 36 imbi12d w=aBaseGy-Ga+Gx-1zxwywxaBaseGy-Ga+Gx-1zyaBaseGy-Ga+Gx-1z
38 simplr GTopGrpxBaseGyBaseGwJxwywzJyzwJxwyw
39 tgptmd GTopGrpGTopMnd
40 39 ad3antrrr GTopGrpxBaseGyBaseGwJxwywzJyzGTopMnd
41 1 13 tgptopon GTopGrpJTopOnBaseG
42 41 ad3antrrr GTopGrpxBaseGyBaseGwJxwywzJyzJTopOnBaseG
43 42 42 12 cnmptc GTopGrpxBaseGyBaseGwJxwywzJyzaBaseGyJCnJ
44 42 cnmptid GTopGrpxBaseGyBaseGwJxwywzJyzaBaseGaJCnJ
45 1 15 tgpsubcn GTopGrp-GJ×tJCnJ
46 45 ad3antrrr GTopGrpxBaseGyBaseGwJxwywzJyz-GJ×tJCnJ
47 42 43 44 46 cnmpt12f GTopGrpxBaseGyBaseGwJxwywzJyzaBaseGy-GaJCnJ
48 42 42 19 cnmptc GTopGrpxBaseGyBaseGwJxwywzJyzaBaseGxJCnJ
49 1 20 40 42 47 48 cnmpt1plusg GTopGrpxBaseGyBaseGwJxwywzJyzaBaseGy-Ga+GxJCnJ
50 simprl GTopGrpxBaseGyBaseGwJxwywzJyzzJ
51 cnima aBaseGy-Ga+GxJCnJzJaBaseGy-Ga+Gx-1zJ
52 49 50 51 syl2anc GTopGrpxBaseGyBaseGwJxwywzJyzaBaseGy-Ga+Gx-1zJ
53 37 38 52 rspcdva GTopGrpxBaseGyBaseGwJxwywzJyzxaBaseGy-Ga+Gx-1zyaBaseGy-Ga+Gx-1z
54 34 53 mpd GTopGrpxBaseGyBaseGwJxwywzJyzyaBaseGy-Ga+Gx-1z
55 oveq2 a=yy-Ga=y-Gy
56 55 oveq1d a=yy-Ga+Gx=y-Gy+Gx
57 56 eleq1d a=yy-Ga+Gxzy-Gy+Gxz
58 57 32 elrab2 yaBaseGy-Ga+Gx-1zyBaseGy-Gy+Gxz
59 58 simprbi yaBaseGy-Ga+Gx-1zy-Gy+Gxz
60 54 59 syl GTopGrpxBaseGyBaseGwJxwywzJyzy-Gy+Gxz
61 23 60 eqeltrrd GTopGrpxBaseGyBaseGwJxwywzJyzxz
62 61 expr GTopGrpxBaseGyBaseGwJxwywzJyzxz
63 8 62 impbid GTopGrpxBaseGyBaseGwJxwywzJxzyz
64 63 ralrimiva GTopGrpxBaseGyBaseGwJxwywzJxzyz
65 64 ex GTopGrpxBaseGyBaseGwJxwywzJxzyz
66 65 imim1d GTopGrpxBaseGyBaseGzJxzyzx=ywJxwywx=y
67 66 ralimdvva GTopGrpxBaseGyBaseGzJxzyzx=yxBaseGyBaseGwJxwywx=y
68 ist0-2 JTopOnBaseGJKol2xBaseGyBaseGzJxzyzx=y
69 41 68 syl GTopGrpJKol2xBaseGyBaseGzJxzyzx=y
70 ist1-2 JTopOnBaseGJFrexBaseGyBaseGwJxwywx=y
71 41 70 syl GTopGrpJFrexBaseGyBaseGwJxwywx=y
72 67 69 71 3imtr4d GTopGrpJKol2JFre
73 3 72 impbid2 GTopGrpJFreJKol2
74 2 73 bitrd GTopGrpJHausJKol2