This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ocvval

Description: Value of the orthocomplement of a subset (normally a subspace) of a pre-Hilbert space. (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 ocvval 
|- ( S C_ V -> ( ._|_ ` S ) = { 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 1 fvexi 
 |-  V e. _V
7 6 elpw2 
 |-  ( S e. ~P V <-> S C_ V )
8 1 2 3 4 5 ocvfval 
 |-  ( W e. _V -> ._|_ = ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) )
9 8 fveq1d 
 |-  ( W e. _V -> ( ._|_ ` S ) = ( ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) ` S ) )
10 raleq 
 |-  ( s = S -> ( A. y e. s ( x ., y ) = .0. <-> A. y e. S ( x ., y ) = .0. ) )
11 10 rabbidv 
 |-  ( s = S -> { x e. V | A. y e. s ( x ., y ) = .0. } = { x e. V | A. y e. S ( x ., y ) = .0. } )
12 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. } )
13 6 rabex 
 |-  { x e. V | A. y e. S ( x ., y ) = .0. } e. _V
14 11 12 13 fvmpt 
 |-  ( S e. ~P V -> ( ( s e. ~P V |-> { x e. V | A. y e. s ( x ., y ) = .0. } ) ` S ) = { x e. V | A. y e. S ( x ., y ) = .0. } )
15 9 14 sylan9eq 
 |-  ( ( W e. _V /\ S e. ~P V ) -> ( ._|_ ` S ) = { x e. V | A. y e. S ( x ., y ) = .0. } )
16 0fv 
 |-  ( (/) ` S ) = (/)
17 fvprc 
 |-  ( -. W e. _V -> ( ocv ` W ) = (/) )
18 5 17 eqtrid 
 |-  ( -. W e. _V -> ._|_ = (/) )
19 18 fveq1d 
 |-  ( -. W e. _V -> ( ._|_ ` S ) = ( (/) ` S ) )
20 ssrab2 
 |-  { x e. V | A. y e. S ( x ., y ) = .0. } C_ V
21 fvprc 
 |-  ( -. W e. _V -> ( Base ` W ) = (/) )
22 1 21 eqtrid 
 |-  ( -. W e. _V -> V = (/) )
23 sseq0 
 |-  ( ( { x e. V | A. y e. S ( x ., y ) = .0. } C_ V /\ V = (/) ) -> { x e. V | A. y e. S ( x ., y ) = .0. } = (/) )
24 20 22 23 sylancr 
 |-  ( -. W e. _V -> { x e. V | A. y e. S ( x ., y ) = .0. } = (/) )
25 16 19 24 3eqtr4a 
 |-  ( -. W e. _V -> ( ._|_ ` S ) = { x e. V | A. y e. S ( x ., y ) = .0. } )
26 25 adantr 
 |-  ( ( -. W e. _V /\ S e. ~P V ) -> ( ._|_ ` S ) = { x e. V | A. y e. S ( x ., y ) = .0. } )
27 15 26 pm2.61ian 
 |-  ( S e. ~P V -> ( ._|_ ` S ) = { x e. V | A. y e. S ( x ., y ) = .0. } )
28 7 27 sylbir 
 |-  ( S C_ V -> ( ._|_ ` S ) = { x e. V | A. y e. S ( x ., y ) = .0. } )