Theorem cvlexch1

Description: An atomic covering lattice has the exchange property. (Contributed by NM, 6-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	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)$$

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	iscvlat	$$⊢K\in \mathrm{CvLat}\leftrightarrow \left(K\in \mathrm{AtLat}\wedge \forall p\in A\forall q\in A\forall x\in B\left(\left(\neg p\underset{\dot{}}{\le }x\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)\right)\right)$$
6	5	simprbi	$$⊢K\in \mathrm{CvLat}\to \forall p\in A\forall q\in A\forall x\in B\left(\left(\neg p\underset{\dot{}}{\le }x\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)\right)$$
7		breq1	$$⊢p=P\to \left(p\underset{\dot{}}{\le }x\leftrightarrow P\underset{\dot{}}{\le }x\right)$$
8	7	notbid	$$⊢p=P\to \left(\neg p\underset{\dot{}}{\le }x\leftrightarrow \neg P\underset{\dot{}}{\le }x\right)$$
9		breq1	$$⊢p=P\to \left(p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\leftrightarrow P\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)$$
10	8 9	anbi12d	$$⊢p=P\to \left(\left(\neg p\underset{\dot{}}{\le }x\wedge p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }x\wedge P\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\right)$$
11		oveq2	$$⊢p=P\to x\underset{\dot{}}{\vee }p=x\underset{\dot{}}{\vee }P$$
12	11	breq2d	$$⊢p=P\to \left(q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\leftrightarrow q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }P\right)\right)$$
13	10 12	imbi12d	$$⊢p=P\to \left(\left(\left(\neg p\underset{\dot{}}{\le }x\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)\right)\leftrightarrow \left(\left(\neg P\underset{\dot{}}{\le }x\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)\right)\right)$$
14		oveq2	$$⊢q=Q\to x\underset{\dot{}}{\vee }q=x\underset{\dot{}}{\vee }Q$$
15	14	breq2d	$$⊢q=Q\to \left(P\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\leftrightarrow P\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }Q\right)\right)$$
16	15	anbi2d	$$⊢q=Q\to \left(\left(\neg P\underset{\dot{}}{\le }x\wedge P\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }x\wedge P\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }Q\right)\right)\right)$$
17		breq1	$$⊢q=Q\to \left(q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }P\right)\leftrightarrow Q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }P\right)\right)$$
18	16 17	imbi12d	$$⊢q=Q\to \left(\left(\left(\neg P\underset{\dot{}}{\le }x\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)\right)\leftrightarrow \left(\left(\neg P\underset{\dot{}}{\le }x\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)\right)\right)$$
19		breq2	$$⊢x=X\to \left(P\underset{\dot{}}{\le }x\leftrightarrow P\underset{\dot{}}{\le }X\right)$$
20	19	notbid	$$⊢x=X\to \left(\neg P\underset{\dot{}}{\le }x\leftrightarrow \neg P\underset{\dot{}}{\le }X\right)$$
21		oveq1	$$⊢x=X\to x\underset{\dot{}}{\vee }Q=X\underset{\dot{}}{\vee }Q$$
22	21	breq2d	$$⊢x=X\to \left(P\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }Q\right)\leftrightarrow P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)$$
23	20 22	anbi12d	$$⊢x=X\to \left(\left(\neg P\underset{\dot{}}{\le }x\wedge P\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }Q\right)\right)\leftrightarrow \left(\neg P\underset{\dot{}}{\le }X\wedge P\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }Q\right)\right)\right)$$
24		oveq1	$$⊢x=X\to x\underset{\dot{}}{\vee }P=X\underset{\dot{}}{\vee }P$$
25	24	breq2d	$$⊢x=X\to \left(Q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }P\right)\leftrightarrow Q\underset{\dot{}}{\le }\left(X\underset{\dot{}}{\vee }P\right)\right)$$
26	23 25	imbi12d	$$⊢x=X\to \left(\left(\left(\neg P\underset{\dot{}}{\le }x\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)\right)\leftrightarrow \left(\left(\neg P\underset{\dot{}}{\le }X\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)\right)\right)$$
27	13 18 26	rspc3v	$$⊢\left(P\in A\wedge Q\in A\wedge X\in B\right)\to \left(\forall p\in A\forall q\in A\forall x\in B\left(\left(\neg p\underset{\dot{}}{\le }x\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)\right)\to \left(\left(\neg P\underset{\dot{}}{\le }X\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)\right)\right)$$
28	6 27	mpan9	$$⊢\left(K\in \mathrm{CvLat}\wedge \left(P\in A\wedge Q\in A\wedge X\in B\right)\right)\to \left(\left(\neg P\underset{\dot{}}{\le }X\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)\right)$$
29	28	exp4b	$$⊢K\in \mathrm{CvLat}\to \left(\left(P\in A\wedge Q\in A\wedge X\in B\right)\to \left(\neg P\underset{\dot{}}{\le }X\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)\right)\right)$$
30	29	3imp	$$⊢\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)$$