Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dilN Unicode version

Definition df-dilN 28984
 Description: Define set of all dilations. Definition of dilation in [Crawley] p. 111. (Contributed by NM, 30-Jan-2012.)
Assertion
Ref Expression
df-dilN
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-dilN
StepHypRef Expression
1 cdilN 28980 . 2
2 vk . . 3
3 cvv 2727 . . 3
4 vd . . . 4
52cv 1618 . . . . 5
6 catm 28142 . . . . 5
75, 6cfv 4592 . . . 4
8 vx . . . . . . . . 9
98cv 1618 . . . . . . . 8
104cv 1618 . . . . . . . . 9
11 cwpointsN 28864 . . . . . . . . . 10
125, 11cfv 4592 . . . . . . . . 9
1310, 12cfv 4592 . . . . . . . 8
149, 13wss 3078 . . . . . . 7
15 vf . . . . . . . . . 10
1615cv 1618 . . . . . . . . 9
179, 16cfv 4592 . . . . . . . 8
1817, 9wceq 1619 . . . . . . 7
1914, 18wi 6 . . . . . 6
20 cpsubsp 28374 . . . . . . 7
215, 20cfv 4592 . . . . . 6
2219, 8, 21wral 2509 . . . . 5
23 cpautN 28865 . . . . . 6
245, 23cfv 4592 . . . . 5
2522, 15, 24crab 2512 . . . 4
264, 7, 25cmpt 3974 . . 3
272, 3, 26cmpt 3974 . 2
281, 27wceq 1619 1
 Colors of variables: wff set class This definition is referenced by:  dilfsetN  29030
 Copyright terms: Public domain W3C validator