Step |
Hyp |
Ref |
Expression |
1 |
|
nvcnlm |
|- ( W e. NrmVec -> W e. NrmMod ) |
2 |
|
nlmtlm |
|- ( W e. NrmMod -> W e. TopMod ) |
3 |
1 2
|
syl |
|- ( W e. NrmVec -> W e. TopMod ) |
4 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
5 |
4
|
nlmnrg |
|- ( W e. NrmMod -> ( Scalar ` W ) e. NrmRing ) |
6 |
1 5
|
syl |
|- ( W e. NrmVec -> ( Scalar ` W ) e. NrmRing ) |
7 |
|
nvclvec |
|- ( W e. NrmVec -> W e. LVec ) |
8 |
4
|
lvecdrng |
|- ( W e. LVec -> ( Scalar ` W ) e. DivRing ) |
9 |
7 8
|
syl |
|- ( W e. NrmVec -> ( Scalar ` W ) e. DivRing ) |
10 |
|
nrgtdrg |
|- ( ( ( Scalar ` W ) e. NrmRing /\ ( Scalar ` W ) e. DivRing ) -> ( Scalar ` W ) e. TopDRing ) |
11 |
6 9 10
|
syl2anc |
|- ( W e. NrmVec -> ( Scalar ` W ) e. TopDRing ) |
12 |
4
|
istvc |
|- ( W e. TopVec <-> ( W e. TopMod /\ ( Scalar ` W ) e. TopDRing ) ) |
13 |
3 11 12
|
sylanbrc |
|- ( W e. NrmVec -> W e. TopVec ) |