Metamath Proof Explorer


Theorem tgpsubcn

Description: In a topological group, the "subtraction" (or "division") is continuous. Axiom GT' of BourbakiTop1 p. III.1. (Contributed by FL, 21-Jun-2010) (Revised by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypotheses tgpsubcn.2 J=TopOpenG
tgpsubcn.3 -˙=-G
Assertion tgpsubcn GTopGrp-˙J×tJCnJ

Proof

Step Hyp Ref Expression
1 tgpsubcn.2 J=TopOpenG
2 tgpsubcn.3 -˙=-G
3 eqid BaseG=BaseG
4 eqid +G=+G
5 eqid invgG=invgG
6 3 4 5 2 grpsubfval -˙=xBaseG,yBaseGx+GinvgGy
7 tgptmd GTopGrpGTopMnd
8 1 3 tgptopon GTopGrpJTopOnBaseG
9 8 8 cnmpt1st GTopGrpxBaseG,yBaseGxJ×tJCnJ
10 8 8 cnmpt2nd GTopGrpxBaseG,yBaseGyJ×tJCnJ
11 1 5 tgpinv GTopGrpinvgGJCnJ
12 8 8 10 11 cnmpt21f GTopGrpxBaseG,yBaseGinvgGyJ×tJCnJ
13 1 4 7 8 8 9 12 cnmpt2plusg GTopGrpxBaseG,yBaseGx+GinvgGyJ×tJCnJ
14 6 13 eqeltrid GTopGrp-˙J×tJCnJ