# Metamath Proof Explorer

## Definition df-oml

Description: Define the class of orthomodular lattices. Definition from Kalmbach p. 16. (Contributed by NM, 18-Sep-2011)

Ref Expression
Assertion df-oml ${⊢}\mathrm{OML}=\left\{{l}\in \mathrm{OL}|\forall {a}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{l}}{b}\to {b}={a}\mathrm{join}\left({l}\right)\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)\right)\right\}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 coml ${class}\mathrm{OML}$
1 vl ${setvar}{l}$
2 col ${class}\mathrm{OL}$
3 va ${setvar}{a}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{l}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{l}}$
7 vb ${setvar}{b}$
8 3 cv ${setvar}{a}$
9 cple ${class}\mathrm{le}$
10 5 9 cfv ${class}{\le }_{{l}}$
11 7 cv ${setvar}{b}$
12 8 11 10 wbr ${wff}{a}{\le }_{{l}}{b}$
13 cjn ${class}\mathrm{join}$
14 5 13 cfv ${class}\mathrm{join}\left({l}\right)$
15 cmee ${class}\mathrm{meet}$
16 5 15 cfv ${class}\mathrm{meet}\left({l}\right)$
17 coc ${class}\mathrm{oc}$
18 5 17 cfv ${class}\mathrm{oc}\left({l}\right)$
19 8 18 cfv ${class}\mathrm{oc}\left({l}\right)\left({a}\right)$
20 11 19 16 co ${class}\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)$
21 8 20 14 co ${class}\left({a}\mathrm{join}\left({l}\right)\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)\right)$
22 11 21 wceq ${wff}{b}={a}\mathrm{join}\left({l}\right)\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)$
23 12 22 wi ${wff}\left({a}{\le }_{{l}}{b}\to {b}={a}\mathrm{join}\left({l}\right)\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)\right)$
24 23 7 6 wral ${wff}\forall {b}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{l}}{b}\to {b}={a}\mathrm{join}\left({l}\right)\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)\right)$
25 24 3 6 wral ${wff}\forall {a}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{l}}{b}\to {b}={a}\mathrm{join}\left({l}\right)\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)\right)$
26 25 1 2 crab ${class}\left\{{l}\in \mathrm{OL}|\forall {a}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{l}}{b}\to {b}={a}\mathrm{join}\left({l}\right)\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)\right)\right\}$
27 0 26 wceq ${wff}\mathrm{OML}=\left\{{l}\in \mathrm{OL}|\forall {a}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\forall {b}\in {\mathrm{Base}}_{{l}}\phantom{\rule{.4em}{0ex}}\left({a}{\le }_{{l}}{b}\to {b}={a}\mathrm{join}\left({l}\right)\left({b}\mathrm{meet}\left({l}\right)\mathrm{oc}\left({l}\right)\left({a}\right)\right)\right)\right\}$