Metamath Proof Explorer

Theorem latm12

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

Ref Expression
Hypotheses olmass.b ⊢ B = Base K
olmass.m ⊢ ∧ ˙ = meet ⁡ K
Assertion latm12 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = Y ∧ ˙ X ∧ ˙ 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 simpr1 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
6 simpr2 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
7 1 2 latmcom ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y = Y ∧ ˙ X
8 4 5 6 7 syl3anc ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y = Y ∧ ˙ X
9 8 oveq1d ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = Y ∧ ˙ X ∧ ˙ Z
10 1 2 latmassOLD ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = X ∧ ˙ Y ∧ ˙ Z
11 simpr3 ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
12 6 5 11 3jca ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B ∧ X ∈ B ∧ Z ∈ B
13 1 2 latmassOLD ⊢ K ∈ OL ∧ Y ∈ B ∧ X ∈ B ∧ Z ∈ B → Y ∧ ˙ X ∧ ˙ Z = Y ∧ ˙ X ∧ ˙ Z
14 12 13 syldan ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∧ ˙ X ∧ ˙ Z = Y ∧ ˙ X ∧ ˙ Z
15 9 10 14 3eqtr3d ⊢ K ∈ OL ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∧ ˙ Y ∧ ˙ Z = Y ∧ ˙ X ∧ ˙ Z