| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lsslvec.x |
|- X = ( W |`s U ) |
| 2 |
|
lsslvec.s |
|- S = ( LSubSp ` W ) |
| 3 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
| 4 |
1 2
|
lsslmod |
|- ( ( W e. LMod /\ U e. S ) -> X e. LMod ) |
| 5 |
3 4
|
sylan |
|- ( ( W e. LVec /\ U e. S ) -> X e. LMod ) |
| 6 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
| 7 |
1 6
|
resssca |
|- ( U e. S -> ( Scalar ` W ) = ( Scalar ` X ) ) |
| 8 |
7
|
adantl |
|- ( ( W e. LVec /\ U e. S ) -> ( Scalar ` W ) = ( Scalar ` X ) ) |
| 9 |
6
|
lvecdrng |
|- ( W e. LVec -> ( Scalar ` W ) e. DivRing ) |
| 10 |
9
|
adantr |
|- ( ( W e. LVec /\ U e. S ) -> ( Scalar ` W ) e. DivRing ) |
| 11 |
8 10
|
eqeltrrd |
|- ( ( W e. LVec /\ U e. S ) -> ( Scalar ` X ) e. DivRing ) |
| 12 |
|
eqid |
|- ( Scalar ` X ) = ( Scalar ` X ) |
| 13 |
12
|
islvec |
|- ( X e. LVec <-> ( X e. LMod /\ ( Scalar ` X ) e. DivRing ) ) |
| 14 |
5 11 13
|
sylanbrc |
|- ( ( W e. LVec /\ U e. S ) -> X e. LVec ) |