Theorem ltrncl

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

	Ref	Expression
Hypotheses	ltrn1o.b	|- B = ( Base ` K )
	ltrn1o.h	|- H = ( LHyp ` K )
	ltrn1o.t	|- T = ( ( LTrn ` K ) ` W )
Assertion	ltrncl	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ X e. B ) -> ( F ` X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		ltrn1o.b	|- B = ( Base ` K )
2		ltrn1o.h	|- H = ( LHyp ` K )
3		ltrn1o.t	|- T = ( ( LTrn ` K ) ` W )
4		simp1l	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ X e. B ) -> K e. V )
5		eqid	|- ( LAut ` K ) = ( LAut ` K )
6	2 5 3	ltrnlaut	|- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. ( LAut ` K ) )
7	6	3adant3	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ X e. B ) -> F e. ( LAut ` K ) )
8		simp3	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ X e. B ) -> X e. B )
9	1 5	lautcl	|- ( ( ( K e. V /\ F e. ( LAut ` K ) ) /\ X e. B ) -> ( F ` X ) e. B )
10	4 7 8 9	syl21anc	|- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ X e. B ) -> ( F ` X ) e. B )