Metamath Proof Explorer


Theorem latmmdir

Description: Lattice meet distributes over itself. ( inindir analog.) (Contributed by NM, 6-Jun-2012)

Ref Expression
Hypotheses olmass.b B = Base K
olmass.m ˙ = meet K
Assertion latmmdir K OL X B Y B Z B X ˙ Y ˙ Z = X ˙ Z ˙ Y ˙ Z

Proof

Step Hyp Ref Expression
1 olmass.b B = Base K
2 olmass.m ˙ = meet K
3 ollat K OL K Lat
4 3 adantr K OL X B Y B Z B K Lat
5 simpr3 K OL X B Y B Z B Z B
6 1 2 latmidm K Lat Z B Z ˙ Z = Z
7 4 5 6 syl2anc K OL X B Y B Z B Z ˙ Z = Z
8 7 oveq2d K OL X B Y B Z B X ˙ Y ˙ Z ˙ Z = X ˙ Y ˙ Z
9 simpl K OL X B Y B Z B K OL
10 simpr1 K OL X B Y B Z B X B
11 simpr2 K OL X B Y B Z B Y B
12 1 2 latm4 K OL X B Y B Z B Z B X ˙ Y ˙ Z ˙ Z = X ˙ Z ˙ Y ˙ Z
13 9 10 11 5 5 12 syl122anc K OL X B Y B Z B X ˙ Y ˙ Z ˙ Z = X ˙ Z ˙ Y ˙ Z
14 8 13 eqtr3d K OL X B Y B Z B X ˙ Y ˙ Z = X ˙ Z ˙ Y ˙ Z