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 | |
|
tgpsubcn.3 | |
||
Assertion | tgpsubcn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgpsubcn.2 | |
|
2 | tgpsubcn.3 | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 3 4 5 2 | grpsubfval | |
7 | tgptmd | |
|
8 | 1 3 | tgptopon | |
9 | 8 8 | cnmpt1st | |
10 | 8 8 | cnmpt2nd | |
11 | 1 5 | tgpinv | |
12 | 8 8 10 11 | cnmpt21f | |
13 | 1 4 7 8 8 9 12 | cnmpt2plusg | |
14 | 6 13 | eqeltrid | |