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 = (
	ltrncvr.h	|- H = ( LHyp ` K )
	ltrncvr.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	ltrncvr	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( X C Y <-> ( F ` X ) C ( F ` Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltrncvr.b	|- B = ( Base ` K )
2		ltrncvr.c	|- C = (
3		ltrncvr.h	|- H = ( LHyp ` K )
4		ltrncvr.t	|- T = ( ( LTrn ` K ) ` W )
5		simp1l	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> K e. V )
6		eqid	|- ( LAut ` K ) = ( LAut ` K )
7	3 6 4	ltrnlaut	|- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. ( LAut ` K ) )
8	7	3adant3	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> F e. ( LAut ` K ) )
9		simp3l	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> X e. B )
10		simp3r	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
11	1 2 6	lautcvr	|- ( ( K e. V /\ ( F e. ( LAut ` K ) /\ X e. B /\ Y e. B ) ) -> ( X C Y <-> ( F ` X ) C ( F ` Y ) ) )
12	5 8 9 10 11	syl13anc	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( X C Y <-> ( F ` X ) C ( F ` Y ) ) )