Step |
Hyp |
Ref |
Expression |
1 |
|
djhexmid.h |
|- H = ( LHyp ` K ) |
2 |
|
djhexmid.u |
|- U = ( ( DVecH ` K ) ` W ) |
3 |
|
djhexmid.v |
|- V = ( Base ` U ) |
4 |
|
djhexmid.o |
|- ._|_ = ( ( ocH ` K ) ` W ) |
5 |
|
djhexmid.j |
|- .\/ = ( ( joinH ` K ) ` W ) |
6 |
|
simpl |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( K e. HL /\ W e. H ) ) |
7 |
|
simpr |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> X C_ V ) |
8 |
1 2 3 4
|
dochssv |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) C_ V ) |
9 |
1 2 3 4 5
|
djhval |
|- ( ( ( K e. HL /\ W e. H ) /\ ( X C_ V /\ ( ._|_ ` X ) C_ V ) ) -> ( X .\/ ( ._|_ ` X ) ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) ) ) |
10 |
6 7 8 9
|
syl12anc |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( X .\/ ( ._|_ ` X ) ) = ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) ) ) |
11 |
|
eqid |
|- ( LSubSp ` U ) = ( LSubSp ` U ) |
12 |
1 2 3 11 4
|
dochlss |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) e. ( LSubSp ` U ) ) |
13 |
|
eqid |
|- ( 0g ` U ) = ( 0g ` U ) |
14 |
1 2 11 13 4
|
dochnoncon |
|- ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` X ) e. ( LSubSp ` U ) ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) = { ( 0g ` U ) } ) |
15 |
12 14
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) = { ( 0g ` U ) } ) |
16 |
1 2 4 3 13
|
doch1 |
|- ( ( K e. HL /\ W e. H ) -> ( ._|_ ` V ) = { ( 0g ` U ) } ) |
17 |
16
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` V ) = { ( 0g ` U ) } ) |
18 |
15 17
|
eqtr4d |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) = ( ._|_ ` V ) ) |
19 |
18
|
fveq2d |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` ( ._|_ ` X ) ) ) ) = ( ._|_ ` ( ._|_ ` V ) ) ) |
20 |
|
eqid |
|- ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W ) |
21 |
1 20 2 3
|
dih1rn |
|- ( ( K e. HL /\ W e. H ) -> V e. ran ( ( DIsoH ` K ) ` W ) ) |
22 |
21
|
adantr |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> V e. ran ( ( DIsoH ` K ) ` W ) ) |
23 |
1 20 4
|
dochoc |
|- ( ( ( K e. HL /\ W e. H ) /\ V e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` V ) ) = V ) |
24 |
22 23
|
syldan |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` ( ._|_ ` V ) ) = V ) |
25 |
10 19 24
|
3eqtrd |
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( X .\/ ( ._|_ ` X ) ) = V ) |