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