Metamath Proof Explorer

Theorem dochval

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

Ref Expression
Hypotheses dochval.b 
|- B = ( Base ` K )
dochval.g 
|- G = ( glb ` K )
dochval.o 
|- ._|_ = ( oc ` K )
dochval.h 
|- H = ( LHyp ` K )
dochval.i 
|- I = ( ( DIsoH ` K ) ` W )
dochval.u 
|- U = ( ( DVecH ` K ) ` W )
dochval.v 
|- V = ( Base ` U )
dochval.n 
|- N = ( ( ocH ` K ) ` W )
Assertion dochval 
|- ( ( ( K e. Y /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( I ` ( ._|_ ` ( G ` { y e. B | X C_ ( I ` y ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 dochval.b 
 |-  B = ( Base ` K )
2 dochval.g 
 |-  G = ( glb ` K )
3 dochval.o 
 |-  ._|_ = ( oc ` K )
4 dochval.h 
 |-  H = ( LHyp ` K )
5 dochval.i 
 |-  I = ( ( DIsoH ` K ) ` W )
6 dochval.u 
 |-  U = ( ( DVecH ` K ) ` W )
7 dochval.v 
 |-  V = ( Base ` U )
8 dochval.n 
 |-  N = ( ( ocH ` K ) ` W )
9 1 2 3 4 5 6 7 8 dochfval 
 |-  ( ( K e. Y /\ W e. H ) -> N = ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) )
10 9 adantr 
 |-  ( ( ( K e. Y /\ W e. H ) /\ X C_ V ) -> N = ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) )
11 10 fveq1d 
 |-  ( ( ( K e. Y /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) ` X ) )
12 7 fvexi 
 |-  V e. _V
13 12 elpw2 
 |-  ( X e. ~P V <-> X C_ V )
14 13 biimpri 
 |-  ( X C_ V -> X e. ~P V )
15 14 adantl 
 |-  ( ( ( K e. Y /\ W e. H ) /\ X C_ V ) -> X e. ~P V )
16 fvex 
 |-  ( I ` ( ._|_ ` ( G ` { y e. B | X C_ ( I ` y ) } ) ) ) e. _V
17 sseq1 
 |-  ( x = X -> ( x C_ ( I ` y ) <-> X C_ ( I ` y ) ) )
18 17 rabbidv 
 |-  ( x = X -> { y e. B | x C_ ( I ` y ) } = { y e. B | X C_ ( I ` y ) } )
19 18 fveq2d 
 |-  ( x = X -> ( G ` { y e. B | x C_ ( I ` y ) } ) = ( G ` { y e. B | X C_ ( I ` y ) } ) )
20 19 fveq2d 
 |-  ( x = X -> ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) = ( ._|_ ` ( G ` { y e. B | X C_ ( I ` y ) } ) ) )
21 20 fveq2d 
 |-  ( x = X -> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) = ( I ` ( ._|_ ` ( G ` { y e. B | X C_ ( I ` y ) } ) ) ) )
22 eqid 
 |-  ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) = ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) )
23 21 22 fvmptg 
 |-  ( ( X e. ~P V /\ ( I ` ( ._|_ ` ( G ` { y e. B | X C_ ( I ` y ) } ) ) ) e. _V ) -> ( ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) ` X ) = ( I ` ( ._|_ ` ( G ` { y e. B | X C_ ( I ` y ) } ) ) ) )
24 15 16 23 sylancl 
 |-  ( ( ( K e. Y /\ W e. H ) /\ X C_ V ) -> ( ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) ` X ) = ( I ` ( ._|_ ` ( G ` { y e. B | X C_ ( I ` y ) } ) ) ) )
25 11 24 eqtrd 
 |-  ( ( ( K e. Y /\ W e. H ) /\ X C_ V ) -> ( N ` X ) = ( I ` ( ._|_ ` ( G ` { y e. B | X C_ ( I ` y ) } ) ) ) )