Theorem dlatjmdi

Description: In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	dlatjmdi.b	$$⊢B={\mathrm{Base}}_K$$
	dlatjmdi.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dlatjmdi.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
Assertion	dlatjmdi	$$⊢\left(K\in \mathrm{DLat}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to X\underset{\dot{}}{\vee }\left(Y\underset{\dot{}}{\wedge }Z\right)=\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\wedge }\left(X\underset{\dot{}}{\vee }Z\right)$$

Proof

Step	Hyp	Ref	Expression
1		dlatjmdi.b	$$⊢B={\mathrm{Base}}_K$$
2		dlatjmdi.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dlatjmdi.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		eqid	$$⊢\mathrm{ODual}\left(K\right)=\mathrm{ODual}\left(K\right)$$
5	4	odudlatb	$$⊢K\in \mathrm{DLat}\to \left(K\in \mathrm{DLat}\leftrightarrow \mathrm{ODual}\left(K\right)\in \mathrm{DLat}\right)$$
6	5	ibi	$$⊢K\in \mathrm{DLat}\to \mathrm{ODual}\left(K\right)\in \mathrm{DLat}$$
7	4 1	odubas	$$⊢B={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
8	4 3	odujoin	$$⊢\underset{\dot{}}{\wedge }=\mathrm{join}\left(\mathrm{ODual}\left(K\right)\right)$$
9	4 2	odumeet	$$⊢\underset{\dot{}}{\vee }=\mathrm{meet}\left(\mathrm{ODual}\left(K\right)\right)$$
10	7 8 9	dlatmjdi	$$⊢\left(\mathrm{ODual}\left(K\right)\in \mathrm{DLat}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to X\underset{\dot{}}{\vee }\left(Y\underset{\dot{}}{\wedge }Z\right)=\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\wedge }\left(X\underset{\dot{}}{\vee }Z\right)$$
11	6 10	sylan	$$⊢\left(K\in \mathrm{DLat}\wedge \left(X\in B\wedge Y\in B\wedge Z\in B\right)\right)\to X\underset{\dot{}}{\vee }\left(Y\underset{\dot{}}{\wedge }Z\right)=\left(X\underset{\dot{}}{\vee }Y\right)\underset{\dot{}}{\wedge }\left(X\underset{\dot{}}{\vee }Z\right)$$