Metamath Proof Explorer

Theorem ltrncvr

Description: Covering property of a lattice translation. (Contributed by NM, 20-May-2012)

Ref Expression
Hypotheses ltrncvr.b ⊢ B = Base K
ltrncvr.c ⊢ C = ⋖ K
ltrncvr.h ⊢ H = LHyp ⁡ K
ltrncvr.t ⊢ T = LTrn ⁡ K ⁡ W
Assertion ltrncvr ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ F ⁡ X C F ⁡ Y

Proof

Step Hyp Ref Expression
1 ltrncvr.b ⊢ B = Base K
2 ltrncvr.c ⊢ C = ⋖ K
3 ltrncvr.h ⊢ H = LHyp ⁡ K
4 ltrncvr.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 lautcvr ⊢ K ∈ V ∧ F ∈ LAut ⁡ K ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ F ⁡ X C F ⁡ Y
12 5 8 9 10 11 syl13anc ⊢ K ∈ V ∧ W ∈ H ∧ F ∈ T ∧ X ∈ B ∧ Y ∈ B → X C Y ↔ F ⁡ X C F ⁡ Y