![]() |
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 28495 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 2760 | . . . . 5 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | opoccl.o | . . . . 5 ⊢ ⊥ = (oc‘𝐾) | |
4 | eqid 2760 | . . . . 5 ⊢ (join‘𝐾) = (join‘𝐾) | |
5 | eqid 2760 | . . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
6 | eqid 2760 | . . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
7 | eqid 2760 | . . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 34990 | . . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
9 | 8 | 3anidm23 1532 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
10 | 9 | simp1d 1137 | . 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋)))) |
11 | 10 | simp1d 1137 | 1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 = wceq 1632 ∈ wcel 2139 class class class wbr 4804 ‘cfv 6049 (class class class)co 6814 Basecbs 16079 lecple 16170 occoc 16171 joincjn 17165 meetcmee 17166 0.cp0 17258 1.cp1 17259 OPcops 34980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-nul 4941 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-sbc 3577 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-uni 4589 df-br 4805 df-dm 5276 df-iota 6012 df-fv 6057 df-ov 6817 df-oposet 34984 |
This theorem is referenced by: opcon2b 35005 oplecon3b 35008 oplecon1b 35009 opoc1 35010 opltcon3b 35012 opltcon1b 35013 opltcon2b 35014 riotaocN 35017 oldmm1 35025 oldmm2 35026 oldmm3N 35027 oldmm4 35028 oldmj1 35029 oldmj2 35030 oldmj3 35031 oldmj4 35032 olm11 35035 latmassOLD 35037 omllaw2N 35052 omllaw4 35054 cmtcomlemN 35056 cmt2N 35058 cmt3N 35059 cmt4N 35060 cmtbr2N 35061 cmtbr3N 35062 cmtbr4N 35063 lecmtN 35064 omlfh1N 35066 omlfh3N 35067 omlspjN 35069 cvrcon3b 35085 cvrcmp2 35092 atlatmstc 35127 glbconN 35184 glbconxN 35185 cvrexch 35227 1cvrco 35279 1cvratex 35280 1cvrjat 35282 polval2N 35713 polsubN 35714 2polpmapN 35720 2polvalN 35721 poldmj1N 35735 pmapj2N 35736 polatN 35738 2polatN 35739 pnonsingN 35740 ispsubcl2N 35754 polsubclN 35759 poml4N 35760 pmapojoinN 35775 pl42lem1N 35786 lhpoc2N 35822 lhpocnle 35823 lhpmod2i2 35845 lhpmod6i1 35846 lhprelat3N 35847 trlcl 35972 trlle 35992 docaclN 36933 doca2N 36935 djajN 36946 dih1 37095 dih1dimatlem 37138 dochcl 37162 dochvalr3 37172 doch2val2 37173 dochss 37174 dochocss 37175 dochoc 37176 dochnoncon 37200 djhlj 37210 |
Copyright terms: Public domain | W3C validator |