Metamath Proof Explorer

Theorem latm32

Description: A rearrangement of lattice meet. ( in12 analog.) (Contributed by NM, 13-Nov-2012)

Ref Expression
Hypotheses olmass.b ⊢ B = Base K
olmass.m ⊢ ∧ ˙ = meet ⁡ K
Assertion latm32 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = X ∧ ˙ Z ∧ ˙ Y

Proof

Step Hyp Ref Expression
1 olmass.b ⊢ B = Base K
2 olmass.m ⊢ ∧ ˙ = meet ⁡ K
3 ollat ⊢ K ∈ OL → K ∈ Lat
4 1 2 latmcom ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Y ∧ ˙ Z = Z ∧ ˙ Y
5 3 4 syl3an1 ⊢ K ∈ OL ∧ Y ∈ B ∧ Z ∈ B → Y ∧ ˙ Z = Z ∧ ˙ Y
6 5 3adant3r1 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∧ ˙ Z = Z ∧ ˙ Y
7 6 oveq2d ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = X ∧ ˙ Z ∧ ˙ Y
8 1 2 latmassOLD ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ 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 simpr3 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
12 simpr2 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
13 1 2 latmassOLD ⊢ K ∈ OL ∧ X ∈ B ∧ Z ∈ B ∧ Y ∈ B → X ∧ ˙ Z ∧ ˙ Y = X ∧ ˙ Z ∧ ˙ Y
14 9 10 11 12 13 syl13anc ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Z ∧ ˙ Y = X ∧ ˙ Z ∧ ˙ Y
15 7 8 14 3eqtr4d ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = X ∧ ˙ Z ∧ ˙ Y