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 29387 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 2737 | . . . . 5 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | opoccl.o | . . . . 5 ⊢ ⊥ = (oc‘𝐾) | |
4 | eqid 2737 | . . . . 5 ⊢ (join‘𝐾) = (join‘𝐾) | |
5 | eqid 2737 | . . . . 5 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
6 | eqid 2737 | . . . . 5 ⊢ (0.‘𝐾) = (0.‘𝐾) | |
7 | eqid 2737 | . . . . 5 ⊢ (1.‘𝐾) = (1.‘𝐾) | |
8 | 1, 2, 3, 4, 5, 6, 7 | oposlem 36933 | . . . 4 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
9 | 8 | 3anidm23 1423 | . . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋(meet‘𝐾)( ⊥ ‘𝑋)) = (0.‘𝐾))) |
10 | 9 | simp1d 1144 | . 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋)))) |
11 | 10 | simp1d 1144 | 1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘𝑋) ∈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 = wceq 1543 ∈ wcel 2110 class class class wbr 5053 ‘cfv 6380 (class class class)co 7213 Basecbs 16760 lecple 16809 occoc 16810 joincjn 17818 meetcmee 17819 0.cp0 17929 1.cp1 17930 OPcops 36923 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-nul 5199 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-uni 4820 df-br 5054 df-dm 5561 df-iota 6338 df-fv 6388 df-ov 7216 df-oposet 36927 |
This theorem is referenced by: opcon2b 36948 oplecon3b 36951 oplecon1b 36952 opoc1 36953 opltcon3b 36955 opltcon1b 36956 opltcon2b 36957 riotaocN 36960 oldmm1 36968 oldmm2 36969 oldmm3N 36970 oldmm4 36971 oldmj1 36972 oldmj2 36973 oldmj3 36974 oldmj4 36975 olm11 36978 latmassOLD 36980 omllaw2N 36995 omllaw4 36997 cmtcomlemN 36999 cmt2N 37001 cmt3N 37002 cmt4N 37003 cmtbr2N 37004 cmtbr3N 37005 cmtbr4N 37006 lecmtN 37007 omlfh1N 37009 omlfh3N 37010 omlspjN 37012 cvrcon3b 37028 cvrcmp2 37035 atlatmstc 37070 glbconN 37128 glbconxN 37129 cvrexch 37171 1cvrco 37223 1cvratex 37224 1cvrjat 37226 polval2N 37657 polsubN 37658 2polpmapN 37664 2polvalN 37665 poldmj1N 37679 pmapj2N 37680 polatN 37682 2polatN 37683 pnonsingN 37684 ispsubcl2N 37698 polsubclN 37703 poml4N 37704 pmapojoinN 37719 pl42lem1N 37730 lhpoc2N 37766 lhpocnle 37767 lhpmod2i2 37789 lhpmod6i1 37790 lhprelat3N 37791 trlcl 37915 trlle 37935 docaclN 38875 doca2N 38877 djajN 38888 dih1 39037 dih1dimatlem 39080 dochcl 39104 dochvalr3 39114 doch2val2 39115 dochss 39116 dochocss 39117 dochoc 39118 dochnoncon 39142 djhlj 39152 |
Copyright terms: Public domain | W3C validator |