Theorem ldil1o

Description: A lattice dilation is a one-to-one onto function. (Contributed by NM, 19-Apr-2013)

	Ref	Expression
Hypotheses	ldil1o.b	|- B = ( Base ` K )
	ldil1o.h	|- H = ( LHyp ` K )
	ldil1o.d	|- D = ( ( LDil ` K ) ` W )
Assertion	ldil1o	|- ( ( ( K e. V /\ W e. H ) /\ F e. D ) -> F : B -1-1-onto-> B )

Proof

Step	Hyp	Ref	Expression
1		ldil1o.b	|- B = ( Base ` K )
2		ldil1o.h	|- H = ( LHyp ` K )
3		ldil1o.d	|- D = ( ( LDil ` K ) ` W )
4		simpll	|- ( ( ( K e. V /\ W e. H ) /\ F e. D ) -> K e. V )
5		eqid	|- ( LAut ` K ) = ( LAut ` K )
6	2 5 3	ldillaut	|- ( ( ( K e. V /\ W e. H ) /\ F e. D ) -> F e. ( LAut ` K ) )
7	1 5	laut1o	|- ( ( K e. V /\ F e. ( LAut ` K ) ) -> F : B -1-1-onto-> B )
8	4 6 7	syl2anc	|- ( ( ( K e. V /\ W e. H ) /\ F e. D ) -> F : B -1-1-onto-> B )