This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem doch1

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

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

Proof

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