| Step |
Hyp |
Ref |
Expression |
| 1 |
|
dvh3dim.h |
|- H = ( LHyp ` K ) |
| 2 |
|
dvh3dim.u |
|- U = ( ( DVecH ` K ) ` W ) |
| 3 |
|
dvh3dim.v |
|- V = ( Base ` U ) |
| 4 |
|
dvh3dim.n |
|- N = ( LSpan ` U ) |
| 5 |
|
dvh3dim.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
| 6 |
|
dvh3dim.x |
|- ( ph -> X e. V ) |
| 7 |
|
dvhdim.y |
|- ( ph -> Y e. V ) |
| 8 |
|
dvhdim.o |
|- .0. = ( 0g ` U ) |
| 9 |
|
dvhdim.x |
|- ( ph -> X =/= .0. ) |
| 10 |
|
dvhdimlem.y |
|- ( ph -> Y =/= .0. ) |
| 11 |
1 2 3 4 5 6 7 7 8 9 10 10
|
dvh4dimlem |
|- ( ph -> E. z e. V -. z e. ( N ` { X , Y , Y } ) ) |
| 12 |
1 2 5
|
dvhlmod |
|- ( ph -> U e. LMod ) |
| 13 |
|
df-tp |
|- { X , Y , Y } = ( { X , Y } u. { Y } ) |
| 14 |
|
prssi |
|- ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V ) |
| 15 |
6 7 14
|
syl2anc |
|- ( ph -> { X , Y } C_ V ) |
| 16 |
7
|
snssd |
|- ( ph -> { Y } C_ V ) |
| 17 |
15 16
|
unssd |
|- ( ph -> ( { X , Y } u. { Y } ) C_ V ) |
| 18 |
13 17
|
eqsstrid |
|- ( ph -> { X , Y , Y } C_ V ) |
| 19 |
|
ssun1 |
|- { X , Y } C_ ( { X , Y } u. { Y } ) |
| 20 |
19 13
|
sseqtrri |
|- { X , Y } C_ { X , Y , Y } |
| 21 |
20
|
a1i |
|- ( ph -> { X , Y } C_ { X , Y , Y } ) |
| 22 |
3 4
|
lspss |
|- ( ( U e. LMod /\ { X , Y , Y } C_ V /\ { X , Y } C_ { X , Y , Y } ) -> ( N ` { X , Y } ) C_ ( N ` { X , Y , Y } ) ) |
| 23 |
12 18 21 22
|
syl3anc |
|- ( ph -> ( N ` { X , Y } ) C_ ( N ` { X , Y , Y } ) ) |
| 24 |
23
|
ssneld |
|- ( ph -> ( -. z e. ( N ` { X , Y , Y } ) -> -. z e. ( N ` { X , Y } ) ) ) |
| 25 |
24
|
reximdv |
|- ( ph -> ( E. z e. V -. z e. ( N ` { X , Y , Y } ) -> E. z e. V -. z e. ( N ` { X , Y } ) ) ) |
| 26 |
11 25
|
mpd |
|- ( ph -> E. z e. V -. z e. ( N ` { X , Y } ) ) |