Metamath Proof Explorer

Theorem dochss

Description: Subset law for orthocomplement. (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses dochss.h 
|- H = ( LHyp ` K )
dochss.u 
|- U = ( ( DVecH ` K ) ` W )
dochss.v 
|- V = ( Base ` U )
dochss.o 
|- ._|_ = ( ( ocH ` K ) ` W )
Assertion dochss 
|- ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) )

Proof

Step Hyp Ref Expression
1 dochss.h 
 |-  H = ( LHyp ` K )
2 dochss.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 dochss.v 
 |-  V = ( Base ` U )
4 dochss.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
5 simp1l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> K e. HL )
6 hlclat 
 |-  ( K e. HL -> K e. CLat )
7 5 6 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> K e. CLat )
8 ssrab2 
 |-  { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } C_ ( Base ` K )
9 8 a1i 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } C_ ( Base ` K ) )
10 simpll3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) /\ z e. ( Base ` K ) ) /\ Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) ) -> X C_ Y )
11 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) /\ z e. ( Base ` K ) ) /\ Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) ) -> Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) )
12 10 11 sstrd 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) /\ z e. ( Base ` K ) ) /\ Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) ) -> X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) )
13 12 ex 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) /\ z e. ( Base ` K ) ) -> ( Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) -> X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) ) )
14 13 ss2rabdv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } C_ { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } )
15 eqid 
 |-  ( Base ` K ) = ( Base ` K )
16 eqid 
 |-  ( le ` K ) = ( le ` K )
17 eqid 
 |-  ( glb ` K ) = ( glb ` K )
18 15 16 17 clatglbss 
 |-  ( ( K e. CLat /\ { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } C_ ( Base ` K ) /\ { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } C_ { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) -> ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ( le ` K ) ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) )
19 7 9 14 18 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ( le ` K ) ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) )
20 hlop 
 |-  ( K e. HL -> K e. OP )
21 5 20 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> K e. OP )
22 15 17 clatglbcl 
 |-  ( ( K e. CLat /\ { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } C_ ( Base ` K ) ) -> ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) e. ( Base ` K ) )
23 7 8 22 sylancl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) e. ( Base ` K ) )
24 ssrab2 
 |-  { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } C_ ( Base ` K )
25 15 17 clatglbcl 
 |-  ( ( K e. CLat /\ { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } C_ ( Base ` K ) ) -> ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) e. ( Base ` K ) )
26 7 24 25 sylancl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) e. ( Base ` K ) )
27 eqid 
 |-  ( oc ` K ) = ( oc ` K )
28 15 16 27 oplecon3b 
 |-  ( ( K e. OP /\ ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) e. ( Base ` K ) /\ ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) e. ( Base ` K ) ) -> ( ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ( le ` K ) ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) <-> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ( le ` K ) ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
29 21 23 26 28 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ( le ` K ) ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) <-> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ( le ` K ) ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
30 19 29 mpbid 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ( le ` K ) ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) )
31 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( K e. HL /\ W e. H ) )
32 15 27 opoccl 
 |-  ( ( K e. OP /\ ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) e. ( Base ` K ) )
33 21 26 32 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) e. ( Base ` K ) )
34 15 27 opoccl 
 |-  ( ( K e. OP /\ ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) e. ( Base ` K ) ) -> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) e. ( Base ` K ) )
35 21 23 34 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) e. ( Base ` K ) )
36 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
37 15 16 1 36 dihord 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) e. ( Base ` K ) /\ ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) e. ( Base ` K ) ) -> ( ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) C_ ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) <-> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ( le ` K ) ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
38 31 33 35 37 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) C_ ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) <-> ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ( le ` K ) ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
39 30 38 mpbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) C_ ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
40 15 17 27 1 36 2 3 4 dochval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V ) -> ( ._|_ ` Y ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
41 40 3adant3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ._|_ ` Y ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | Y C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
42 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> X C_ Y )
43 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> Y C_ V )
44 42 43 sstrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> X C_ V )
45 15 17 27 1 36 2 3 4 dochval 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X C_ V ) -> ( ._|_ ` X ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
46 31 44 45 syl2anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ._|_ ` X ) = ( ( ( DIsoH ` K ) ` W ) ` ( ( oc ` K ) ` ( ( glb ` K ) ` { z e. ( Base ` K ) | X C_ ( ( ( DIsoH ` K ) ` W ) ` z ) } ) ) ) )
47 39 41 46 3sstr4d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ Y C_ V /\ X C_ Y ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) )