Metamath Proof Explorer

Theorem ltrnm

Description: Lattice translation of a meet. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrnm.b ⊢ B = Base K
ltrnm.m ⊢ ∧ ˙ = meet ⁡ K
ltrnm.h ⊢ H = LHyp ⁡ K
ltrnm.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrnm ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → F ⁡ X ∧ ˙ Y = F ⁡ X ∧ ˙ F ⁡ Y

Proof

Step Hyp Ref Expression
1 ltrnm.b ⊢ B = Base K
2 ltrnm.m ⊢ ∧ ˙ = meet ⁡ K
3 ltrnm.h ⊢ H = LHyp ⁡ K
4 ltrnm.t ⊢ T = LTrn ⁡ K ⁡ W
5 simp1l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → K ∈ HL
6 5 hllatd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → K ∈ Lat
7 eqid ⊢ LAut ⁡ K = LAut ⁡ K
8 3 7 4 ltrnlaut ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T → F ∈ LAut ⁡ K
9 8 3adant3 ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → F ∈ LAut ⁡ K
10 simp3l ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X ∈ B
11 simp3r ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
12 1 2 7 lautm ⊢ K ∈ Lat ∧ F ∈ LAut ⁡ K ∧ X ∈ B ∧ Y ∈ B → F ⁡ X ∧ ˙ Y = F ⁡ X ∧ ˙ F ⁡ Y
13 6 9 10 11 12 syl13anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → F ⁡ X ∧ ˙ Y = F ⁡ X ∧ ˙ F ⁡ Y