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 | |
|
tgpsubcn.3 | |
||
Assertion | istgp2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgpsubcn.2 | |
|
2 | tgpsubcn.3 | |
|
3 | tgpgrp | |
|
4 | tgptps | |
|
5 | 1 2 | tgpsubcn | |
6 | 3 4 5 | 3jca | |
7 | simp1 | |
|
8 | grpmnd | |
|
9 | 8 | 3ad2ant1 | |
10 | simp2 | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | 7 | 3ad2ant1 | |
15 | simp2 | |
|
16 | simp3 | |
|
17 | 11 12 2 13 14 15 16 | grpsubinv | |
18 | 17 | mpoeq3dva | |
19 | eqid | |
|
20 | 11 12 19 | plusffval | |
21 | 18 20 | eqtr4di | |
22 | 11 1 | istps | |
23 | 10 22 | sylib | |
24 | 23 23 | cnmpt1st | |
25 | 23 23 | cnmpt2nd | |
26 | 11 13 | grpinvf | |
27 | 26 | 3ad2ant1 | |
28 | 27 | feqmptd | |
29 | eqid | |
|
30 | 11 2 13 29 | grpinvval2 | |
31 | 7 30 | sylan | |
32 | 31 | mpteq2dva | |
33 | 28 32 | eqtrd | |
34 | 11 29 | grpidcl | |
35 | 34 | 3ad2ant1 | |
36 | 23 23 35 | cnmptc | |
37 | 23 | cnmptid | |
38 | simp3 | |
|
39 | 23 36 37 38 | cnmpt12f | |
40 | 33 39 | eqeltrd | |
41 | 23 23 25 40 | cnmpt21f | |
42 | 23 23 24 41 38 | cnmpt22f | |
43 | 21 42 | eqeltrrd | |
44 | 19 1 | istmd | |
45 | 9 10 43 44 | syl3anbrc | |
46 | 1 13 | istgp | |
47 | 7 45 40 46 | syl3anbrc | |
48 | 6 47 | impbii | |