Definition df-ldil

Description: Define set of all lattice dilations. Similar to definition of dilation in Crawley p. 111. (Contributed by NM, 11-May-2012)

	Ref	Expression
Assertion	df-ldil	|- LDil = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldil	|- LDil
1		vk	|- k
2		cvv	|- _V
3		vw	|- w
4		clh	|- LHyp
5	1	cv	|- k
6	5 4	cfv	|- ( LHyp ` k )
7		vf	|- f
8		claut	|- LAut
9	5 8	cfv	|- ( LAut ` k )
10		vx	|- x
11		cbs	|- Base
12	5 11	cfv	|- ( Base ` k )
13	10	cv	|- x
14		cple	|- le
15	5 14	cfv	|- ( le ` k )
16	3	cv	|- w
17	13 16 15	wbr	|- x ( le ` k ) w
18	7	cv	|- f
19	13 18	cfv	|- ( f ` x )
20	19 13	wceq	|- ( f ` x ) = x
21	17 20	wi	|- ( x ( le ` k ) w -> ( f ` x ) = x )
22	21 10 12	wral	|- A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x )
23	22 7 9	crab	|- { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) }
24	3 6 23	cmpt	|- ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } )
25	1 2 24	cmpt	|- ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } ) )
26	0 25	wceq	|- LDil = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } ) )