Definition df-ldil 35390

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

Assertion

Ref	Expression
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 ) } ) )

Distinct variable group:   w, k, f, x

Detailed syntax breakdown of Definition df-ldil

Step	Hyp	Ref	Expression
1		cldil 35386	. 2 class LDil
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vw	. . . 4 setvar w
5	2	cv 1482	. . . . 5 class k
6		clh 35270	. . . . 5 class LHyp
7	5, 6	cfv 5888	. . . 4 class ( LHyp ` k )
8		vx	. . . . . . . . 9 setvar x
9	8	cv 1482	. . . . . . . 8 class x
10	4	cv 1482	. . . . . . . 8 class w
11		cple 15948	. . . . . . . . 9 class le
12	5, 11	cfv 5888	. . . . . . . 8 class ( le ` k )
13	9, 10, 12	wbr 4653	. . . . . . 7 wff x ( le ` k ) w
14		vf	. . . . . . . . . 10 setvar f
15	14	cv 1482	. . . . . . . . 9 class f
16	9, 15	cfv 5888	. . . . . . . 8 class ( f ` x )
17	16, 9	wceq 1483	. . . . . . 7 wff ( f ` x ) = x
18	13, 17	wi 4	. . . . . 6 wff ( x ( le ` k ) w -> ( f ` x ) = x )
19		cbs 15857	. . . . . . 7 class Base
20	5, 19	cfv 5888	. . . . . 6 class ( Base ` k )
21	18, 8, 20	wral 2912	. . . . 5 wff A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x )
22		claut 35271	. . . . . 6 class LAut
23	5, 22	cfv 5888	. . . . 5 class ( LAut ` k )
24	21, 14, 23	crab 2916	. . . 4 class { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) }
25	4, 7, 24	cmpt 4729	. . 3 class ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } )
26	2, 3, 25	cmpt 4729	. 2 class ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } ) )
27	1, 26	wceq 1483	1 wff LDil = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } ) )

This definition is referenced by:  ldilfset  35394