Metamath Proof Explorer

Theorem ltrncnvleN

Description: Less-than or equal property of lattice translation converse. (Contributed by NM, 10-May-2013) (New usage is discouraged.)

Ref Expression
Hypotheses ltrnle.b ⊢ B = Base K
ltrnle.l ⊢ ≤ ˙ = ≤ K
ltrnle.h ⊢ H = LHyp ⁡ K
ltrnle.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrncnvleN ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F -1 ⁡ X ≤ ˙ F -1 ⁡ 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 simp3 ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X ∈ B ∧ Y ∈ B
10 1 2 6 lautcnvle ⊢ K ∈ V ∧ F ∈ LAut ⁡ K ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F -1 ⁡ X ≤ ˙ F -1 ⁡ Y
11 5 8 9 10 syl21anc ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X ≤ ˙ Y ↔ F -1 ⁡ X ≤ ˙ F -1 ⁡ Y