Metamath Proof Explorer

Theorem hdmapoc

Description: Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in Holland95 p. 14. (Contributed by NM, 17-Jun-2015)

Ref Expression
Hypotheses hdmapoc.h 
|- H = ( LHyp ` K )
hdmapoc.u 
|- U = ( ( DVecH ` K ) ` W )
hdmapoc.v 
|- V = ( Base ` U )
hdmapoc.r 
|- R = ( Scalar ` U )
hdmapoc.z 
|- .0. = ( 0g ` R )
hdmapoc.o 
|- O = ( ( ocH ` K ) ` W )
hdmapoc.s 
|- S = ( ( HDMap ` K ) ` W )
hdmapoc.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
hdmapoc.x 
|- ( ph -> X C_ V )
Assertion hdmapoc 
|- ( ph -> ( O ` X ) = { y e. V | A. z e. X ( ( S ` z ) ` y ) = .0. } )

Proof

Step Hyp Ref Expression
1 hdmapoc.h 
 |-  H = ( LHyp ` K )
2 hdmapoc.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 hdmapoc.v 
 |-  V = ( Base ` U )
4 hdmapoc.r 
 |-  R = ( Scalar ` U )
5 hdmapoc.z 
 |-  .0. = ( 0g ` R )
6 hdmapoc.o 
 |-  O = ( ( ocH ` K ) ` W )
7 hdmapoc.s 
 |-  S = ( ( HDMap ` K ) ` W )
8 hdmapoc.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 hdmapoc.x 
 |-  ( ph -> X C_ V )
10 1 2 3 6 dochssv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( O ` X ) C_ V )
11 8 9 10 syl2anc 
 |-  ( ph -> ( O ` X ) C_ V )
12 11 sseld 
 |-  ( ph -> ( y e. ( O ` X ) -> y e. V ) )
13 12 pm4.71rd 
 |-  ( ph -> ( y e. ( O ` X ) <-> ( y e. V /\ y e. ( O ` X ) ) ) )
14 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
15 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
16 1 2 8 dvhlmod 
 |-  ( ph -> U e. LMod )
17 16 adantr 
 |-  ( ( ph /\ y e. V ) -> U e. LMod )
18 1 2 3 14 6 dochlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( O ` X ) e. ( LSubSp ` U ) )
19 8 9 18 syl2anc 
 |-  ( ph -> ( O ` X ) e. ( LSubSp ` U ) )
20 19 adantr 
 |-  ( ( ph /\ y e. V ) -> ( O ` X ) e. ( LSubSp ` U ) )
21 simpr 
 |-  ( ( ph /\ y e. V ) -> y e. V )
22 3 14 15 17 20 21 lspsnel5 
 |-  ( ( ph /\ y e. V ) -> ( y e. ( O ` X ) <-> ( ( LSpan ` U ) ` { y } ) C_ ( O ` X ) ) )
23 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
24 8 adantr 
 |-  ( ( ph /\ y e. V ) -> ( K e. HL /\ W e. H ) )
