Theorem isdlat

Description: Property of being a distributive lattice. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	isdlat.b	$$⊢B={\mathrm{Base}}_K$$
	isdlat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	isdlat.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
Assertion	isdlat	$$⊢K\in \mathrm{DLat}\leftrightarrow \left(K\in \mathrm{Lat}\wedge \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isdlat.b	$$⊢B={\mathrm{Base}}_K$$
2		isdlat.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		isdlat.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		fveq2	$$⊢k=K\to {\mathrm{Base}}_k={\mathrm{Base}}_K$$
5	4 1	eqtr4di	$$⊢k=K\to {\mathrm{Base}}_k=B$$
6		fveq2	$$⊢k=K\to \mathrm{join}\left(k\right)=\mathrm{join}\left(K\right)$$
7	6 2	eqtr4di	$$⊢k=K\to \mathrm{join}\left(k\right)=\underset{\dot{}}{\vee }$$
8		fveq2	$$⊢k=K\to \mathrm{meet}\left(k\right)=\mathrm{meet}\left(K\right)$$
9	8 3	eqtr4di	$$⊢k=K\to \mathrm{meet}\left(k\right)=\underset{\dot{}}{\wedge }$$
10	9	sbceq1d	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{\wedge }/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right)$$
11	7 10	sbceqbid	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{\vee }/j\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{\wedge }/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right)$$
12	5 11	sbceqbid	$$⊢k=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_k/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{\vee }/j\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{\wedge }/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right)$$
13	1	fvexi	$$⊢B\in \mathrm{V}$$
14	2	fvexi	$$⊢\underset{\dot{}}{\vee }\in \mathrm{V}$$
15	3	fvexi	$$⊢\underset{\dot{}}{\wedge }\in \mathrm{V}$$
16		raleq	$$⊢b=B\to \left(\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall z\in Bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right)$$
17	16	raleqbi1dv	$$⊢b=B\to \left(\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall y\in B\forall z\in Bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right)$$
18	17	raleqbi1dv	$$⊢b=B\to \left(\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in Bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right)$$
19		simpr	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to m=\underset{\dot{}}{\wedge }$$
20		eqidd	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to x=x$$
21		simpl	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to j=\underset{\dot{}}{\vee }$$
22	21	oveqd	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to yjz=y\underset{\dot{}}{\vee }z$$
23	19 20 22	oveq123d	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to xm\left(yjz\right)=x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)$$
24	19	oveqd	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to xmy=x\underset{\dot{}}{\wedge }y$$
25	19	oveqd	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to xmz=x\underset{\dot{}}{\wedge }z$$
26	21 24 25	oveq123d	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to \left(xmy\right)j\left(xmz\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)$$
27	23 26	eqeq12d	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to \left(xm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)\right)$$
28	27	ralbidv	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to \left(\forall z\in Bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall z\in Bx\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)\right)$$
29	28	2ralbidv	$$⊢\left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to \left(\forall x\in B\forall y\in B\forall z\in Bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)\right)$$
30	18 29	sylan9bb	$$⊢\left(b=B\wedge \left(j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\right)\to \left(\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)\right)$$
31	30	3impb	$$⊢\left(b=B\wedge j=\underset{\dot{}}{\vee }\wedge m=\underset{\dot{}}{\wedge }\right)\to \left(\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)\right)$$
32	13 14 15 31	sbc3ie	$$⊢\underset{\dot{}}{[}B/b\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{\vee }/j\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{\wedge }/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)$$
33	12 32	syl6bb	$$⊢k=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_k/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\leftrightarrow \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)\right)$$
34		df-dlat	$$⊢\mathrm{DLat}=\left\{k\in \mathrm{Lat}|\underset{\dot{}}{[}{\mathrm{Base}}_k/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{join}\left(k\right)/j\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{meet}\left(k\right)/m\underset{\dot{}}{]}\forall x\in b\forall y\in b\forall z\in bxm\left(yjz\right)=\left(xmy\right)j\left(xmz\right)\right\}$$
35	33 34	elrab2	$$⊢K\in \mathrm{DLat}\leftrightarrow \left(K\in \mathrm{Lat}\wedge \forall x\in B\forall y\in B\forall z\in Bx\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)\right)$$