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 = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cldil	⊢ LDil
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		clh	⊢ LHyp
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( LHyp ‘ 𝑘 )
7		vf	⊢ 𝑓
8		claut	⊢ LAut
9	5 8	cfv	⊢ ( LAut ‘ 𝑘 )
10		vx	⊢ 𝑥
11		cbs	⊢ Base
12	5 11	cfv	⊢ ( Base ‘ 𝑘 )
13	10	cv	⊢ 𝑥
14		cple	⊢ le
15	5 14	cfv	⊢ ( le ‘ 𝑘 )
16	3	cv	⊢ 𝑤
17	13 16 15	wbr	⊢ 𝑥 ( le ‘ 𝑘 ) 𝑤
18	7	cv	⊢ 𝑓
19	13 18	cfv	⊢ ( 𝑓 ‘ 𝑥 )
20	19 13	wceq	⊢ ( 𝑓 ‘ 𝑥 ) = 𝑥
21	17 20	wi	⊢ ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 )
22	21 10 12	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 )
23	22 7 9	crab	⊢ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) }
24	3 6 23	cmpt	⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
25	1 2 24	cmpt	⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
26	0 25	wceq	⊢ LDil = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )