Step |
Hyp |
Ref |
Expression |
1 |
|
dih0vb.h |
|- H = ( LHyp ` K ) |
2 |
|
dih0vb.o |
|- .0. = ( 0. ` K ) |
3 |
|
dih0vb.i |
|- I = ( ( DIsoH ` K ) ` W ) |
4 |
|
dih0vb.u |
|- U = ( ( DVecH ` K ) ` W ) |
5 |
|
dih0vb.v |
|- V = ( Base ` U ) |
6 |
|
dih0vb.z |
|- Z = ( 0g ` U ) |
7 |
|
dih0vb.n |
|- N = ( LSpan ` U ) |
8 |
|
dih0vb.k |
|- ( ph -> ( K e. HL /\ W e. H ) ) |
9 |
|
dih0vb.x |
|- ( ph -> X e. V ) |
10 |
2 1 3 4 6
|
dih0 |
|- ( ( K e. HL /\ W e. H ) -> ( I ` .0. ) = { Z } ) |
11 |
8 10
|
syl |
|- ( ph -> ( I ` .0. ) = { Z } ) |
12 |
11
|
eqeq2d |
|- ( ph -> ( ( N ` { X } ) = ( I ` .0. ) <-> ( N ` { X } ) = { Z } ) ) |
13 |
1 4 8
|
dvhlmod |
|- ( ph -> U e. LMod ) |
14 |
5 6 7
|
lspsneq0 |
|- ( ( U e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { Z } <-> X = Z ) ) |
15 |
13 9 14
|
syl2anc |
|- ( ph -> ( ( N ` { X } ) = { Z } <-> X = Z ) ) |
16 |
12 15
|
bitr2d |
|- ( ph -> ( X = Z <-> ( N ` { X } ) = ( I ` .0. ) ) ) |