Step |
Hyp |
Ref |
Expression |
1 |
|
lss0v.x |
|- X = ( W |`s U ) |
2 |
|
lss0v.o |
|- .0. = ( 0g ` W ) |
3 |
|
lss0v.z |
|- Z = ( 0g ` X ) |
4 |
|
lss0v.l |
|- L = ( LSubSp ` W ) |
5 |
|
0ss |
|- (/) C_ U |
6 |
|
eqid |
|- ( LSpan ` W ) = ( LSpan ` W ) |
7 |
|
eqid |
|- ( LSpan ` X ) = ( LSpan ` X ) |
8 |
1 6 7 4
|
lsslsp |
|- ( ( W e. LMod /\ U e. L /\ (/) C_ U ) -> ( ( LSpan ` W ) ` (/) ) = ( ( LSpan ` X ) ` (/) ) ) |
9 |
5 8
|
mp3an3 |
|- ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` W ) ` (/) ) = ( ( LSpan ` X ) ` (/) ) ) |
10 |
2 6
|
lsp0 |
|- ( W e. LMod -> ( ( LSpan ` W ) ` (/) ) = { .0. } ) |
11 |
10
|
adantr |
|- ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` W ) ` (/) ) = { .0. } ) |
12 |
1 4
|
lsslmod |
|- ( ( W e. LMod /\ U e. L ) -> X e. LMod ) |
13 |
3 7
|
lsp0 |
|- ( X e. LMod -> ( ( LSpan ` X ) ` (/) ) = { Z } ) |
14 |
12 13
|
syl |
|- ( ( W e. LMod /\ U e. L ) -> ( ( LSpan ` X ) ` (/) ) = { Z } ) |
15 |
9 11 14
|
3eqtr3rd |
|- ( ( W e. LMod /\ U e. L ) -> { Z } = { .0. } ) |
16 |
15
|
unieqd |
|- ( ( W e. LMod /\ U e. L ) -> U. { Z } = U. { .0. } ) |
17 |
3
|
fvexi |
|- Z e. _V |
18 |
17
|
unisn |
|- U. { Z } = Z |
19 |
2
|
fvexi |
|- .0. e. _V |
20 |
19
|
unisn |
|- U. { .0. } = .0. |
21 |
16 18 20
|
3eqtr3g |
|- ( ( W e. LMod /\ U e. L ) -> Z = .0. ) |