Metamath Proof Explorer

Theorem ocvfval

Description: The orthocomplement operation. (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 13-Oct-2015)

Ref Expression
Hypotheses ocvfval.v 
|- V = ( Base ` W )
ocvfval.i 
|- ., = ( .i ` W )
ocvfval.f 
|- F = ( Scalar ` W )
ocvfval.z 
|- .0. = ( 0g ` F )
ocvfval.o 
|- ._|_ = ( ocv ` W )
Assertion ocvfval 
|- ( W e. X -> ._|_ = ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) )

Proof

Step Hyp Ref Expression
1 ocvfval.v 
 |-  V = ( Base ` W )
2 ocvfval.i 
 |-  ., = ( .i ` W )
3 ocvfval.f 
 |-  F = ( Scalar ` W )
4 ocvfval.z 
 |-  .0. = ( 0g ` F )
5 ocvfval.o 
 |-  ._|_ = ( ocv ` W )
6 elex 
 |-  ( W e. X -> W e. _V )
7 fveq2 
 |-  ( h = W -> ( Base ` h ) = ( Base ` W ) )
8 7 1 eqtr4di 
 |-  ( h = W -> ( Base ` h ) = V )
9 8 pweqd 
 |-  ( h = W -> ~P ( Base ` h ) = ~P V )
10 fveq2 
 |-  ( h = W -> ( .i ` h ) = ( .i ` W ) )
11 10 2 eqtr4di 
 |-  ( h = W -> ( .i ` h ) = ., )
12 11 oveqd 
 |-  ( h = W -> ( x ( .i ` h ) y ) = ( x ., y ) )
13 fveq2 
 |-  ( h = W -> ( Scalar ` h ) = ( Scalar ` W ) )
14 13 3 eqtr4di 
 |-  ( h = W -> ( Scalar ` h ) = F )
15 14 fveq2d 
 |-  ( h = W -> ( 0g ` ( Scalar ` h ) ) = ( 0g ` F ) )
16 15 4 eqtr4di 
 |-  ( h = W -> ( 0g ` ( Scalar ` h ) ) = .0. )
17 12 16 eqeq12d 
 |-  ( h = W -> ( ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) <-> ( x ., y ) = .0. ) )
18 17 ralbidv 
 |-  ( h = W -> ( A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) <-> A. y e. s ( x ., y ) = .0. ) )
19 8 18 rabeqbidv 
 |-  ( h = W -> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) } = { x e. V | A. y e. s ( x ., y ) = .0. } )
20 9 19 mpteq12dv 
 |-  ( h = W -> ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) } ) = ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) )
21 df-ocv 
 |-  ocv = ( h e. _V |-> ( s e. ~P ( Base ` h ) |-> { x e. ( Base ` h ) | A. y e. s ( x ( .i ` h ) y ) = ( 0g ` ( Scalar ` h ) ) } ) )
22 eqid 
 |-  ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) = ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } )
23 1 fvexi 
 |-  V e. _V
24 ssrab2 
 |-  { x e. V | A. y e. s ( x ., y ) = .0. } C_ V
25 23 24 elpwi2 
 |-  { x e. V | A. y e. s ( x ., y ) = .0. } e. ~P V
26 25 a1i 
 |-  ( s e. ~P V -> { x e. V | A. y e. s ( x ., y ) = .0. } e. ~P V )
27 22 26 fmpti 
 |-  ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) : ~P V --> ~P V
28 23 pwex 
 |-  ~P V e. _V
29 fex2 
 |-  ( ( ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) : ~P V --> ~P V /\ ~P V e. _V /\ ~P V e. _V ) -> ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) e. _V )
30 27 28 28 29 mp3an 
 |-  ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) e. _V
31 20 21 30 fvmpt 
 |-  ( W e. _V -> ( ocv ` W ) = ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) )
32 6 31 syl 
 |-  ( W e. X -> ( ocv ` W ) = ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) )
33 5 32 syl5eq 
 |-  ( W e. X -> ._|_ = ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) )