Step |
Hyp |
Ref |
Expression |
1 |
|
lssssr.o |
|- .0. = ( 0g ` W ) |
2 |
|
lssssr.s |
|- S = ( LSubSp ` W ) |
3 |
|
lssssr.w |
|- ( ph -> W e. LMod ) |
4 |
|
lssssr.t |
|- ( ph -> T C_ V ) |
5 |
|
lssssr.u |
|- ( ph -> U e. S ) |
6 |
|
lssssr.1 |
|- ( ( ph /\ x e. ( V \ { .0. } ) ) -> ( x e. T -> x e. U ) ) |
7 |
|
simpr |
|- ( ( ph /\ x = .0. ) -> x = .0. ) |
8 |
1 2
|
lss0cl |
|- ( ( W e. LMod /\ U e. S ) -> .0. e. U ) |
9 |
3 5 8
|
syl2anc |
|- ( ph -> .0. e. U ) |
10 |
9
|
adantr |
|- ( ( ph /\ x = .0. ) -> .0. e. U ) |
11 |
7 10
|
eqeltrd |
|- ( ( ph /\ x = .0. ) -> x e. U ) |
12 |
11
|
a1d |
|- ( ( ph /\ x = .0. ) -> ( x e. T -> x e. U ) ) |
13 |
4
|
sseld |
|- ( ph -> ( x e. T -> x e. V ) ) |
14 |
13
|
ancrd |
|- ( ph -> ( x e. T -> ( x e. V /\ x e. T ) ) ) |
15 |
14
|
adantr |
|- ( ( ph /\ x =/= .0. ) -> ( x e. T -> ( x e. V /\ x e. T ) ) ) |
16 |
|
eldifsn |
|- ( x e. ( V \ { .0. } ) <-> ( x e. V /\ x =/= .0. ) ) |
17 |
16 6
|
sylan2br |
|- ( ( ph /\ ( x e. V /\ x =/= .0. ) ) -> ( x e. T -> x e. U ) ) |
18 |
17
|
exp32 |
|- ( ph -> ( x e. V -> ( x =/= .0. -> ( x e. T -> x e. U ) ) ) ) |
19 |
18
|
com23 |
|- ( ph -> ( x =/= .0. -> ( x e. V -> ( x e. T -> x e. U ) ) ) ) |
20 |
19
|
imp4b |
|- ( ( ph /\ x =/= .0. ) -> ( ( x e. V /\ x e. T ) -> x e. U ) ) |
21 |
15 20
|
syld |
|- ( ( ph /\ x =/= .0. ) -> ( x e. T -> x e. U ) ) |
22 |
12 21
|
pm2.61dane |
|- ( ph -> ( x e. T -> x e. U ) ) |
23 |
22
|
ssrdv |
|- ( ph -> T C_ U ) |