Metamath Proof Explorer

Theorem ltrnj

Description: Lattice translation of a meet. TODO: change antecedent to K e. HL (Contributed by NM, 25-May-2012)

Ref Expression
Hypotheses ltrnj.b ⊢ B = Base K
ltrnj.j ⊢ ∨ ˙ = join ⁡ K
ltrnj.h ⊢ H = LHyp ⁡ K
ltrnj.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrnj ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → F ⁡ X ∨ ˙ Y = F ⁡ X ∨ ˙ F ⁡ Y

Proof

Step Hyp Ref Expression
1 ltrnj.b ⊢ B = Base K
2 ltrnj.j ⊢ ∨ ˙ = join ⁡ K
3 ltrnj.h ⊢ H = LHyp ⁡ K
4 ltrnj.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 lautj ⊢ 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