Step |
Hyp |
Ref |
Expression |
1 |
|
dochnel.h |
|- H = ( LHyp ` K ) |
2 |
|
dochnel.o |
|- ._|_ = ( ( ocH ` K ) ` W ) |
3 |
|
dochnel.u |
|- U = ( ( DVecH ` K ) ` W ) |
4 |
|
dochnel.v |
|- V = ( Base ` U ) |
5 |
|
dochnel.z |
|- .0. = ( 0g ` U ) |
6 |
|
dochnel.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
7 |
|
dochnel.x |
|- ( ph -> X e. ( V \ { .0. } ) ) |
8 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
9 |
1 3 6
|
dvhlmod |
|- ( ph -> U e. LMod ) |
10 |
7
|
eldifad |
|- ( ph -> X e. V ) |
11 |
|
eqid |
|- ( LSpan ` U ) = ( LSpan ` U ) |
12 |
4 8 11
|
lspsncl |
|- ( ( U e. LMod /\ X e. V ) -> ( ( LSpan ` U ) ` { X } ) e. ( LSubSp ` U ) ) |
13 |
9 10 12
|
syl2anc |
|- ( ph -> ( ( LSpan ` U ) ` { X } ) e. ( LSubSp ` U ) ) |
14 |
4 11
|
lspsnid |
|- ( ( U e. LMod /\ X e. V ) -> X e. ( ( LSpan ` U ) ` { X } ) ) |
15 |
9 10 14
|
syl2anc |
|- ( ph -> X e. ( ( LSpan ` U ) ` { X } ) ) |
16 |
|
eldifsni |
|- ( X e. ( V \ { .0. } ) -> X =/= .0. ) |
17 |
7 16
|
syl |
|- ( ph -> X =/= .0. ) |
18 |
|
eldifsn |
|- ( X e. ( ( ( LSpan ` U ) ` { X } ) \ { .0. } ) <-> ( X e. ( ( LSpan ` U ) ` { X } ) /\ X =/= .0. ) ) |
19 |
15 17 18
|
sylanbrc |
|- ( ph -> X e. ( ( ( LSpan ` U ) ` { X } ) \ { .0. } ) ) |
20 |
1 3 8 5 2 6 13 19
|
dochnel2 |
|- ( ph -> -. X e. ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) ) |
21 |
10
|
snssd |
|- ( ph -> { X } C_ V ) |
22 |
1 3 2 4 11 6 21
|
dochocsp |
|- ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) = ( ._|_ ` { X } ) ) |
23 |
20 22
|
neleqtrd |
|- ( ph -> -. X e. ( ._|_ ` { X } ) ) |