25 1 2 3 15 23 dihlsprn 
 |-  ( ( ( K e. HL /\ W e. H ) /\ y e. V ) -> ( ( LSpan ` U ) ` { y } ) e. ran ( ( DIsoH ` K ) ` W ) )
26 24 21 25 syl2anc 
 |-  ( ( ph /\ y e. V ) -> ( ( LSpan ` U ) ` { y } ) e. ran ( ( DIsoH ` K ) ` W ) )
27 1 23 2 3 6 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( O ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
28 8 9 27 syl2anc 
 |-  ( ph -> ( O ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
29 28 adantr 
 |-  ( ( ph /\ y e. V ) -> ( O ` X ) e. ran ( ( DIsoH ` K ) ` W ) )
30 1 23 6 24 26 29 dochord 
 |-  ( ( ph /\ y e. V ) -> ( ( ( LSpan ` U ) ` { y } ) C_ ( O ` X ) <-> ( O ` ( O ` X ) ) C_ ( O ` ( ( LSpan ` U ) ` { y } ) ) ) )
31 21 snssd 
 |-  ( ( ph /\ y e. V ) -> { y } C_ V )
32 1 2 6 3 15 24 31 dochocsp 
 |-  ( ( ph /\ y e. V ) -> ( O ` ( ( LSpan ` U ) ` { y } ) ) = ( O ` { y } ) )
33 32 sseq2d 
 |-  ( ( ph /\ y e. V ) -> ( ( O ` ( O ` X ) ) C_ ( O ` ( ( LSpan ` U ) ` { y } ) ) <-> ( O ` ( O ` X ) ) C_ ( O ` { y } ) ) )
34 9 adantr 
 |-  ( ( ph /\ y e. V ) -> X C_ V )
35 1 23 2 3 6 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { y } C_ V ) -> ( O ` { y } ) e. ran ( ( DIsoH ` K ) ` W ) )
36 24 31 35 syl2anc 
 |-  ( ( ph /\ y e. V ) -> ( O ` { y } ) e. ran ( ( DIsoH ` K ) ` W ) )
37 1 2 3 23 6 24 34 36 dochsscl 
 |-  ( ( ph /\ y e. V ) -> ( X C_ ( O ` { y } ) <-> ( O ` ( O ` X ) ) C_ ( O ` { y } ) ) )
38 33 37 bitr4d 
 |-  ( ( ph /\ y e. V ) -> ( ( O ` ( O ` X ) ) C_ ( O ` ( ( LSpan ` U ) ` { y } ) ) <-> X C_ ( O ` { y } ) ) )
39 22 30 38 3bitrd 
 |-  ( ( ph /\ y e. V ) -> ( y e. ( O ` X ) <-> X C_ ( O ` { y } ) ) )
40 dfss3 
 |-  ( X C_ ( O ` { y } ) <-> A. z e. X z e. ( O ` { y } ) )
41 39 40 bitrdi 
 |-  ( ( ph /\ y e. V ) -> ( y e. ( O ` X ) <-> A. z e. X z e. ( O ` { y } ) ) )
42 8 ad2antrr 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> ( K e. HL /\ W e. H ) )
43 34 sselda 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> z e. V )
44 simplr 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> y e. V )
45 1 6 2 3 4 5 7 42 43 44 hdmapellkr 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> ( ( ( S ` z ) ` y ) = .0. <-> y e. ( O ` { z } ) ) )
46 1 6 2 3 42 44 43 dochsncom 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> ( y e. ( O ` { z } ) <-> z e. ( O ` { y } ) ) )
47 45 46 bitrd 
 |-  ( ( ( ph /\ y e. V ) /\ z e. X ) -> ( ( ( S ` z ) ` y ) = .0. <-> z e. ( O ` { y } ) ) )
48 47 ralbidva 
 |-  ( ( ph /\ y e. V ) -> ( A. z e. X ( ( S ` z ) ` y ) = .0. <-> A. z e. X z e. ( O ` { y } ) ) )
49 41 48 bitr4d 
 |-  ( ( ph /\ y e. V ) -> ( y e. ( O ` X ) <-> A. z e. X ( ( S ` z ) ` y ) = .0. ) )
50 49 pm5.32da 
 |-  ( ph -> ( ( y e. V /\ y e. ( O ` X ) ) <-> ( y e. V /\ A. z e. X ( ( S ` z ) ` y ) = .0. ) ) )
51 13 50 bitrd 
 |-  ( ph -> ( y e. ( O ` X ) <-> ( y e. V /\ A. z e. X ( ( S ` z ) ` y ) = .0. ) ) )
52 51 abbi2dv 
 |-  ( ph -> ( O ` X ) = { y | ( y e. V /\ A. z e. X ( ( S ` z ) ` y ) = .0. ) } )
53 df-rab 
 |-  { y e. V | A. z e. X ( ( S ` z ) ` y ) = .0. } = { y | ( y e. V /\ A. z e. X ( ( S ` z ) ` y ) = .0. ) }
54 52 53 eqtr4di 
 |-  ( ph -> ( O ` X ) = { y e. V | A. z e. X ( ( S ` z ) ` y ) = .0. } )