Theorem hlexch1

Description: A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011)

	Ref	Expression
Hypotheses	hlsuprexch.b	$$⊢B={\mathrm{Base}}_K$$
	hlsuprexch.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	hlsuprexch.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	hlsuprexch.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	hlexch1	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\wedge \neg P\underset{\dot{}}{\le }X\right)\to \left(P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\to Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlsuprexch.b	$$⊢B={\mathrm{Base}}_K$$
2		hlsuprexch.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		hlsuprexch.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		hlsuprexch.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		hlcvl	$$⊢K\in \mathrm{HL}\to K\in \mathrm{CvLat}$$
6	1 2 3 4	cvlexch1	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\wedge \neg P\underset{\dot{}}{\le }X\right)\to \left(P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\to Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)$$
7	5 6	syl3an1	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\wedge \neg P\underset{\dot{}}{\le }X\right)\to \left(P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\to Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)$$