Theorem latdisdlem

Description: Lemma for latdisd . (Contributed by Stefan O'Rear, 30-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	latdisdlem	$$⊢K\in \mathrm{Lat}\to \left(\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\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)\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 3	latmcl	$$⊢\left(K\in \mathrm{Lat}\wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{\wedge }y\in B$$
5	4	3adant3r3	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\underset{\dot{}}{\wedge }y\in B$$
6		simpr1	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\in B$$
7		simpr3	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to z\in B$$
8		oveq1	$$⊢u=x\underset{\dot{}}{\wedge }y\to u\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)$$
9		oveq1	$$⊢u=x\underset{\dot{}}{\wedge }y\to u\underset{\dot{}}{\vee }v=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }v$$
10		oveq1	$$⊢u=x\underset{\dot{}}{\wedge }y\to u\underset{\dot{}}{\vee }w=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w$$
11	9 10	oveq12d	$$⊢u=x\underset{\dot{}}{\wedge }y\to \left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w\right)$$
12	8 11	eqeq12d	$$⊢u=x\underset{\dot{}}{\wedge }y\to \left(u\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\leftrightarrow \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w\right)\right)$$
13		oveq1	$$⊢v=x\to v\underset{\dot{}}{\wedge }w=x\underset{\dot{}}{\wedge }w$$
14	13	oveq2d	$$⊢v=x\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)$$
15		oveq2	$$⊢v=x\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }v=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x$$
16	15	oveq1d	$$⊢v=x\to \left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w\right)$$
17	14 16	eqeq12d	$$⊢v=x\to \left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w\right)\leftrightarrow \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w\right)\right)$$
18		oveq2	$$⊢w=z\to x\underset{\dot{}}{\wedge }w=x\underset{\dot{}}{\wedge }z$$
19	18	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)$$
20		oveq2	$$⊢w=z\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w=\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z$$
21	20	oveq2d	$$⊢w=z\to \left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z\right)$$
22	19 21	eqeq12d	$$⊢w=z\to \left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }w\right)\leftrightarrow \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z\right)\right)$$
23	12 17 22	rspc3v	$$⊢\left(x\underset{\dot{}}{\wedge }y\in B\wedge x\in B\wedge z\in B\right)\to \left(\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z\right)\right)$$
24	5 6 7 23	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z\right)\right)$$
25	24	imp	$$⊢\left(\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\right)\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }z\right)=\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z\right)$$
26		simpl	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to K\in \mathrm{Lat}$$
27	1 2	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge x\underset{\dot{}}{\wedge }y\in B\wedge x\in B\right)\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x=x\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)$$
28	26 5 6 27	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x=x\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)$$
29	1 2 3	latabs1	$$⊢\left(K\in \mathrm{Lat}\wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)=x$$
30	29	3adant3r3	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)=x$$
31	28 30	eqtrd	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x=x$$
32	1 2	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge x\underset{\dot{}}{\wedge }y\in B\wedge z\in B\right)\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z=z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)$$
33	26 5 7 32	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z=z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)$$
34	31 33	oveq12d	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z\right)=x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)\right)$$
35	34	adantr	$$⊢\left(\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\right)\to \left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(\left(x\underset{\dot{}}{\wedge }y\right)\underset{\dot{}}{\vee }z\right)=x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)\right)$$
36		simpr2	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to y\in B$$
37		oveq1	$$⊢u=z\to u\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=z\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)$$
38		oveq1	$$⊢u=z\to u\underset{\dot{}}{\vee }v=z\underset{\dot{}}{\vee }v$$
39		oveq1	$$⊢u=z\to u\underset{\dot{}}{\vee }w=z\underset{\dot{}}{\vee }w$$
40	38 39	oveq12d	$$⊢u=z\to \left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)=\left(z\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }w\right)$$
41	37 40	eqeq12d	$$⊢u=z\to \left(u\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\leftrightarrow z\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(z\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }w\right)\right)$$
42	13	oveq2d	$$⊢v=x\to z\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)$$
43		oveq2	$$⊢v=x\to z\underset{\dot{}}{\vee }v=z\underset{\dot{}}{\vee }x$$
44	43	oveq1d	$$⊢v=x\to \left(z\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }w\right)=\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }w\right)$$
45	42 44	eqeq12d	$$⊢v=x\to \left(z\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(z\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }w\right)\leftrightarrow z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }w\right)\right)$$
46		oveq2	$$⊢w=y\to x\underset{\dot{}}{\wedge }w=x\underset{\dot{}}{\wedge }y$$
47	46	oveq2d	$$⊢w=y\to z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)$$
48		oveq2	$$⊢w=y\to z\underset{\dot{}}{\vee }w=z\underset{\dot{}}{\vee }y$$
49	48	oveq2d	$$⊢w=y\to \left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }w\right)=\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)$$
50	47 49	eqeq12d	$$⊢w=y\to \left(z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }w\right)=\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }w\right)\leftrightarrow z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)=\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)\right)$$
51	41 45 50	rspc3v	$$⊢\left(z\in B\wedge x\in B\wedge y\in B\right)\to \left(\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\to z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)=\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)\right)$$
52	7 6 36 51	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\to z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)=\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)\right)$$
53	52	imp	$$⊢\left(\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\right)\to z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)=\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)$$
54	53	oveq2d	$$⊢\left(\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\right)\to x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)\right)=x\underset{\dot{}}{\wedge }\left(\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)\right)$$
55	1 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge z\in B\wedge x\in B\right)\to z\underset{\dot{}}{\vee }x\in B$$
56	26 7 6 55	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to z\underset{\dot{}}{\vee }x\in B$$
57	1 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge z\in B\wedge y\in B\right)\to z\underset{\dot{}}{\vee }y\in B$$
58	26 7 36 57	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to z\underset{\dot{}}{\vee }y\in B$$
59	1 3	latmass	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge z\underset{\dot{}}{\vee }x\in B\wedge z\underset{\dot{}}{\vee }y\in B\right)\right)\to \left(x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }x\right)\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)=x\underset{\dot{}}{\wedge }\left(\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)\right)$$
60	26 6 56 58 59	syl13anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }x\right)\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)=x\underset{\dot{}}{\wedge }\left(\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)\right)$$
61	1 2	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge z\in B\wedge x\in B\right)\to z\underset{\dot{}}{\vee }x=x\underset{\dot{}}{\vee }z$$
62	26 7 6 61	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to z\underset{\dot{}}{\vee }x=x\underset{\dot{}}{\vee }z$$
63	62	oveq2d	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }x\right)=x\underset{\dot{}}{\wedge }\left(x\underset{\dot{}}{\vee }z\right)$$
64	1 2 3	latabs2	$$⊢\left(K\in \mathrm{Lat}\wedge x\in B\wedge z\in B\right)\to x\underset{\dot{}}{\wedge }\left(x\underset{\dot{}}{\vee }z\right)=x$$
65	26 6 7 64	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\underset{\dot{}}{\wedge }\left(x\underset{\dot{}}{\vee }z\right)=x$$
66	63 65	eqtrd	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }x\right)=x$$
67	1 2	latjcom	$$⊢\left(K\in \mathrm{Lat}\wedge z\in B\wedge y\in B\right)\to z\underset{\dot{}}{\vee }y=y\underset{\dot{}}{\vee }z$$
68	26 7 36 67	syl3anc	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to z\underset{\dot{}}{\vee }y=y\underset{\dot{}}{\vee }z$$
69	66 68	oveq12d	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to \left(x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }x\right)\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)=x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)$$
70	60 69	eqtr3d	$$⊢\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\to x\underset{\dot{}}{\wedge }\left(\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)\right)=x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)$$
71	70	adantr	$$⊢\left(\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\right)\to x\underset{\dot{}}{\wedge }\left(\left(z\underset{\dot{}}{\vee }x\right)\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }y\right)\right)=x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)$$
72	54 71	eqtrd	$$⊢\left(\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\right)\to x\underset{\dot{}}{\wedge }\left(z\underset{\dot{}}{\vee }\left(x\underset{\dot{}}{\wedge }y\right)\right)=x\underset{\dot{}}{\wedge }\left(y\underset{\dot{}}{\vee }z\right)$$
73	25 35 72	3eqtrrd	$$⊢\left(\left(K\in \mathrm{Lat}\wedge \left(x\in B\wedge y\in B\wedge z\in B\right)\right)\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\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)$$
74	73	an32s	$$⊢\left(\left(K\in \mathrm{Lat}\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\right)\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)$$
75	74	ralrimivvva	$$⊢\left(K\in \mathrm{Lat}\wedge \forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\right)\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)$$
76	75	ex	$$⊢K\in \mathrm{Lat}\to \left(\forall u\in B\forall v\in B\forall w\in Bu\underset{\dot{}}{\vee }\left(v\underset{\dot{}}{\wedge }w\right)=\left(u\underset{\dot{}}{\vee }v\right)\underset{\dot{}}{\wedge }\left(u\underset{\dot{}}{\vee }w\right)\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)\right)$$