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 = ( 𝑘 ∈ 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 ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )