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

Metamath Proof Explorer

Definition df-dilN

Description: Define set of all dilations. Definition of dilation in Crawley p. 111. (Contributed by NM, 30-Jan-2012)

Ref Expression
Assertion df-dilN Dil = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdilN ⊢ Dil
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vd ⊢ 𝑑
4 catm ⊢ Atoms
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( Atoms ‘ 𝑘 )
7 vf ⊢ 𝑓
8 cpautN ⊢ PAut
9 5 8 cfv ⊢ ( PAut ‘ 𝑘 )
10 vx ⊢ 𝑥
11 cpsubsp ⊢ PSubSp
12 5 11 cfv ⊢ ( PSubSp ‘ 𝑘 )
13 10 cv ⊢ 𝑥
14 cwpointsN ⊢ WAtoms
15 5 14 cfv ⊢ ( WAtoms ‘ 𝑘 )
16 3 cv ⊢ 𝑑
17 16 15 cfv ⊢ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 )
18 13 17 wss ⊢ 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 )
19 7 cv ⊢ 𝑓
20 13 19 cfv ⊢ ( 𝑓 ‘ 𝑥 )
21 20 13 wceq ⊢ ( 𝑓 ‘ 𝑥 ) = 𝑥
22 18 21 wi ⊢ ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 )
23 22 10 12 wral ⊢ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 )
24 23 7 9 crab ⊢ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) }
25 3 6 24 cmpt ⊢ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } )
26 1 2 25 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )
27 0 26 wceq ⊢ Dil = ( 𝑘 ∈ V ↦ ( 𝑑 ∈ ( Atoms ‘ 𝑘 ) ↦ { 𝑓 ∈ ( PAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( PSubSp ‘ 𝑘 ) ( 𝑥 ⊆ ( ( WAtoms ‘ 𝑘 ) ‘ 𝑑 ) → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) )