| Step |
Hyp |
Ref |
Expression |
| 1 |
|
tlmlmod |
⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ LMod ) |
| 2 |
|
lmodgrp |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp ) |
| 3 |
1 2
|
syl |
⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ Grp ) |
| 4 |
|
tlmtmd |
⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ TopMnd ) |
| 5 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
| 6 |
|
eqid |
⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 ) |
| 7 |
5 6
|
grpinvf |
⊢ ( 𝑊 ∈ Grp → ( invg ‘ 𝑊 ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ) |
| 8 |
3 7
|
syl |
⊢ ( 𝑊 ∈ TopMod → ( invg ‘ 𝑊 ) : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑊 ) ) |
| 9 |
8
|
feqmptd |
⊢ ( 𝑊 ∈ TopMod → ( invg ‘ 𝑊 ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ) ) |
| 10 |
|
eqid |
⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 ) |
| 11 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 ) |
| 12 |
|
eqid |
⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) |
| 13 |
|
eqid |
⊢ ( invg ‘ ( Scalar ‘ 𝑊 ) ) = ( invg ‘ ( Scalar ‘ 𝑊 ) ) |
| 14 |
5 6 10 11 12 13
|
lmodvneg1 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ) |
| 15 |
1 14
|
sylan |
⊢ ( ( 𝑊 ∈ TopMod ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑥 ) = ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ) |
| 16 |
15
|
mpteq2dva |
⊢ ( 𝑊 ∈ TopMod → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ( invg ‘ 𝑊 ) ‘ 𝑥 ) ) ) |
| 17 |
9 16
|
eqtr4d |
⊢ ( 𝑊 ∈ TopMod → ( invg ‘ 𝑊 ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ) |
| 18 |
|
eqid |
⊢ ( TopOpen ‘ 𝑊 ) = ( TopOpen ‘ 𝑊 ) |
| 19 |
|
eqid |
⊢ ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) = ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) |
| 20 |
|
id |
⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ TopMod ) |
| 21 |
|
tlmtps |
⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ TopSp ) |
| 22 |
5 18
|
istps |
⊢ ( 𝑊 ∈ TopSp ↔ ( TopOpen ‘ 𝑊 ) ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ) |
| 23 |
21 22
|
sylib |
⊢ ( 𝑊 ∈ TopMod → ( TopOpen ‘ 𝑊 ) ∈ ( TopOn ‘ ( Base ‘ 𝑊 ) ) ) |
| 24 |
10
|
tlmscatps |
⊢ ( 𝑊 ∈ TopMod → ( Scalar ‘ 𝑊 ) ∈ TopSp ) |
| 25 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) |
| 26 |
25 19
|
istps |
⊢ ( ( Scalar ‘ 𝑊 ) ∈ TopSp ↔ ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( TopOn ‘ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
| 27 |
24 26
|
sylib |
⊢ ( 𝑊 ∈ TopMod → ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( TopOn ‘ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
| 28 |
10
|
lmodring |
⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Ring ) |
| 29 |
1 28
|
syl |
⊢ ( 𝑊 ∈ TopMod → ( Scalar ‘ 𝑊 ) ∈ Ring ) |
| 30 |
|
ringgrp |
⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( Scalar ‘ 𝑊 ) ∈ Grp ) |
| 31 |
29 30
|
syl |
⊢ ( 𝑊 ∈ TopMod → ( Scalar ‘ 𝑊 ) ∈ Grp ) |
| 32 |
25 12
|
ringidcl |
⊢ ( ( Scalar ‘ 𝑊 ) ∈ Ring → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) |
| 33 |
29 32
|
syl |
⊢ ( 𝑊 ∈ TopMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) |
| 34 |
25 13
|
grpinvcl |
⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) |
| 35 |
31 33 34
|
syl2anc |
⊢ ( 𝑊 ∈ TopMod → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) |
| 36 |
23 27 35
|
cnmptc |
⊢ ( 𝑊 ∈ TopMod → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ) ∈ ( ( TopOpen ‘ 𝑊 ) Cn ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) ) ) |
| 37 |
23
|
cnmptid |
⊢ ( 𝑊 ∈ TopMod → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ 𝑥 ) ∈ ( ( TopOpen ‘ 𝑊 ) Cn ( TopOpen ‘ 𝑊 ) ) ) |
| 38 |
10 11 18 19 20 23 36 37
|
cnmpt1vsca |
⊢ ( 𝑊 ∈ TopMod → ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑥 ) ) ∈ ( ( TopOpen ‘ 𝑊 ) Cn ( TopOpen ‘ 𝑊 ) ) ) |
| 39 |
17 38
|
eqeltrd |
⊢ ( 𝑊 ∈ TopMod → ( invg ‘ 𝑊 ) ∈ ( ( TopOpen ‘ 𝑊 ) Cn ( TopOpen ‘ 𝑊 ) ) ) |
| 40 |
18 6
|
istgp |
⊢ ( 𝑊 ∈ TopGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ TopMnd ∧ ( invg ‘ 𝑊 ) ∈ ( ( TopOpen ‘ 𝑊 ) Cn ( TopOpen ‘ 𝑊 ) ) ) ) |
| 41 |
3 4 39 40
|
syl3anbrc |
⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ TopGrp ) |