Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  opoccl Structured version   Unicode version

Theorem opoccl 30054
Description: Closure of orthocomplement operation. (choccl 22810 analog.) (Contributed by NM, 20-Oct-2011.)
Hypotheses
Ref Expression
opoccl.b  |-  B  =  ( Base `  K
)
opoccl.o  |-  ._|_  =  ( oc `  K )
Assertion
Ref Expression
opoccl  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  (  ._|_  `  X )  e.  B )

Proof of Theorem opoccl
StepHypRef Expression
1 opoccl.b . . . . 5  |-  B  =  ( Base `  K
)
2 eqid 2438 . . . . 5  |-  ( le
`  K )  =  ( le `  K
)
3 opoccl.o . . . . 5  |-  ._|_  =  ( oc `  K )
4 eqid 2438 . . . . 5  |-  ( join `  K )  =  (
join `  K )
5 eqid 2438 . . . . 5  |-  ( meet `  K )  =  (
meet `  K )
6 eqid 2438 . . . . 5  |-  ( 0.
`  K )  =  ( 0. `  K
)
7 eqid 2438 . . . . 5  |-  ( 1.
`  K )  =  ( 1. `  K
)
81, 2, 3, 4, 5, 6, 7oposlem 30043 . . . 4  |-  ( ( K  e.  OP  /\  X  e.  B  /\  X  e.  B )  ->  ( ( (  ._|_  `  X )  e.  B  /\  (  ._|_  `  (  ._|_  `  X ) )  =  X  /\  ( X ( le `  K ) X  -> 
(  ._|_  `  X )
( le `  K
) (  ._|_  `  X
) ) )  /\  ( X ( join `  K
) (  ._|_  `  X
) )  =  ( 1. `  K )  /\  ( X (
meet `  K )
(  ._|_  `  X )
)  =  ( 0.
`  K ) ) )
983anidm23 1244 . . 3  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  ( ( (  ._|_  `  X )  e.  B  /\  (  ._|_  `  (  ._|_  `  X ) )  =  X  /\  ( X ( le `  K ) X  -> 
(  ._|_  `  X )
( le `  K
) (  ._|_  `  X
) ) )  /\  ( X ( join `  K
) (  ._|_  `  X
) )  =  ( 1. `  K )  /\  ( X (
meet `  K )
(  ._|_  `  X )
)  =  ( 0.
`  K ) ) )
109simp1d 970 . 2  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  ( (  ._|_  `  X
)  e.  B  /\  (  ._|_  `  (  ._|_  `  X ) )  =  X  /\  ( X ( le `  K
) X  ->  (  ._|_  `  X ) ( le `  K ) (  ._|_  `  X ) ) ) )
1110simp1d 970 1  |-  ( ( K  e.  OP  /\  X  e.  B )  ->  (  ._|_  `  X )  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937    = wceq 1653    e. wcel 1726   class class class wbr 4214   ` cfv 5456  (class class class)co 6083   Basecbs 13471   lecple 13538   occoc 13539   joincjn 14403   meetcmee 14404   0.cp0 14468   1.cp1 14469   OPcops 30032
This theorem is referenced by:  opcon2b  30057  oplecon3b  30060  oplecon1b  30061  opoc1  30062  opltcon3b  30064  opltcon1b  30065  opltcon2b  30066  riotaocN  30069  oldmm1  30077  oldmm2  30078  oldmm3N  30079  oldmm4  30080  oldmj1  30081  oldmj2  30082  oldmj3  30083  oldmj4  30084  olm11  30087  latmassOLD  30089  omllaw2N  30104  omllaw4  30106  cmtcomlemN  30108  cmt2N  30110  cmt3N  30111  cmt4N  30112  cmtbr2N  30113  cmtbr3N  30114  cmtbr4N  30115  lecmtN  30116  omlfh1N  30118  omlfh3N  30119  omlspjN  30121  cvrcon3b  30137  cvrcmp2  30144  atlatmstc  30179  glbconN  30236  glbconxN  30237  cvrexch  30279  1cvrco  30331  1cvratex  30332  1cvrjat  30334  polval2N  30765  polsubN  30766  2polpmapN  30772  2polvalN  30773  poldmj1N  30787  pmapj2N  30788  polatN  30790  2polatN  30791  pnonsingN  30792  ispsubcl2N  30806  polsubclN  30811  poml4N  30812  pmapojoinN  30827  pl42lem1N  30838  lhpoc2N  30874  lhpocnle  30875  lhpmod2i2  30897  lhpmod6i1  30898  lhprelat3N  30899  trlcl  31023  trlle  31043  docaclN  31984  doca2N  31986  djajN  31997  dih1  32146  dih1dimatlem  32189  dochcl  32213  dochvalr3  32223  doch2val2  32224  dochss  32225  dochocss  32226  dochoc  32227  dochnoncon  32251  djhlj  32261
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-nul 4340
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086  df-oposet 30036
  Copyright terms: Public domain W3C validator