Step |
Hyp |
Ref |
Expression |
1 |
|
lspdisj.v |
|- V = ( Base ` W ) |
2 |
|
lspdisj.o |
|- .0. = ( 0g ` W ) |
3 |
|
lspdisj.n |
|- N = ( LSpan ` W ) |
4 |
|
lspdisj.s |
|- S = ( LSubSp ` W ) |
5 |
|
lspdisj.w |
|- ( ph -> W e. LVec ) |
6 |
|
lspdisj.u |
|- ( ph -> U e. S ) |
7 |
|
lspdisj.x |
|- ( ph -> X e. V ) |
8 |
|
lspdisj.e |
|- ( ph -> -. X e. U ) |
9 |
|
lveclmod |
|- ( W e. LVec -> W e. LMod ) |
10 |
5 9
|
syl |
|- ( ph -> W e. LMod ) |
11 |
|
eqid |
|- ( Scalar ` W ) = ( Scalar ` W ) |
12 |
|
eqid |
|- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
13 |
|
eqid |
|- ( .s ` W ) = ( .s ` W ) |
14 |
11 12 1 13 3
|
lspsnel |
|- ( ( W e. LMod /\ X e. V ) -> ( v e. ( N ` { X } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) ) ) |
15 |
10 7 14
|
syl2anc |
|- ( ph -> ( v e. ( N ` { X } ) <-> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) ) ) |
16 |
15
|
biimpa |
|- ( ( ph /\ v e. ( N ` { X } ) ) -> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) ) |
17 |
16
|
adantrr |
|- ( ( ph /\ ( v e. ( N ` { X } ) /\ v e. U ) ) -> E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) ) |
18 |
|
simprr |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> v = ( k ( .s ` W ) X ) ) |
19 |
8
|
ad2antrr |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> -. X e. U ) |
20 |
|
simplr |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> v e. U ) |
21 |
18 20
|
eqeltrrd |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( k ( .s ` W ) X ) e. U ) |
22 |
|
eqid |
|- ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) ) |
23 |
5
|
ad2antrr |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> W e. LVec ) |
24 |
6
|
ad2antrr |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> U e. S ) |
25 |
7
|
ad2antrr |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> X e. V ) |
26 |
|
simprl |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> k e. ( Base ` ( Scalar ` W ) ) ) |
27 |
1 13 11 12 22 4 23 24 25 26
|
lssvs0or |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( ( k ( .s ` W ) X ) e. U <-> ( k = ( 0g ` ( Scalar ` W ) ) \/ X e. U ) ) ) |
28 |
21 27
|
mpbid |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( k = ( 0g ` ( Scalar ` W ) ) \/ X e. U ) ) |
29 |
28
|
orcomd |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( X e. U \/ k = ( 0g ` ( Scalar ` W ) ) ) ) |
30 |
29
|
ord |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( -. X e. U -> k = ( 0g ` ( Scalar ` W ) ) ) ) |
31 |
19 30
|
mpd |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> k = ( 0g ` ( Scalar ` W ) ) ) |
32 |
31
|
oveq1d |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( k ( .s ` W ) X ) = ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) ) |
33 |
10
|
ad2antrr |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> W e. LMod ) |
34 |
1 11 13 22 2
|
lmod0vs |
|- ( ( W e. LMod /\ X e. V ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) = .0. ) |
35 |
33 25 34
|
syl2anc |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> ( ( 0g ` ( Scalar ` W ) ) ( .s ` W ) X ) = .0. ) |
36 |
18 32 35
|
3eqtrd |
|- ( ( ( ph /\ v e. U ) /\ ( k e. ( Base ` ( Scalar ` W ) ) /\ v = ( k ( .s ` W ) X ) ) ) -> v = .0. ) |
37 |
36
|
exp32 |
|- ( ( ph /\ v e. U ) -> ( k e. ( Base ` ( Scalar ` W ) ) -> ( v = ( k ( .s ` W ) X ) -> v = .0. ) ) ) |
38 |
37
|
adantrl |
|- ( ( ph /\ ( v e. ( N ` { X } ) /\ v e. U ) ) -> ( k e. ( Base ` ( Scalar ` W ) ) -> ( v = ( k ( .s ` W ) X ) -> v = .0. ) ) ) |
39 |
38
|
rexlimdv |
|- ( ( ph /\ ( v e. ( N ` { X } ) /\ v e. U ) ) -> ( E. k e. ( Base ` ( Scalar ` W ) ) v = ( k ( .s ` W ) X ) -> v = .0. ) ) |
40 |
17 39
|
mpd |
|- ( ( ph /\ ( v e. ( N ` { X } ) /\ v e. U ) ) -> v = .0. ) |
41 |
40
|
ex |
|- ( ph -> ( ( v e. ( N ` { X } ) /\ v e. U ) -> v = .0. ) ) |
42 |
|
elin |
|- ( v e. ( ( N ` { X } ) i^i U ) <-> ( v e. ( N ` { X } ) /\ v e. U ) ) |
43 |
|
velsn |
|- ( v e. { .0. } <-> v = .0. ) |
44 |
41 42 43
|
3imtr4g |
|- ( ph -> ( v e. ( ( N ` { X } ) i^i U ) -> v e. { .0. } ) ) |
45 |
44
|
ssrdv |
|- ( ph -> ( ( N ` { X } ) i^i U ) C_ { .0. } ) |
46 |
1 4 3
|
lspsncl |
|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. S ) |
47 |
10 7 46
|
syl2anc |
|- ( ph -> ( N ` { X } ) e. S ) |
48 |
2 4
|
lss0ss |
|- ( ( W e. LMod /\ ( N ` { X } ) e. S ) -> { .0. } C_ ( N ` { X } ) ) |
49 |
10 47 48
|
syl2anc |
|- ( ph -> { .0. } C_ ( N ` { X } ) ) |
50 |
2 4
|
lss0ss |
|- ( ( W e. LMod /\ U e. S ) -> { .0. } C_ U ) |
51 |
10 6 50
|
syl2anc |
|- ( ph -> { .0. } C_ U ) |
52 |
49 51
|
ssind |
|- ( ph -> { .0. } C_ ( ( N ` { X } ) i^i U ) ) |
53 |
45 52
|
eqssd |
|- ( ph -> ( ( N ` { X } ) i^i U ) = { .0. } ) |