Metamath Proof Explorer

Theorem doch0

Description: Orthocomplement of the zero subspace. (Contributed by NM, 19-Jun-2014)

Ref Expression
Hypotheses doch0.h 
|- H = ( LHyp ` K )
doch0.u 
|- U = ( ( DVecH ` K ) ` W )
doch0.o 
|- ._|_ = ( ( ocH ` K ) ` W )
doch0.v 
|- V = ( Base ` U )
doch0.z 
|- .0. = ( 0g ` U )
Assertion doch0 
|- ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { .0. } ) = V )

Proof

Step Hyp Ref Expression
1 doch0.h 
 |-  H = ( LHyp ` K )
2 doch0.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 doch0.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
4 doch0.v 
 |-  V = ( Base ` U )
5 doch0.z 
 |-  .0. = ( 0g ` U )
6 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
7 1 6 2 5 dih0rn 
 |-  ( ( K e. HL /\ W e. H ) -> { .0. } e. ran ( ( DIsoH ` K ) ` W ) )
8 eqid 
 |-  ( oc ` K ) = ( oc ` K )
9 8 1 6 3 dochvalr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { .0. } e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` { .0. } ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` { .0. } ) ) ) )
10 7 9 mpdan 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { .0. } ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` { .0. } ) ) ) )
11 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
12 1 11 6 2 5 dih0cnv 
 |-  ( ( K e. HL /\ W e. H ) -> ( `' ( ( DIsoH ` K ) ` W ) ` { .0. } ) = ( 0. ` K ) )
13 12 fveq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` { .0. } ) ) = ( ( oc ` K ) ` ( 0. ` K ) ) )
14 hlop 
 |-  ( K e. HL -> K e. OP )
15 14 adantr 
 |-  ( ( K e. HL /\ W e. H ) -> K e. OP )
16 eqid 
 |-  ( 1. ` K ) = ( 1. ` K )
17 11 16 8 opoc0 
 |-  ( K e. OP -> ( ( oc ` K ) ` ( 0. ` K ) ) = ( 1. ` K ) )
18 15 17 syl 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( oc ` K ) ` ( 0. ` K ) ) = ( 1. ` K ) )
19 13 18 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` { .0. } ) ) = ( 1. ` K ) )
20 19 fveq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` { .0. } ) ) ) = ( ( ( DIsoH ` K ) ` W ) ` ( 1. ` K ) ) )
21 16 1 6 2 4 dih1 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoH ` K ) ` W ) ` ( 1. ` K ) ) = V )
22 20 21 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( `' ( ( DIsoH ` K ) ` W ) ` { .0. } ) ) ) = V )
23 10 22 eqtrd 
 |-  ( ( K e. HL /\ W e. H ) -> ( ._|_ ` { .0. } ) = V )