Theorem hlsuprexch

Description: A Hilbert lattice has the superposition and exchange properties. (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	hlsuprexch	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(\left(P\ne Q\to \exists z\in A\left(z\ne P\wedge z\ne Q\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\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		eqid	$$⊢{<}_K={<}_K$$
6		eqid	$$⊢\mathrm{0.}\left(K\right)=\mathrm{0.}\left(K\right)$$
7		eqid	$$⊢\mathrm{1.}\left(K\right)=\mathrm{1.}\left(K\right)$$
8	1 2 5 3 6 7 4	ishlat2	$$⊢K\in \mathrm{HL}\leftrightarrow \left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)\wedge \left(\forall x\in A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\right)\wedge \exists x\in B\exists y\in B\exists z\in B\left(\left(\mathrm{0.}\left(K\right){<}_{K}x\wedge x{<}_{K}y\right)\wedge \left(y{<}_{K}z\wedge z{<}_K\mathrm{1.}\left(K\right)\right)\right)\right)\right)$$
9		simprl	$$⊢\left(\left(K\in \mathrm{OML}\wedge K\in \mathrm{CLat}\wedge K\in \mathrm{AtLat}\right)\wedge \left(\forall x\in A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\right)\wedge \exists x\in B\exists y\in B\exists z\in B\left(\left(\mathrm{0.}\left(K\right){<}_{K}x\wedge x{<}_{K}y\right)\wedge \left(y{<}_{K}z\wedge z{<}_K\mathrm{1.}\left(K\right)\right)\right)\right)\right)\to \forall x\in A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\right)$$
10	8 9	sylbi	$$⊢K\in \mathrm{HL}\to \forall x\in A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\right)$$
11		neeq1	$$⊢x=P\to \left(x\ne y\leftrightarrow P\ne y\right)$$
12		neeq2	$$⊢x=P\to \left(z\ne x\leftrightarrow z\ne P\right)$$
13		oveq1	$$⊢x=P\to x\underset{\dot{}}{\vee }y=P\underset{\dot{}}{\vee }y$$
14	13	breq2d	$$⊢x=P\to \left(z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\leftrightarrow z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)$$
15	12 14	3anbi13d	$$⊢x=P\to \left(\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\leftrightarrow \left(z\ne P\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)\right)$$
16	15	rexbidv	$$⊢x=P\to \left(\exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\leftrightarrow \exists z\in A\left(z\ne P\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)\right)$$
17	11 16	imbi12d	$$⊢x=P\to \left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\leftrightarrow \left(P\ne y\to \exists z\in A\left(z\ne P\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)\right)\right)$$
18		breq1	$$⊢x=P\to \left(x\underset{\dot{}}{\le }z\leftrightarrow P\underset{\dot{}}{\le }z\right)$$
19	18	notbid	$$⊢x=P\to \left(\neg x\underset{\dot{}}{\le }z\leftrightarrow \neg P\underset{\dot{}}{\le }z\right)$$
20		breq1	$$⊢x=P\to \left(x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\leftrightarrow P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)$$
21	19 20	anbi12d	$$⊢x=P\to \left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\right)$$
22		oveq2	$$⊢x=P\to z\underset{\dot{}}{\vee }x=z\underset{\dot{}}{\vee }P$$
23	22	breq2d	$$⊢x=P\to \left(y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\leftrightarrow y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)$$
24	21 23	imbi12d	$$⊢x=P\to \left(\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\leftrightarrow \left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)$$
25	24	ralbidv	$$⊢x=P\to \left(\forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\leftrightarrow \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)$$
26	17 25	anbi12d	$$⊢x=P\to \left(\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\right)\leftrightarrow \left(\left(P\ne y\to \exists z\in A\left(z\ne P\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)\right)$$
27		neeq2	$$⊢y=Q\to \left(P\ne y\leftrightarrow P\ne Q\right)$$
28		neeq2	$$⊢y=Q\to \left(z\ne y\leftrightarrow z\ne Q\right)$$
29		oveq2	$$⊢y=Q\to P\underset{\dot{}}{\vee }y=P\underset{\dot{}}{\vee }Q$$
30	29	breq2d	$$⊢y=Q\to \left(z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\leftrightarrow z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
31	28 30	3anbi23d	$$⊢y=Q\to \left(\left(z\ne P\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)\leftrightarrow \left(z\ne P\wedge z\ne Q\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
32	31	rexbidv	$$⊢y=Q\to \left(\exists z\in A\left(z\ne P\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)\leftrightarrow \exists z\in A\left(z\ne P\wedge z\ne Q\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)$$
33	27 32	imbi12d	$$⊢y=Q\to \left(\left(P\ne y\to \exists z\in A\left(z\ne P\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)\right)\leftrightarrow \left(P\ne Q\to \exists z\in A\left(z\ne P\wedge z\ne Q\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\right)$$
34		oveq2	$$⊢y=Q\to z\underset{\dot{}}{\vee }y=z\underset{\dot{}}{\vee }Q$$
35	34	breq2d	$$⊢y=Q\to \left(P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\leftrightarrow P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)$$
36	35	anbi2d	$$⊢y=Q\to \left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)\right)$$
37		breq1	$$⊢y=Q\to \left(y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\leftrightarrow Q\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)$$
38	36 37	imbi12d	$$⊢y=Q\to \left(\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow \left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)$$
39	38	ralbidv	$$⊢y=Q\to \left(\forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)$$
40	33 39	anbi12d	$$⊢y=Q\to \left(\left(\left(P\ne y\to \exists z\in A\left(z\ne P\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)\leftrightarrow \left(\left(P\ne Q\to \exists z\in A\left(z\ne P\wedge z\ne Q\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)\right)$$
41	26 40	rspc2v	$$⊢\left(P\in A\wedge Q\in A\right)\to \left(\forall x\in A\forall y\in A\left(\left(x\ne y\to \exists z\in A\left(z\ne x\wedge z\ne y\wedge z\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }y\right)\right)\right)\wedge \forall z\in B\left(\left(\neg x\underset{\dot{}}{\le }z\wedge x\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }y\right)\right)\to y\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }x\right)\right)\right)\to \left(\left(P\ne Q\to \exists z\in A\left(z\ne P\wedge z\ne Q\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)\right)$$
42	10 41	mpan9	$$⊢\left(K\in \mathrm{HL}\wedge \left(P\in A\wedge Q\in A\right)\right)\to \left(\left(P\ne Q\to \exists z\in A\left(z\ne P\wedge z\ne Q\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)$$
43	42	3impb	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to \left(\left(P\ne Q\to \exists z\in A\left(z\ne P\wedge z\ne Q\wedge z\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \forall z\in B\left(\left(\neg P\underset{\dot{}}{\le }z\wedge P\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(z\underset{\dot{}}{\vee }P\right)\right)\right)$$