# Metamath Proof Explorer

## Theorem isoml

Description: The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011)

Ref Expression
Hypotheses isoml.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
isoml.l
isoml.j
isoml.m
isoml.o
Assertion isoml

### Proof

Step Hyp Ref Expression
1 isoml.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 isoml.l
3 isoml.j
4 isoml.m
5 isoml.o
6 fveq2 ${⊢}{k}={K}\to {\mathrm{Base}}_{{k}}={\mathrm{Base}}_{{K}}$
7 6 1 eqtr4di ${⊢}{k}={K}\to {\mathrm{Base}}_{{k}}={B}$
8 fveq2 ${⊢}{k}={K}\to {\le }_{{k}}={\le }_{{K}}$
9 8 2 eqtr4di
10 9 breqd
11 fveq2 ${⊢}{k}={K}\to \mathrm{join}\left({k}\right)=\mathrm{join}\left({K}\right)$
12 11 3 eqtr4di
13 eqidd ${⊢}{k}={K}\to {x}={x}$
14 fveq2 ${⊢}{k}={K}\to \mathrm{meet}\left({k}\right)=\mathrm{meet}\left({K}\right)$
15 14 4 eqtr4di
16 eqidd ${⊢}{k}={K}\to {y}={y}$
17 fveq2 ${⊢}{k}={K}\to \mathrm{oc}\left({k}\right)=\mathrm{oc}\left({K}\right)$
18 17 5 eqtr4di
19 18 fveq1d
20 15 16 19 oveq123d
21 12 13 20 oveq123d
22 21 eqeq2d
23 10 22 imbi12d
24 7 23 raleqbidv
25 7 24 raleqbidv
26 df-oml ${⊢}\mathrm{OML}=\left\{{k}\in \mathrm{OL}|\forall {x}\in {\mathrm{Base}}_{{k}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{k}}\phantom{\rule{.4em}{0ex}}\left({x}{\le }_{{k}}{y}\to {y}={x}\mathrm{join}\left({k}\right)\left({y}\mathrm{meet}\left({k}\right)\mathrm{oc}\left({k}\right)\left({x}\right)\right)\right)\right\}$
27 25 26 elrab2