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

Definition df-dilN 30840
 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 30836 . 2
2 vk . . 3
3 cvv 2948 . . 3
4 vd . . . 4
52cv 1651 . . . . 5
6 catm 29998 . . . . 5
75, 6cfv 5446 . . . 4
8 vx . . . . . . . . 9
98cv 1651 . . . . . . . 8
104cv 1651 . . . . . . . . 9
11 cwpointsN 30720 . . . . . . . . . 10
125, 11cfv 5446 . . . . . . . . 9
1310, 12cfv 5446 . . . . . . . 8
149, 13wss 3312 . . . . . . 7
15 vf . . . . . . . . . 10
1615cv 1651 . . . . . . . . 9
179, 16cfv 5446 . . . . . . . 8
1817, 9wceq 1652 . . . . . . 7
1914, 18wi 4 . . . . . 6
20 cpsubsp 30230 . . . . . . 7
215, 20cfv 5446 . . . . . 6
2219, 8, 21wral 2697 . . . . 5
23 cpautN 30721 . . . . . 6
245, 23cfv 5446 . . . . 5
2522, 15, 24crab 2701 . . . 4
264, 7, 25cmpt 4258 . . 3
272, 3, 26cmpt 4258 . 2
281, 27wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  dilfsetN  30886
 Copyright terms: Public domain W3C validator