# Metamath Proof Explorer

## Theorem latmmdiN

Description: Lattice meet distributes over itself. ( inindi analog.) (Contributed by NM, 8-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses olmass.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
olmass.m
Assertion latmmdiN

### Proof

Step Hyp Ref Expression
1 olmass.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 olmass.m
3 ollat ${⊢}{K}\in \mathrm{OL}\to {K}\in \mathrm{Lat}$
4 3 adantr ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{Lat}$
5 simpr1 ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {B}$
6 1 2 latmidm
7 4 5 6 syl2anc
8 7 oveq1d
9 simpl ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {K}\in \mathrm{OL}$
10 simpr2 ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {B}$
11 simpr3 ${⊢}\left({K}\in \mathrm{OL}\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {B}$
12 1 2 latm4
13 9 5 5 10 11 12 syl122anc
14 8 13 eqtr3d