This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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