Metamath Proof Explorer


Theorem tlmtgp

Description: A topological vector space is a topological group. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion tlmtgp WTopModWTopGrp

Proof

Step Hyp Ref Expression
1 tlmlmod WTopModWLMod
2 lmodgrp WLModWGrp
3 1 2 syl WTopModWGrp
4 tlmtmd WTopModWTopMnd
5 eqid BaseW=BaseW
6 eqid invgW=invgW
7 5 6 grpinvf WGrpinvgW:BaseWBaseW
8 3 7 syl WTopModinvgW:BaseWBaseW
9 8 feqmptd WTopModinvgW=xBaseWinvgWx
10 eqid ScalarW=ScalarW
11 eqid W=W
12 eqid 1ScalarW=1ScalarW
13 eqid invgScalarW=invgScalarW
14 5 6 10 11 12 13 lmodvneg1 WLModxBaseWinvgScalarW1ScalarWWx=invgWx
15 1 14 sylan WTopModxBaseWinvgScalarW1ScalarWWx=invgWx
16 15 mpteq2dva WTopModxBaseWinvgScalarW1ScalarWWx=xBaseWinvgWx
17 9 16 eqtr4d WTopModinvgW=xBaseWinvgScalarW1ScalarWWx
18 eqid TopOpenW=TopOpenW
19 eqid TopOpenScalarW=TopOpenScalarW
20 id WTopModWTopMod
21 tlmtps WTopModWTopSp
22 5 18 istps WTopSpTopOpenWTopOnBaseW
23 21 22 sylib WTopModTopOpenWTopOnBaseW
24 10 tlmscatps WTopModScalarWTopSp
25 eqid BaseScalarW=BaseScalarW
26 25 19 istps ScalarWTopSpTopOpenScalarWTopOnBaseScalarW
27 24 26 sylib WTopModTopOpenScalarWTopOnBaseScalarW
28 10 lmodring WLModScalarWRing
29 1 28 syl WTopModScalarWRing
30 ringgrp ScalarWRingScalarWGrp
31 29 30 syl WTopModScalarWGrp
32 25 12 ringidcl ScalarWRing1ScalarWBaseScalarW
33 29 32 syl WTopMod1ScalarWBaseScalarW
34 25 13 grpinvcl ScalarWGrp1ScalarWBaseScalarWinvgScalarW1ScalarWBaseScalarW
35 31 33 34 syl2anc WTopModinvgScalarW1ScalarWBaseScalarW
36 23 27 35 cnmptc WTopModxBaseWinvgScalarW1ScalarWTopOpenWCnTopOpenScalarW
37 23 cnmptid WTopModxBaseWxTopOpenWCnTopOpenW
38 10 11 18 19 20 23 36 37 cnmpt1vsca WTopModxBaseWinvgScalarW1ScalarWWxTopOpenWCnTopOpenW
39 17 38 eqeltrd WTopModinvgWTopOpenWCnTopOpenW
40 18 6 istgp WTopGrpWGrpWTopMndinvgWTopOpenWCnTopOpenW
41 3 4 39 40 syl3anbrc WTopModWTopGrp