| Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > opoccl | Structured version Visualization version GIF version | ||
| Description: Closure of orthocomplement operation. (choccl 31285 analog.) (Contributed by NM, 20-Oct-2011.) |
| Ref | Expression |
|---|---|
| opoccl.b | ⊢ 𝐵 = (Base‘𝐾) |
| opoccl.o | ⊢ ⊥ = (oc‘𝐾) |
| Ref | Expression |
|---|---|
| opoccl | ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | opoccl.b | . . . . 5 ⊢ 𝐵 = (Base‘𝐾) | |
| 2 | eqid 2729 | . . . . 5 ⊢ (le‘𝐾) = (le‘𝐾) | |
| 3 | opoccl.o | . . . . 5 ⊢ ⊥ = (oc‘𝐾) | |
| 4 | eqid 2729 | . . . . 5 ⊢ (join‘𝐾) = (join‘𝐾) | |
| 5 | eqid 2729 | . . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
| 6 | eqid 2729 | . . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
| 7 | eqid 2729 | . . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
| 8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 39168 | . . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
| 9 | 8 | 3anidm23 1423 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
| 10 | 9 | simp1d 1142 | . 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋)))) |
| 11 | 10 | simp1d 1142 | 1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 class class class wbr 5102 ‘cfv 6499 (class class class)co 7369 Basecbs 17155 lecple 17203 occoc 17204 joincjn 18252 meetcmee 18253 0.cp0 18362 1.cp1 18363 OPcops 39158 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-nul 5256 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ne 2926 df-ral 3045 df-rab 3403 df-v 3446 df-dif 3914 df-un 3916 df-ss 3928 df-nul 4293 df-if 4485 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-br 5103 df-dm 5641 df-iota 6452 df-fv 6507 df-ov 7372 df-oposet 39162 |
| This theorem is referenced by: opcon2b 39183 oplecon3b 39186 oplecon1b 39187 opoc1 39188 opltcon3b 39190 opltcon1b 39191 opltcon2b 39192 riotaocN 39195 oldmm1 39203 oldmm2 39204 oldmm3N 39205 oldmm4 39206 oldmj1 39207 oldmj2 39208 oldmj3 39209 oldmj4 39210 olm11 39213 latmassOLD 39215 omllaw2N 39230 omllaw4 39232 cmtcomlemN 39234 cmt2N 39236 cmt3N 39237 cmt4N 39238 cmtbr2N 39239 cmtbr3N 39240 cmtbr4N 39241 lecmtN 39242 omlfh1N 39244 omlfh3N 39245 omlspjN 39247 cvrcon3b 39263 cvrcmp2 39270 atlatmstc 39305 glbconN 39363 glbconNOLD 39364 glbconxN 39365 cvrexch 39407 1cvrco 39459 1cvratex 39460 1cvrjat 39462 polval2N 39893 polsubN 39894 2polpmapN 39900 2polvalN 39901 poldmj1N 39915 pmapj2N 39916 polatN 39918 2polatN 39919 pnonsingN 39920 ispsubcl2N 39934 polsubclN 39939 poml4N 39940 pmapojoinN 39955 pl42lem1N 39966 lhpoc2N 40002 lhpocnle 40003 lhpmod2i2 40025 lhpmod6i1 40026 lhprelat3N 40027 trlcl 40151 trlle 40171 docaclN 41111 doca2N 41113 djajN 41124 dih1 41273 dih1dimatlem 41316 dochcl 41340 dochvalr3 41350 doch2val2 41351 dochss 41352 dochocss 41353 dochoc 41354 dochnoncon 41378 djhlj 41388 |
| Copyright terms: Public domain | W3C validator |