# Metamath Proof Explorer

## 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
isdlat.m
Assertion isdlat

### Proof

Step Hyp Ref Expression
1 isdlat.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 isdlat.j
3 isdlat.m
4 fveq2 ${⊢}{k}={K}\to {\mathrm{Base}}_{{k}}={\mathrm{Base}}_{{K}}$
5 4 1 syl6eqr ${⊢}{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 syl6eqr
8 fveq2 ${⊢}{k}={K}\to \mathrm{meet}\left({k}\right)=\mathrm{meet}\left({K}\right)$
9 8 3 syl6eqr
10 9 sbceq1d
11 7 10 sbceqbid
12 5 11 sbceqbid
13 1 fvexi ${⊢}{B}\in \mathrm{V}$
14 2 fvexi
15 3 fvexi
16 raleq ${⊢}{b}={B}\to \left(\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)\right)$
17 16 raleqbi1dv ${⊢}{b}={B}\to \left(\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)↔\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)\right)$
18 17 raleqbi1dv ${⊢}{b}={B}\to \left(\forall {x}\in {b}\phantom{\rule{.4em}{0ex}}\forall {y}\in {b}\phantom{\rule{.4em}{0ex}}\forall {z}\in {b}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}{x}{m}\left({y}{j}{z}\right)=\left({x}{m}{y}\right){j}\left({x}{m}{z}\right)\right)$
19 simpr
20 eqidd
21 simpl
22 21 oveqd
23 19 20 22 oveq123d
24 19 oveqd
25 19 oveqd
26 21 24 25 oveq123d
27 23 26 eqeq12d
28 27 ralbidv
29 28 2ralbidv
30 18 29 sylan9bb
31 30 3impb
32 13 14 15 31 sbc3ie
33 12 32 syl6bb
34 df-dlat
35 33 34 elrab2