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 ) } ) ) ) )