Theorem cvlexchb1

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011)

	Ref	Expression
Hypotheses	cvlexch.b	$$⊢B={\mathrm{Base}}_K$$
	cvlexch.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cvlexch.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	cvlexch.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
Assertion	cvlexchb1	$$⊢\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)\leftrightarrow X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		cvlexch.b	$$⊢B={\mathrm{Base}}_K$$
2		cvlexch.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		cvlexch.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		cvlexch.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		cvllat	$$⊢K\in \mathrm{CvLat}\to K\in \mathrm{Lat}$$
6	5	adantr	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to K\in \mathrm{Lat}$$
7		simpr3	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to X\in B$$
8		simpr2	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to Q\in A$$
9	1 4	atbase	$$⊢Q\in A\to Q\in B$$
10	8 9	syl	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to Q\in B$$
11	1 2 3	latlej1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Q\in B\right)\to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)$$
12	6 7 10 11	syl3anc	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)$$
13	12	3adant3	$$⊢\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 X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)$$
14	13	adantr	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)$$
15		simpr	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)$$
16		simpr1	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to P\in A$$
17	1 4	atbase	$$⊢P\in A\to P\in B$$
18	16 17	syl	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to P\in B$$
19	1 3	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge Q\in B\right)\to X\underset{\dot{}}{\vee }Q\in B$$
20	6 7 10 19	syl3anc	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to X\underset{\dot{}}{\vee }Q\in B$$
21	1 2 3	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(X\in B\wedge P\in B\wedge X\underset{\dot{}}{\vee }Q\in B\right)\right)\to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
22	6 7 18 20 21	syl13anc	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
23	22	3adant3	$$⊢\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(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
24	23	adantr	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
25	14 15 24	mpbi2and	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to \left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)$$
26	1 2 3	latlej1	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge P\in B\right)\to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)$$
27	6 7 18 26	syl3anc	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)$$
28	27	3adant3	$$⊢\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 X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)$$
29	28	adantr	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)$$
30	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)$$
31	30	imp	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)$$
32	1 3	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge P\in B\right)\to X\underset{\dot{}}{\vee }P\in B$$
33	6 7 18 32	syl3anc	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to X\underset{\dot{}}{\vee }P\in B$$
34	1 2 3	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(X\in B\wedge Q\in B\wedge X\underset{\dot{}}{\vee }P\in B\right)\right)\to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\wedge Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)$$
35	6 7 10 33 34	syl13anc	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\wedge Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)$$
36	35	3adant3	$$⊢\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(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\wedge Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)$$
37	36	adantr	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to \left(\left(X\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\wedge Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)$$
38	29 31 37	mpbi2and	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)$$
39	1 2	latasymb	$$⊢\left(K\in \mathrm{Lat}\wedge X\underset{\dot{}}{\vee }P\in B\wedge X\underset{\dot{}}{\vee }Q\in B\right)\to \left(\left(\left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\wedge \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\right)$$
40	6 33 20 39	syl3anc	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to \left(\left(\left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\wedge \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\right)$$
41	40	3adant3	$$⊢\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(\left(\left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\wedge \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\right)$$
42	41	adantr	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to \left(\left(\left(X\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\wedge \left(X\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)\leftrightarrow X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\right)$$
43	25 38 42	mpbi2and	$$⊢\left(\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)\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\to X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q$$
44	43	ex	$$⊢\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 X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\right)$$
45	1 2 3	latlej2	$$⊢\left(K\in \mathrm{Lat}\wedge X\in B\wedge P\in B\right)\to P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)$$
46	6 7 18 45	syl3anc	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)$$
47		breq2	$$⊢X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\to \left(P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\leftrightarrow P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
48	46 47	syl5ibcom	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to \left(X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\to P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
49	48	3adant3	$$⊢\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(X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\to P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
50	44 49	impbid	$$⊢\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)\leftrightarrow X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\right)$$