| Step |
Hyp |
Ref |
Expression |
| 1 |
|
lmodfopne.t |
|- .x. = ( .sf ` W ) |
| 2 |
|
lmodfopne.a |
|- .+ = ( +f ` W ) |
| 3 |
|
lmodfopne.v |
|- V = ( Base ` W ) |
| 4 |
|
lmodfopne.s |
|- S = ( Scalar ` W ) |
| 5 |
|
lmodfopne.k |
|- K = ( Base ` S ) |
| 6 |
|
lmodfopne.0 |
|- .0. = ( 0g ` S ) |
| 7 |
|
lmodfopne.1 |
|- .1. = ( 1r ` S ) |
| 8 |
1 2 3 4 5
|
lmodfopnelem1 |
|- ( ( W e. LMod /\ .+ = .x. ) -> V = K ) |
| 9 |
8
|
ex |
|- ( W e. LMod -> ( .+ = .x. -> V = K ) ) |
| 10 |
4 5 6
|
lmod0cl |
|- ( W e. LMod -> .0. e. K ) |
| 11 |
4 5 7
|
lmod1cl |
|- ( W e. LMod -> .1. e. K ) |
| 12 |
10 11
|
jca |
|- ( W e. LMod -> ( .0. e. K /\ .1. e. K ) ) |
| 13 |
|
eleq2 |
|- ( V = K -> ( .0. e. V <-> .0. e. K ) ) |
| 14 |
|
eleq2 |
|- ( V = K -> ( .1. e. V <-> .1. e. K ) ) |
| 15 |
13 14
|
anbi12d |
|- ( V = K -> ( ( .0. e. V /\ .1. e. V ) <-> ( .0. e. K /\ .1. e. K ) ) ) |
| 16 |
12 15
|
syl5ibrcom |
|- ( W e. LMod -> ( V = K -> ( .0. e. V /\ .1. e. V ) ) ) |
| 17 |
9 16
|
syld |
|- ( W e. LMod -> ( .+ = .x. -> ( .0. e. V /\ .1. e. V ) ) ) |
| 18 |
17
|
imp |
|- ( ( W e. LMod /\ .+ = .x. ) -> ( .0. e. V /\ .1. e. V ) ) |