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	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	isoml.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	isoml.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	isoml.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
Assertion	isoml	$$⊢K\in \mathrm{OML}\leftrightarrow \left(K\in \mathrm{OL}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isoml.b	$$⊢B={\mathrm{Base}}_K$$
2		isoml.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		isoml.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		isoml.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		isoml.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
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	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
10	9	breqd	$$⊢k=K\to \left(x{\le }_{k}y\leftrightarrow x\underset{\dot{}}{\le }y\right)$$
11		fveq2	$$⊢k=K\to \mathrm{join}\left(k\right)=\mathrm{join}\left(K\right)$$
12	11 3	eqtr4di	$$⊢k=K\to \mathrm{join}\left(k\right)=\underset{\dot{}}{\vee }$$
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	$$⊢k=K\to \mathrm{meet}\left(k\right)=\underset{\dot{}}{\wedge }$$
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	$$⊢k=K\to \mathrm{oc}\left(k\right)=\underset{\dot{}}{\perp }$$
19	18	fveq1d	$$⊢k=K\to \mathrm{oc}\left(k\right)\left(x\right)=\underset{\dot{}}{\perp }\left(x\right)$$
20	15 16 19	oveq123d	$$⊢k=K\to y\mathrm{meet}\left(k\right)\mathrm{oc}\left(k\right)\left(x\right)=y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)$$
21	12 13 20	oveq123d	$$⊢k=K\to x\mathrm{join}\left(k\right)\left(y\mathrm{meet}\left(k\right)\mathrm{oc}\left(k\right)\left(x\right)\right)=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)$$
22	21	eqeq2d	$$⊢k=K\to \left(y=x\mathrm{join}\left(k\right)\left(y\mathrm{meet}\left(k\right)\mathrm{oc}\left(k\right)\left(x\right)\right)\leftrightarrow y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)$$
23	10 22	imbi12d	$$⊢k=K\to \left(\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)\leftrightarrow \left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\right)$$
24	7 23	raleqbidv	$$⊢k=K\to \left(\forall y\in {\mathrm{Base}}_k\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)\leftrightarrow \forall y\in B\left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\right)$$
25	7 24	raleqbidv	$$⊢k=K\to \left(\forall x\in {\mathrm{Base}}_k\forall y\in {\mathrm{Base}}_k\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)\leftrightarrow \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\right)$$
26		df-oml	$$⊢\mathrm{OML}=\left\{k\in \mathrm{OL}|\forall x\in {\mathrm{Base}}_k\forall y\in {\mathrm{Base}}_k\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	$$⊢K\in \mathrm{OML}\leftrightarrow \left(K\in \mathrm{OL}\wedge \forall x\in B\forall y\in B\left(x\underset{\dot{}}{\le }y\to y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\right)\right)$$