Metamath Proof Explorer

Theorem ltrnle

Description: Less-than or equal property of a lattice translation. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrnle.b ⊢ B = Base K
ltrnle.l ⊢ ≤ ˙ = ≤ K
ltrnle.h ⊢ H = LHyp ⁡ K
ltrnle.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrnle ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F ⁡ X ≤ ˙ F ⁡ Y

Proof

Step Hyp Ref Expression
1 ltrnle.b ⊢ B = Base K
2 ltrnle.l ⊢ ≤ ˙ = ≤ K
3 ltrnle.h ⊢ H = LHyp ⁡ K
4 ltrnle.t ⊢ T = LTrn ⁡ K ⁡ W
5 simp1l ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → K ∈ V
6 eqid ⊢ LAut ⁡ K = LAut ⁡ K
7 3 6 4 ltrnlaut ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T → F ∈ LAut ⁡ K
8 7 3adant3 ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → F ∈ LAut ⁡ K
9 simp3l ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X ∈ B
10 simp3r ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
11 1 2 6 lautle ⊢ K ∈ V ∧ F ∈ LAut ⁡ K ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F ⁡ X ≤ ˙ F ⁡ Y
12 5 8 9 10 11 syl22anc ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F ⁡ X ≤ ˙ F ⁡ Y