Metamath Proof Explorer

Theorem elocv

Description: Elementhood in the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (Contributed 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 elocv 
|- ( A e. ( ._|_ ` S ) <-> ( S C_ V /\ A e. V /\ A. x e. S ( A ., x ) = .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 elfvdm 
 |-  ( A e. ( ._|_ ` S ) -> S e. dom ._|_ )
7 n0i 
 |-  ( A e. ( ._|_ ` S ) -> -. ( ._|_ ` S ) = (/) )
8 fvprc 
 |-  ( -. W e. _V -> ( ocv ` W ) = (/) )
9 5 8 eqtrid 
 |-  ( -. W e. _V -> ._|_ = (/) )
10 9 fveq1d 
 |-  ( -. W e. _V -> ( ._|_ ` S ) = ( (/) ` S ) )
11 0fv 
 |-  ( (/) ` S ) = (/)
12 10 11 eqtrdi 
 |-  ( -. W e. _V -> ( ._|_ ` S ) = (/) )
13 7 12 nsyl2 
 |-  ( A e. ( ._|_ ` S ) -> W e. _V )
14 1 2 3 4 5 ocvfval 
 |-  ( W e. _V -> ._|_ = ( s e. ~P V |-> { y e. V | A. x e. s ( y ., x ) = .0. } ) )
15 13 14 syl 
 |-  ( A e. ( ._|_ ` S ) -> ._|_ = ( s e. ~P V |-> { y e. V | A. x e. s ( y ., x ) = .0. } ) )
16 15 dmeqd 
 |-  ( A e. ( ._|_ ` S ) -> dom ._|_ = dom ( s e. ~P V |-> { y e. V | A. x e. s ( y ., x ) = .0. } ) )
17 1 fvexi 
 |-  V e. _V
18 17 rabex 
 |-  { y e. V | A. x e. s ( y ., x ) = .0. } e. _V
19 eqid 
 |-  ( s e. ~P V |-> { y e. V | A. x e. s ( y ., x ) = .0. } ) = ( s e. ~P V |-> { y e. V | A. x e. s ( y ., x ) = .0. } )
20 18 19 dmmpti 
 |-  dom ( s e. ~P V |-> { y e. V | A. x e. s ( y ., x ) = .0. } ) = ~P V
21 16 20 eqtrdi 
 |-  ( A e. ( ._|_ ` S ) -> dom ._|_ = ~P V )
22 6 21 eleqtrd 
 |-  ( A e. ( ._|_ ` S ) -> S e. ~P V )
23 22 elpwid 
 |-  ( A e. ( ._|_ ` S ) -> S C_ V )
24 1 2 3 4 5 ocvval 
 |-  ( S C_ V -> ( ._|_ ` S ) = { y e. V | A. x e. S ( y ., x ) = .0. } )
25 24 eleq2d 
 |-  ( S C_ V -> ( A e. ( ._|_ ` S ) <-> A e. { y e. V | A. x e. S ( y ., x ) = .0. } ) )
26 oveq1 
 |-  ( y = A -> ( y ., x ) = ( A ., x ) )
27 26 eqeq1d 
 |-  ( y = A -> ( ( y ., x ) = .0. <-> ( A ., x ) = .0. ) )
28 27 ralbidv 
 |-  ( y = A -> ( A. x e. S ( y ., x ) = .0. <-> A. x e. S ( A ., x ) = .0. ) )
29 28 elrab 
 |-  ( A e. { y e. V | A. x e. S ( y ., x ) = .0. } <-> ( A e. V /\ A. x e. S ( A ., x ) = .0. ) )
30 25 29 bitrdi 
 |-  ( S C_ V -> ( A e. ( ._|_ ` S ) <-> ( A e. V /\ A. x e. S ( A ., x ) = .0. ) ) )
31 23 30 biadanii 
 |-  ( A e. ( ._|_ ` S ) <-> ( S C_ V /\ ( A e. V /\ A. x e. S ( A ., x ) = .0. ) ) )
32 3anass 
 |-  ( ( S C_ V /\ A e. V /\ A. x e. S ( A ., x ) = .0. ) <-> ( S C_ V /\ ( A e. V /\ A. x e. S ( A ., x ) = .0. ) ) )
33 31 32 bitr4i 
 |-  ( A e. ( ._|_ ` S ) <-> ( S C_ V /\ A e. V /\ A. x e. S ( A ., x ) = .0. ) )