Theorem hlsupr

Description: A Hilbert lattice has the superposition property. Theorem 13.2 in Crawley p. 107. (Contributed by NM, 30-Jan-2012)

	Ref	Expression
Hypotheses	hlsupr.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	hlsupr.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	hlsupr.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	hlsupr	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge P\ne Q\right)\to \exists r\in A\left(r\ne P\wedge r\ne Q\wedge r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hlsupr.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		hlsupr.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		hlsupr.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
5	4 1 2 3	hlsuprexch	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(\left(P\ne Q\to \exists r\in A\left(r\ne P\wedge r\ne Q\wedge r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \forall r\in {\mathrm{Base}}_K\left(\left(\neg P\underset{\dot{}}{\le }r\wedge P\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(r\underset{\dot{}}{\vee }P\right)\right)\right)$$
6	5	simpld	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(P\ne Q\to \exists r\in A\left(r\ne P\wedge r\ne Q\wedge r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
7	6	imp	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge P\ne Q\right)\to \exists r\in A\left(r\ne P\wedge r\ne Q\wedge r\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$