Theorem opexmid

Description: Law of excluded middle for orthoposets. ( chjo analog.) (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Hypotheses	opexmid.b	$$⊢B={\mathrm{Base}}_K$$
	opexmid.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
	opexmid.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	opexmid.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
Assertion	opexmid	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		opexmid.b	$$⊢B={\mathrm{Base}}_K$$
2		opexmid.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{oc}\left(K\right)$$
3		opexmid.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		opexmid.u	$$⊢\underset{\dot{}}{1}=\mathrm{1.}\left(K\right)$$
5		eqid	$$⊢{\le }_K={\le }_K$$
6		eqid	$$⊢\mathrm{meet}\left(K\right)=\mathrm{meet}\left(K\right)$$
7		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
8	1 5 2 3 6 7 4	oposlem	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\wedge X\in B\right)\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X{\le }_{K}X\to \underset{\dot{}}{\perp }\left(X\right){\le }_K\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\mathrm{meet}\left(K\right)\underset{\dot{}}{\perp }\left(X\right)=\mathrm{0.}\left(K\right)\right)$$
9	8	3anidm23	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to \left(\left(\underset{\dot{}}{\perp }\left(X\right)\in B\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(X\right)\right)=X\wedge \left(X{\le }_{K}X\to \underset{\dot{}}{\perp }\left(X\right){\le }_K\underset{\dot{}}{\perp }\left(X\right)\right)\right)\wedge X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}\wedge X\mathrm{meet}\left(K\right)\underset{\dot{}}{\perp }\left(X\right)=\mathrm{0.}\left(K\right)\right)$$
10	9	simp2d	$$⊢\left(K\in \mathrm{OP}\wedge X\in B\right)\to X\underset{\dot{}}{\vee }\underset{\dot{}}{\perp }\left(X\right)=\underset{\dot{}}{1}$$