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=TopOpenG
tgpsubcn.3 -˙=-G
Assertion istgp2 GTopGrpGGrpGTopSp-˙J×tJCnJ

Proof

Step Hyp Ref Expression
1 tgpsubcn.2 J=TopOpenG
2 tgpsubcn.3 -˙=-G
3 tgpgrp GTopGrpGGrp
4 tgptps GTopGrpGTopSp
5 1 2 tgpsubcn GTopGrp-˙J×tJCnJ
6 3 4 5 3jca GTopGrpGGrpGTopSp-˙J×tJCnJ
7 simp1 GGrpGTopSp-˙J×tJCnJGGrp
8 grpmnd GGrpGMnd
9 8 3ad2ant1 GGrpGTopSp-˙J×tJCnJGMnd
10 simp2 GGrpGTopSp-˙J×tJCnJGTopSp
11 eqid BaseG=BaseG
12 eqid +G=+G
13 eqid invgG=invgG
14 7 3ad2ant1 GGrpGTopSp-˙J×tJCnJxBaseGyBaseGGGrp
15 simp2 GGrpGTopSp-˙J×tJCnJxBaseGyBaseGxBaseG
16 simp3 GGrpGTopSp-˙J×tJCnJxBaseGyBaseGyBaseG
17 11 12 2 13 14 15 16 grpsubinv GGrpGTopSp-˙J×tJCnJxBaseGyBaseGx-˙invgGy=x+Gy
18 17 mpoeq3dva GGrpGTopSp-˙J×tJCnJxBaseG,yBaseGx-˙invgGy=xBaseG,yBaseGx+Gy
19 eqid +𝑓G=+𝑓G
20 11 12 19 plusffval +𝑓G=xBaseG,yBaseGx+Gy
21 18 20 eqtr4di GGrpGTopSp-˙J×tJCnJxBaseG,yBaseGx-˙invgGy=+𝑓G
22 11 1 istps GTopSpJTopOnBaseG
23 10 22 sylib GGrpGTopSp-˙J×tJCnJJTopOnBaseG
24 23 23 cnmpt1st GGrpGTopSp-˙J×tJCnJxBaseG,yBaseGxJ×tJCnJ
25 23 23 cnmpt2nd GGrpGTopSp-˙J×tJCnJxBaseG,yBaseGyJ×tJCnJ
26 11 13 grpinvf GGrpinvgG:BaseGBaseG
27 26 3ad2ant1 GGrpGTopSp-˙J×tJCnJinvgG:BaseGBaseG
28 27 feqmptd GGrpGTopSp-˙J×tJCnJinvgG=xBaseGinvgGx
29 eqid 0G=0G
30 11 2 13 29 grpinvval2 GGrpxBaseGinvgGx=0G-˙x
31 7 30 sylan GGrpGTopSp-˙J×tJCnJxBaseGinvgGx=0G-˙x
32 31 mpteq2dva GGrpGTopSp-˙J×tJCnJxBaseGinvgGx=xBaseG0G-˙x
33 28 32 eqtrd GGrpGTopSp-˙J×tJCnJinvgG=xBaseG0G-˙x
34 11 29 grpidcl GGrp0GBaseG
35 34 3ad2ant1 GGrpGTopSp-˙J×tJCnJ0GBaseG
36 23 23 35 cnmptc GGrpGTopSp-˙J×tJCnJxBaseG0GJCnJ
37 23 cnmptid GGrpGTopSp-˙J×tJCnJxBaseGxJCnJ
38 simp3 GGrpGTopSp-˙J×tJCnJ-˙J×tJCnJ
39 23 36 37 38 cnmpt12f GGrpGTopSp-˙J×tJCnJxBaseG0G-˙xJCnJ
40 33 39 eqeltrd GGrpGTopSp-˙J×tJCnJinvgGJCnJ
41 23 23 25 40 cnmpt21f GGrpGTopSp-˙J×tJCnJxBaseG,yBaseGinvgGyJ×tJCnJ
42 23 23 24 41 38 cnmpt22f GGrpGTopSp-˙J×tJCnJxBaseG,yBaseGx-˙invgGyJ×tJCnJ
43 21 42 eqeltrrd GGrpGTopSp-˙J×tJCnJ+𝑓GJ×tJCnJ
44 19 1 istmd GTopMndGMndGTopSp+𝑓GJ×tJCnJ
45 9 10 43 44 syl3anbrc GGrpGTopSp-˙J×tJCnJGTopMnd
46 1 13 istgp GTopGrpGGrpGTopMndinvgGJCnJ
47 7 45 40 46 syl3anbrc GGrpGTopSp-˙J×tJCnJGTopGrp
48 6 47 impbii GTopGrpGGrpGTopSp-˙J×tJCnJ