Metamath Proof Explorer

Theorem dochfval

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 dochfval 
|- ( ( K e. X /\ W e. H ) -> N = ( x e. ~P V |-> ( 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 dochffval 
 |-  ( K e. X -> ( ocH ` K ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) )
10 9 fveq1d 
 |-  ( K e. X -> ( ( ocH ` K ) ` W ) = ( ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ` W ) )
11 8 10 syl5eq 
 |-  ( K e. X -> N = ( ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ` W ) )
12 fveq2 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = ( ( DVecH ` K ) ` W ) )
13 12 6 eqtr4di 
 |-  ( w = W -> ( ( DVecH ` K ) ` w ) = U )
14 13 fveq2d 
 |-  ( w = W -> ( Base ` ( ( DVecH ` K ) ` w ) ) = ( Base ` U ) )
15 14 7 eqtr4di 
 |-  ( w = W -> ( Base ` ( ( DVecH ` K ) ` w ) ) = V )
16 15 pweqd 
 |-  ( w = W -> ~P ( Base ` ( ( DVecH ` K ) ` w ) ) = ~P V )
17 fveq2 
 |-  ( w = W -> ( ( DIsoH ` K ) ` w ) = ( ( DIsoH ` K ) ` W ) )
18 17 5 eqtr4di 
 |-  ( w = W -> ( ( DIsoH ` K ) ` w ) = I )
19 18 fveq1d 
 |-  ( w = W -> ( ( ( DIsoH ` K ) ` w ) ` y ) = ( I ` y ) )
20 19 sseq2d 
 |-  ( w = W -> ( x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) <-> x C_ ( I ` y ) ) )
21 20 rabbidv 
 |-  ( w = W -> { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } = { y e. B | x C_ ( I ` y ) } )
22 21 fveq2d 
 |-  ( w = W -> ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) = ( G ` { y e. B | x C_ ( I ` y ) } ) )
23 22 fveq2d 
 |-  ( w = W -> ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) = ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) )
24 18 23 fveq12d 
 |-  ( w = W -> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) = ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) )
25 16 24 mpteq12dv 
 |-  ( w = W -> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) = ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) )
26 eqid 
 |-  ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) = ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) )
27 7 fvexi 
 |-  V e. _V
28 27 pwex 
 |-  ~P V e. _V
29 28 mptex 
 |-  ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) e. _V
30 25 26 29 fvmpt 
 |-  ( W e. H -> ( ( w e. H |-> ( x e. ~P ( Base ` ( ( DVecH ` K ) ` w ) ) |-> ( ( ( DIsoH ` K ) ` w ) ` ( ._|_ ` ( G ` { y e. B | x C_ ( ( ( DIsoH ` K ) ` w ) ` y ) } ) ) ) ) ) ` W ) = ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) )
31 11 30 sylan9eq 
 |-  ( ( K e. X /\ W e. H ) -> N = ( x e. ~P V |-> ( I ` ( ._|_ ` ( G ` { y e. B | x C_ ( I ` y ) } ) ) ) ) )