Theorem cvlexchb2

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012)

	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	cvlexchb2	$$⊢\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(Q\underset{\dot{}}{\vee }X\right)\leftrightarrow P\underset{\dot{}}{\vee }X=Q\underset{\dot{}}{\vee }X\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	1 2 3 4	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)$$
6		cvllat	$$⊢K\in \mathrm{CvLat}\to K\in \mathrm{Lat}$$
7	6	3ad2ant1	$$⊢\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 K\in \mathrm{Lat}$$
8		simp22	$$⊢\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 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)\wedge \neg P\underset{\dot{}}{\le }X\right)\to Q\in B$$
11		simp23	$$⊢\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\in B$$
12	1 3	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge Q\in B\wedge X\in B\right)\to Q\underset{\dot{}}{\vee }X=X\underset{\dot{}}{\vee }Q$$
13	7 10 11 12	syl3anc	$$⊢\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 Q\underset{\dot{}}{\vee }X=X\underset{\dot{}}{\vee }Q$$
14	13	breq2d	$$⊢\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(Q\underset{\dot{}}{\vee }X\right)\leftrightarrow P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
15		simp21	$$⊢\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 P\in A$$
16	1 4	atbase	$$⊢P\in A\to P\in B$$
17	15 16	syl	$$⊢\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 P\in B$$
18	1 3	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge P\in B\wedge X\in B\right)\to P\underset{\dot{}}{\vee }X=X\underset{\dot{}}{\vee }P$$
19	7 17 11 18	syl3anc	$$⊢\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 P\underset{\dot{}}{\vee }X=X\underset{\dot{}}{\vee }P$$
20	19 13	eqeq12d	$$⊢\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{}}{\vee }X=Q\underset{\dot{}}{\vee }X\leftrightarrow X\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }Q\right)$$
21	5 14 20	3bitr4d	$$⊢\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(Q\underset{\dot{}}{\vee }X\right)\leftrightarrow P\underset{\dot{}}{\vee }X=Q\underset{\dot{}}{\vee }X\right)$$