Metamath Proof Explorer

Theorem hlhilocv

Description: The orthocomplement for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015) (Revised by Mario Carneiro, 29-Jun-2015)

Ref Expression
Hypotheses hlhil0.h 
|- H = ( LHyp ` K )
hlhil0.l 
|- L = ( ( DVecH ` K ) ` W )
hlhil0.u 
|- U = ( ( HLHil ` K ) ` W )
hlhil0.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hlhilocv.v 
|- V = ( Base ` L )
hlhilocv.n 
|- N = ( ( ocH ` K ) ` W )
hlhilocv.o 
|- O = ( ocv ` U )
hlhilocv.x 
|- ( ph -> X C_ V )
Assertion hlhilocv 
|- ( ph -> ( O ` X ) = ( N ` X ) )

Proof

Step Hyp Ref Expression
1 hlhil0.h 
 |-  H = ( LHyp ` K )
2 hlhil0.l 
 |-  L = ( ( DVecH ` K ) ` W )
3 hlhil0.u 
 |-  U = ( ( HLHil ` K ) ` W )
4 hlhil0.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
5 hlhilocv.v 
 |-  V = ( Base ` L )
6 hlhilocv.n 
 |-  N = ( ( ocH ` K ) ` W )
7 hlhilocv.o 
 |-  O = ( ocv ` U )
8 hlhilocv.x 
 |-  ( ph -> X C_ V )
9 1 3 4 2 5 hlhilbase 
 |-  ( ph -> V = ( Base ` U ) )
10 rabeq 
 |-  ( V = ( Base ` U ) -> { y e. V | A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) } = { y e. ( Base ` U ) | A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) } )
11 9 10 syl 
 |-  ( ph -> { y e. V | A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) } = { y e. ( Base ` U ) | A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) } )
12 eqid 
 |-  ( ( HDMap ` K ) ` W ) = ( ( HDMap ` K ) ` W )
13 4 ad2antrr 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> ( K e. HL /\ W e. H ) )
14 eqid 
 |-  ( .i ` U ) = ( .i ` U )
15 simplr 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> y e. V )
16 8 adantr 
 |-  ( ( ph /\ y e. V ) -> X C_ V )
17 16 sselda 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> z e. V )
18 1 2 5 12 3 13 14 15 17 hlhilipval 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> ( y ( .i ` U ) z ) = ( ( ( ( HDMap ` K ) ` W ) ` z ) ` y ) )
19 eqid 
 |-  ( Scalar ` L ) = ( Scalar ` L )
20 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
21 eqid 
 |-  ( 0g ` ( Scalar ` L ) ) = ( 0g ` ( Scalar ` L ) )
22 1 2 19 3 20 4 21 hlhils0 
 |-  ( ph -> ( 0g ` ( Scalar ` L ) ) = ( 0g ` ( Scalar ` U ) ) )
23 22 eqcomd 
 |-  ( ph -> ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` L ) ) )
24 23 ad2antrr 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` L ) ) )
25 18 24 eqeq12d 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> ( ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) <-> ( ( ( ( HDMap ` K ) ` W ) ` z ) ` y ) = ( 0g ` ( Scalar ` L ) ) ) )
26 25 ralbidva 
 |-  ( ( ph /\ y e. V ) -> ( A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) <-> A. z e. X ( ( ( ( HDMap ` K ) ` W ) ` z ) ` y ) = ( 0g ` ( Scalar ` L ) ) ) )
27 26 rabbidva 
 |-  ( ph -> { y e. V | A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) } = { y e. V | A. z e. X ( ( ( ( HDMap ` K ) ` W ) ` z ) ` y ) = ( 0g ` ( Scalar ` L ) ) } )
28 11 27 eqtr3d 
 |-  ( ph -> { y e. ( Base ` U ) | A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) } = { y e. V | A. z e. X ( ( ( ( HDMap ` K ) ` W ) ` z ) ` y ) = ( 0g ` ( Scalar ` L ) ) } )
29 8 9 sseqtrd 
 |-  ( ph -> X C_ ( Base ` U ) )
30 eqid 
 |-  ( Base ` U ) = ( Base ` U )
31 eqid 
 |-  ( 0g ` ( Scalar ` U ) ) = ( 0g ` ( Scalar ` U ) )
32 30 14 20 31 7 ocvval 
 |-  ( X C_ ( Base ` U ) -> ( O ` X ) = { y e. ( Base ` U ) | A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) } )
33 29 32 syl 
 |-  ( ph -> ( O ` X ) = { y e. ( Base ` U ) | A. z e. X ( y ( .i ` U ) z ) = ( 0g ` ( Scalar ` U ) ) } )
34 1 2 5 19 21 6 12 4 8 hdmapoc 
 |-  ( ph -> ( N ` X ) = { y e. V | A. z e. X ( ( ( ( HDMap ` K ) ` W ) ` z ) ` y ) = ( 0g ` ( Scalar ` L ) ) } )
35 28 33 34 3eqtr4d 
 |-  ( ph -> ( O ` X ) = ( N ` X ) )