Metamath Proof Explorer


Theorem latmidm

Description: Lattice meet is idempotent. Analogue of inidm . (Contributed by NM, 8-Nov-2011)

Ref Expression
Hypotheses latmidm.b B = Base K
latmidm.m ˙ = meet K
Assertion latmidm K Lat X B X ˙ X = X

Proof

Step Hyp Ref Expression
1 latmidm.b B = Base K
2 latmidm.m ˙ = meet K
3 eqid K = K
4 simpl K Lat X B K Lat
5 1 2 latmcl K Lat X B X B X ˙ X B
6 5 3anidm23 K Lat X B X ˙ X B
7 simpr K Lat X B X B
8 1 3 2 latmle1 K Lat X B X B X ˙ X K X
9 8 3anidm23 K Lat X B X ˙ X K X
10 1 3 latref K Lat X B X K X
11 1 3 2 latlem12 K Lat X B X B X B X K X X K X X K X ˙ X
12 4 7 7 7 11 syl13anc K Lat X B X K X X K X X K X ˙ X
13 10 10 12 mpbi2and K Lat X B X K X ˙ X
14 1 3 4 6 7 9 13 latasymd K Lat X B X ˙ X = X