Theorem omllaw

Description: The orthomodular law. (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Hypotheses	omllaw.b	$$⊢B={\mathrm{Base}}_K$$
	omllaw.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	omllaw.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	omllaw.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	omllaw.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
Assertion	omllaw	$$⊢\left(K\in \mathrm{OML}\wedge X\in B\wedge Y\in B\right)\to \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)$$

Proof

Step	Hyp	Ref	Expression
1		omllaw.b	$$⊢B={\mathrm{Base}}_K$$
2		omllaw.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		omllaw.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		omllaw.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
5		omllaw.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
6	1 2 3 4 5	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)$$
7	6	simprbi	$$⊢K\in \mathrm{OML}\to \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)$$
8		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }y\right)$$
9		id	$$⊢x=X\to x=X$$
10		fveq2	$$⊢x=X\to \underset{\dot{}}{\perp }\left(x\right)=\underset{\dot{}}{\perp }\left(X\right)$$
11	10	oveq2d	$$⊢x=X\to y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)=y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)$$
12	9 11	oveq12d	$$⊢x=X\to x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)=X\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)\right)$$
13	12	eqeq2d	$$⊢x=X\to \left(y=x\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(x\right)\right)\leftrightarrow y=X\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)\right)\right)$$
14	8 13	imbi12d	$$⊢x=X\to \left(\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)\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)$$
15		breq2	$$⊢y=Y\to \left(X\underset{\dot{}}{\le }y\leftrightarrow X\underset{\dot{}}{\le }Y\right)$$
16		id	$$⊢y=Y\to y=Y$$
17		oveq1	$$⊢y=Y\to y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)=Y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)$$
18	17	oveq2d	$$⊢y=Y\to X\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)\right)=X\underset{\dot{}}{\vee }\left(Y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)\right)$$
19	16 18	eqeq12d	$$⊢y=Y\to \left(y=X\underset{\dot{}}{\vee }\left(y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)\right)\leftrightarrow Y=X\underset{\dot{}}{\vee }\left(Y\underset{\dot{}}{\wedge }\underset{\dot{}}{\perp }\left(X\right)\right)\right)$$
20	15 19	imbi12d	$$⊢y=Y\to \left(\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)\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)$$
21	14 20	rspc2v	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\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)\to \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)$$
22	7 21	syl5com	$$⊢K\in \mathrm{OML}\to \left(\left(X\in B\wedge Y\in B\right)\to \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)$$
23	22	3impib	$$⊢\left(K\in \mathrm{OML}\wedge X\in B\wedge Y\in B\right)\to \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)$$