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

Metamath Proof Explorer

Theorem dochval2

Description: Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Apr-2014)

Ref Expression
Hypotheses dochval2.o 
|- ._|_ = ( oc ` K )
dochval2.h 
|- H = ( LHyp ` K )
dochval2.i 
|- I = ( ( DIsoH ` K ) ` W )
dochval2.u 
|- U = ( ( DVecH ` K ) ` W )
dochval2.v 
|- V = ( Base ` U )
dochval2.n 
|- N = ( ( ocH ` K ) ` W )
Assertion dochval2 
|- ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( I ` ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) )

Proof

Step Hyp Ref Expression
1 dochval2.o 
 |-  ._|_ = ( oc ` K )
2 dochval2.h 
 |-  H = ( LHyp ` K )
3 dochval2.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dochval2.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dochval2.v 
 |-  V = ( Base ` U )
6 dochval2.n 
 |-  N = ( ( ocH ` K ) ` W )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 eqid 
 |-  ( glb ` K ) = ( glb ` K )
9 7 8 1 2 3 4 5 6 dochval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( I ` ( ._|_ ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) )
10 hlclat 
 |-  ( K e. HL -> K e. CLat )
11 10 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> K e. CLat )
12 ssrab2 
 |-  { x e. ( Base ` K ) | X C_ ( I ` x ) } C_ ( Base ` K )
13 7 8 clatglbcl 
 |-  ( ( K e. CLat /\ { x e. ( Base ` K ) | X C_ ( I ` x ) } C_ ( Base ` K ) ) -> ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) e. ( Base ` K ) )
14 11 12 13 sylancl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) e. ( Base ` K ) )
15 7 2 3 dihcnvid1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) e. ( Base ` K ) ) -> ( `' I ` ( I ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) = ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) )
16 14 15 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( `' I ` ( I ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) = ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) )
17 7 8 2 3 4 5 dihglb2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( I ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) = |^| { z e. ran I | X C_ z } )
18 17 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( `' I ` ( I ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) = ( `' I ` |^| { z e. ran I | X C_ z } ) )
19 16 18 eqtr3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) = ( `' I ` |^| { z e. ran I | X C_ z } ) )
20 19 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) = ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) )
21 20 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( I ` ( ._|_ ` ( ( glb ` K ) ` { x e. ( Base ` K ) | X C_ ( I ` x ) } ) ) ) = ( I ` ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) )
22 9 21 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( I ` ( ._|_ ` ( `' I ` |^| { z e. ran I | X C_ z } ) ) ) )