Metamath Proof Explorer

Theorem latmidm

Description: Lattice join is idempotent. ( inidm analog.) (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