Metamath Proof Explorer

Theorem dochvalr

Description: Orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014)

Ref Expression
Hypotheses dochvalr.o 
|- ._|_ = ( oc ` K )
dochvalr.h 
|- H = ( LHyp ` K )
dochvalr.i 
|- I = ( ( DIsoH ` K ) ` W )
dochvalr.n 
|- N = ( ( ocH ` K ) ` W )
Assertion dochvalr 
|- ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( N ` X ) = ( I ` ( ._|_ ` ( `' I ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 dochvalr.o 
 |-  ._|_ = ( oc ` K )
2 dochvalr.h 
 |-  H = ( LHyp ` K )
3 dochvalr.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dochvalr.n 
 |-  N = ( ( ocH ` K ) ` W )
5 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
6 eqid 
 |-  ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
7 2 5 3 6 dihrnss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 eqid 
 |-  ( glb ` K ) = ( glb ` K )
10 8 9 1 2 3 5 6 4 dochval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ ( Base ` ( ( DVecH ` K ) ` W ) ) ) -> ( N ` X ) = ( I ` ( ._|_ ` ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) ) ) )
11 7 10 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( N ` X ) = ( I ` ( ._|_ ` ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) ) ) )
12 eqid 
 |-  ( le ` K ) = ( le ` K )
13 hllat 
 |-  ( K e. HL -> K e. Lat )
14 13 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> K e. Lat )
15 hlclat 
 |-  ( K e. HL -> K e. CLat )
16 15 ad2antrr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> K e. CLat )
17 ssrab2 
 |-  { y e. ( Base ` K ) | X C_ ( I ` y ) } C_ ( Base ` K )
18 8 9 clatglbcl 
 |-  ( ( K e. CLat /\ { y e. ( Base ` K ) | X C_ ( I ` y ) } C_ ( Base ` K ) ) -> ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) e. ( Base ` K ) )
19 16 17 18 sylancl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) e. ( Base ` K ) )
20 8 2 3 dihcnvcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. ( Base ` K ) )
21 17 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> { y e. ( Base ` K ) | X C_ ( I ` y ) } C_ ( Base ` K ) )
22 ssid 
 |-  X C_ X
23 2 3 dihcnvid2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( `' I ` X ) ) = X )
24 22 23 sseqtrrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X C_ ( I ` ( `' I ` X ) ) )
25 fveq2 
 |-  ( y = ( `' I ` X ) -> ( I ` y ) = ( I ` ( `' I ` X ) ) )
26 25 sseq2d 
 |-  ( y = ( `' I ` X ) -> ( X C_ ( I ` y ) <-> X C_ ( I ` ( `' I ` X ) ) ) )
27 26 elrab 
 |-  ( ( `' I ` X ) e. { y e. ( Base ` K ) | X C_ ( I ` y ) } <-> ( ( `' I ` X ) e. ( Base ` K ) /\ X C_ ( I ` ( `' I ` X ) ) ) )
28 20 24 27 sylanbrc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) e. { y e. ( Base ` K ) | X C_ ( I ` y ) } )
29 8 12 9 clatglble 
 |-  ( ( K e. CLat /\ { y e. ( Base ` K ) | X C_ ( I ` y ) } C_ ( Base ` K ) /\ ( `' I ` X ) e. { y e. ( Base ` K ) | X C_ ( I ` y ) } ) -> ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) ( le ` K ) ( `' I ` X ) )
30 16 21 28 29 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) ( le ` K ) ( `' I ` X ) )
31 fveq2 
 |-  ( y = z -> ( I ` y ) = ( I ` z ) )
32 31 sseq2d 
 |-  ( y = z -> ( X C_ ( I ` y ) <-> X C_ ( I ` z ) ) )
33 32 elrab 
 |-  ( z e. { y e. ( Base ` K ) | X C_ ( I ` y ) } <-> ( z e. ( Base ` K ) /\ X C_ ( I ` z ) ) )
34 23 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) /\ z e. ( Base ` K ) ) -> ( I ` ( `' I ` X ) ) = X )
35 34 sseq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) /\ z e. ( Base ` K ) ) -> ( ( I ` ( `' I ` X ) ) C_ ( I ` z ) <-> X C_ ( I ` z ) ) )
36 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) /\ z e. ( Base ` K ) ) -> ( K e. HL /\ W e. H ) )
37 20 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) /\ z e. ( Base ` K ) ) -> ( `' I ` X ) e. ( Base ` K ) )
38 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) /\ z e. ( Base ` K ) ) -> z e. ( Base ` K ) )
39 8 12 2 3 dihord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( `' I ` X ) e. ( Base ` K ) /\ z e. ( Base ` K ) ) -> ( ( I ` ( `' I ` X ) ) C_ ( I ` z ) <-> ( `' I ` X ) ( le ` K ) z ) )
40 36 37 38 39 syl3anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) /\ z e. ( Base ` K ) ) -> ( ( I ` ( `' I ` X ) ) C_ ( I ` z ) <-> ( `' I ` X ) ( le ` K ) z ) )
41 35 40 bitr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) /\ z e. ( Base ` K ) ) -> ( X C_ ( I ` z ) <-> ( `' I ` X ) ( le ` K ) z ) )
42 41 biimpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) /\ z e. ( Base ` K ) ) -> ( X C_ ( I ` z ) -> ( `' I ` X ) ( le ` K ) z ) )
43 42 expimpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( z e. ( Base ` K ) /\ X C_ ( I ` z ) ) -> ( `' I ` X ) ( le ` K ) z ) )
44 33 43 biimtrid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( z e. { y e. ( Base ` K ) | X C_ ( I ` y ) } -> ( `' I ` X ) ( le ` K ) z ) )
45 44 ralrimiv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> A. z e. { y e. ( Base ` K ) | X C_ ( I ` y ) } ( `' I ` X ) ( le ` K ) z )
46 8 12 9 clatleglb 
 |-  ( ( K e. CLat /\ ( `' I ` X ) e. ( Base ` K ) /\ { y e. ( Base ` K ) | X C_ ( I ` y ) } C_ ( Base ` K ) ) -> ( ( `' I ` X ) ( le ` K ) ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) <-> A. z e. { y e. ( Base ` K ) | X C_ ( I ` y ) } ( `' I ` X ) ( le ` K ) z ) )
47 16 20 21 46 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( `' I ` X ) ( le ` K ) ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) <-> A. z e. { y e. ( Base ` K ) | X C_ ( I ` y ) } ( `' I ` X ) ( le ` K ) z ) )
48 45 47 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( `' I ` X ) ( le ` K ) ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) )
49 8 12 14 19 20 30 48 latasymd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) = ( `' I ` X ) )
50 49 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( ._|_ ` ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) ) = ( ._|_ ` ( `' I ` X ) ) )
51 50 fveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( I ` ( ._|_ ` ( ( glb ` K ) ` { y e. ( Base ` K ) | X C_ ( I ` y ) } ) ) ) = ( I ` ( ._|_ ` ( `' I ` X ) ) ) )
52 11 51 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> ( N ` X ) = ( I ` ( ._|_ ` ( `' I ` X ) ) ) )