Description: A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | tlmtgp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tlmlmod | |
|
2 | lmodgrp | |
|
3 | 1 2 | syl | |
4 | tlmtmd | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | 5 6 | grpinvf | |
8 | 3 7 | syl | |
9 | 8 | feqmptd | |
10 | eqid | |
|
11 | eqid | |
|
12 | eqid | |
|
13 | eqid | |
|
14 | 5 6 10 11 12 13 | lmodvneg1 | |
15 | 1 14 | sylan | |
16 | 15 | mpteq2dva | |
17 | 9 16 | eqtr4d | |
18 | eqid | |
|
19 | eqid | |
|
20 | id | |
|
21 | tlmtps | |
|
22 | 5 18 | istps | |
23 | 21 22 | sylib | |
24 | 10 | tlmscatps | |
25 | eqid | |
|
26 | 25 19 | istps | |
27 | 24 26 | sylib | |
28 | 10 | lmodring | |
29 | 1 28 | syl | |
30 | ringgrp | |
|
31 | 29 30 | syl | |
32 | 25 12 | ringidcl | |
33 | 29 32 | syl | |
34 | 25 13 | grpinvcl | |
35 | 31 33 34 | syl2anc | |
36 | 23 27 35 | cnmptc | |
37 | 23 | cnmptid | |
38 | 10 11 18 19 20 23 36 37 | cnmpt1vsca | |
39 | 17 38 | eqeltrd | |
40 | 18 6 | istgp | |
41 | 3 4 39 40 | syl3anbrc | |