Theorem dlatmjdi

Description: In a distributive lattice, meets distribute over joins. (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	dlatmjdi	$$⊢\left(K\in \mathrm{DLat}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to 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)$$

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	1 2 3	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)$$
5	4	simprbi	$$⊢K\in \mathrm{DLat}\to \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)$$
6		oveq1	$$⊢x=X\to x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=X\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)$$
7		oveq1	$$⊢x=X\to x\underset{\dot{}}{\wedge }y=X\underset{\dot{}}{\wedge }y$$
8		oveq1	$$⊢x=X\to x\underset{\dot{}}{\wedge }z=X\underset{\dot{}}{\wedge }z$$
9	7 8	oveq12d	$$⊢x=X\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)=\left(X\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }z\right)$$
10	6 9	eqeq12d	$$⊢x=X\to \left(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)\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)$$
11		oveq1	$$⊢y=Y\to y\underset{\dot{}}{\vee }z=Y\underset{\dot{}}{\vee }z$$
12	11	oveq2d	$$⊢y=Y\to X\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)=X\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }z\right)$$
13		oveq2	$$⊢y=Y\to X\underset{\dot{}}{\wedge }y=X\underset{\dot{}}{\wedge }Y$$
14	13	oveq1d	$$⊢y=Y\to \left(X\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }z\right)=\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }z\right)$$
15	12 14	eqeq12d	$$⊢y=Y\to \left(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)\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)$$
16		oveq2	$$⊢z=Z\to Y\underset{\dot{}}{\vee }z=Y\underset{\dot{}}{\vee }Z$$
17	16	oveq2d	$$⊢z=Z\to X\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }z\right)=X\underset{\dot{}}{\wedge }\left(Y\underset{\dot{}}{\vee }Z\right)$$
18		oveq2	$$⊢z=Z\to X\underset{\dot{}}{\wedge }z=X\underset{\dot{}}{\wedge }Z$$
19	18	oveq2d	$$⊢z=Z\to \left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }z\right)=\left(X\underset{\dot{}}{\wedge }Y\right)\underset{\dot{}}{\vee }\left(X\underset{\dot{}}{\wedge }Z\right)$$
20	17 19	eqeq12d	$$⊢z=Z\to \left(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)\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)$$
21	10 15 20	rspc3v	$$⊢\left(X\in B\wedge Y\in B\wedge Z\in B\right)\to \left(\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)\to 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)$$
22	5 21	mpan9	$$⊢\left(K\in \mathrm{DLat}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to 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)$$