Theorem latdisd

Description: In a lattice, joins distribute over meets if and only if meets distribute over joins; the distributive property is self-dual. (Contributed by Stefan O'Rear, 29-Jan-2015)

	Ref	Expression
Hypotheses	latdisd.b	$$⊢B={\mathrm{Base}}_K$$
	latdisd.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	latdisd.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
Assertion	latdisd	$$⊢K\in \mathrm{Lat}\to \left(\forall x\in B\forall y\in B\forall z\in Bx\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)\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)$$

Proof

Step	Hyp	Ref	Expression
1		latdisd.b	$$⊢B={\mathrm{Base}}_K$$
2		latdisd.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		latdisd.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4	1 2 3	latdisdlem	$$⊢K\in \mathrm{Lat}\to \left(\forall x\in B\forall y\in B\forall z\in Bx\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)\to \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=\left(u\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(u\underset{\dot{}}{\wedge }w\right)\right)$$
5		eqid	$$⊢\mathrm{ODual}\left(K\right)=\mathrm{ODual}\left(K\right)$$
6	5	odulat	$$⊢K\in \mathrm{Lat}\to \mathrm{ODual}\left(K\right)\in \mathrm{Lat}$$
7	5 1	odubas	$$⊢B={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
8	5 3	odujoin	$$⊢\underset{\dot{}}{\wedge }=\mathrm{join}\left(\mathrm{ODual}\left(K\right)\right)$$
9	5 2	odumeet	$$⊢\underset{\dot{}}{\vee }=\mathrm{meet}\left(\mathrm{ODual}\left(K\right)\right)$$
10	7 8 9	latdisdlem	$$⊢\mathrm{ODual}\left(K\right)\in \mathrm{Lat}\to \left(\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=\left(u\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(u\underset{\dot{}}{\wedge }w\right)\to \forall x\in B\forall y\in B\forall z\in Bx\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)\right)$$
11	6 10	syl	$$⊢K\in \mathrm{Lat}\to \left(\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=\left(u\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(u\underset{\dot{}}{\wedge }w\right)\to \forall x\in B\forall y\in B\forall z\in Bx\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)\right)$$
12	4 11	impbid	$$⊢K\in \mathrm{Lat}\to \left(\forall x\in B\forall y\in B\forall z\in Bx\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)\leftrightarrow \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=\left(u\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(u\underset{\dot{}}{\wedge }w\right)\right)$$
13		oveq1	$$⊢u=x\to u\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=x\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)$$
14		oveq1	$$⊢u=x\to u\underset{\dot{}}{\wedge }v=x\underset{\dot{}}{\wedge }v$$
15		oveq1	$$⊢u=x\to u\underset{\dot{}}{\wedge }w=x\underset{\dot{}}{\wedge }w$$
16	14 15	oveq12d	$$⊢u=x\to \left(u\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(u\underset{\dot{}}{\wedge }w\right)=\left(x\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)$$
17	13 16	eqeq12d	$$⊢u=x\to \left(u\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=\left(u\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(u\underset{\dot{}}{\wedge }w\right)\leftrightarrow x\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=\left(x\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)\right)$$
18		oveq1	$$⊢v=y\to v\underset{\dot{}}{\vee }w=y\underset{\dot{}}{\vee }w$$
19	18	oveq2d	$$⊢v=y\to x\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }w\right)$$
20		oveq2	$$⊢v=y\to x\underset{\dot{}}{\wedge }v=x\underset{\dot{}}{\wedge }y$$
21	20	oveq1d	$$⊢v=y\to \left(x\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)$$
22	19 21	eqeq12d	$$⊢v=y\to \left(x\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=\left(x\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)\leftrightarrow x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }w\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)\right)$$
23		oveq2	$$⊢w=z\to y\underset{\dot{}}{\vee }w=y\underset{\dot{}}{\vee }z$$
24	23	oveq2d	$$⊢w=z\to x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }w\right)=x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)$$
25		oveq2	$$⊢w=z\to x\underset{\dot{}}{\wedge }w=x\underset{\dot{}}{\wedge }z$$
26	25	oveq2d	$$⊢w=z\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)$$
27	24 26	eqeq12d	$$⊢w=z\to \left(x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }w\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\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	17 22 27	cbvral3vw	$$⊢\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\wedge }\left(v\underset{\dot{}}{\vee }w\right)=\left(u\underset{\dot{}}{\wedge }v\right)\underset{\dot{}}{\vee }\left(u\underset{\dot{}}{\wedge }w\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)$$
29	12 28	bitrdi	$$⊢K\in \mathrm{Lat}\to \left(\forall x\in B\forall y\in B\forall z\in Bx\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)\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)$$