Theorem iscvlat

Description: The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		iscvlat.b	$$⊢B={\mathrm{Base}}_K$$
2		iscvlat.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		iscvlat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		iscvlat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		fveq2	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=\mathrm{Atoms}\left(K\right)$$
6	5 4	eqtr4di	$$⊢k=K\to \mathrm{Atoms}\left(k\right)=A$$
7		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
8	7 1	eqtr4di	$$⊢k=K\to {\mathrm{Base}}_k=B$$
9		fveq2	$$⊢k=K\to {\le }_k={\le }_K$$
10	9 2	eqtr4di	$$⊢k=K\to {\le }_k=\underset{\dot{}}{\le }$$
11	10	breqd	$$⊢k=K\to \left(p{\le }_{k}x\leftrightarrow p\underset{\dot{}}{\le }x\right)$$
12	11	notbid	$$⊢k=K\to \left(\neg p{\le }_{k}x\leftrightarrow \neg p\underset{\dot{}}{\le }x\right)$$
13		eqidd	$$⊢k=K\to p=p$$
14		fveq2	$$⊢k=K\to \mathrm{join}\left(k\right)=\mathrm{join}\left(K\right)$$
15	14 3	eqtr4di	$$⊢k=K\to \mathrm{join}\left(k\right)=\underset{\dot{}}{\vee }$$
16	15	oveqd	$$⊢k=K\to x\mathrm{join}\left(k\right)q=x\underset{\dot{}}{\vee }q$$
17	13 10 16	breq123d	$$⊢k=K\to \left(p{\le }_k\left(x\mathrm{join}\left(k\right)q\right)\leftrightarrow p\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }q\right)\right)$$
18	12 17	anbi12d	$$⊢k=K\to \left(\left(\neg p{\le }_{k}x\wedge p{\le }_k\left(x\mathrm{join}\left(k\right)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)$$
19		eqidd	$$⊢k=K\to q=q$$
20	15	oveqd	$$⊢k=K\to x\mathrm{join}\left(k\right)p=x\underset{\dot{}}{\vee }p$$
21	19 10 20	breq123d	$$⊢k=K\to \left(q{\le }_k\left(x\mathrm{join}\left(k\right)p\right)\leftrightarrow q\underset{\dot{}}{\le }\left(x\underset{\dot{}}{\vee }p\right)\right)$$
22	18 21	imbi12d	$$⊢k=K\to \left(\left(\left(\neg p{\le }_{k}x\wedge p{\le }_k\left(x\mathrm{join}\left(k\right)q\right)\right)\to q{\le }_k\left(x\mathrm{join}\left(k\right)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)$$
23	8 22	raleqbidv	$$⊢k=K\to \left(\forall x\in {\mathrm{Base}}_k\left(\left(\neg p{\le }_{k}x\wedge p{\le }_k\left(x\mathrm{join}\left(k\right)q\right)\right)\to q{\le }_k\left(x\mathrm{join}\left(k\right)p\right)\right)\leftrightarrow \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)$$
24	6 23	raleqbidv	$$⊢k=K\to \left(\forall q\in \mathrm{Atoms}\left(k\right)\forall x\in {\mathrm{Base}}_k\left(\left(\neg p{\le }_{k}x\wedge p{\le }_k\left(x\mathrm{join}\left(k\right)q\right)\right)\to q{\le }_k\left(x\mathrm{join}\left(k\right)p\right)\right)\leftrightarrow \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)$$
25	6 24	raleqbidv	$$⊢k=K\to \left(\forall p\in \mathrm{Atoms}\left(k\right)\forall q\in \mathrm{Atoms}\left(k\right)\forall x\in {\mathrm{Base}}_k\left(\left(\neg p{\le }_{k}x\wedge p{\le }_k\left(x\mathrm{join}\left(k\right)q\right)\right)\to q{\le }_k\left(x\mathrm{join}\left(k\right)p\right)\right)\leftrightarrow \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)$$
26		df-cvlat	$$⊢\mathrm{CvLat}=\left\{k\in \mathrm{AtLat}|\forall p\in \mathrm{Atoms}\left(k\right)\forall q\in \mathrm{Atoms}\left(k\right)\forall x\in {\mathrm{Base}}_k\left(\left(\neg p{\le }_{k}x\wedge p{\le }_k\left(x\mathrm{join}\left(k\right)q\right)\right)\to q{\le }_k\left(x\mathrm{join}\left(k\right)p\right)\right)\right\}$$
27	25 26	elrab2	$$⊢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)$$