Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ufd Structured version   Visualization version   GIF version

Definition df-ufd 32314
Description: Define the class of unique factorization domains. A unique factorization domain (UFD for short), is a commutative ring with an absolute value (from abvtriv 20343 this is equivalent to being a domain) such that every prime ideal contains a prime element (this is a characterization due to Irving Kaplansky). A UFD is sometimes also called a "factorial ring" following the terminology of Bourbaki. (Contributed by Mario Carneiro, 17-Feb-2015.)
Assertion
Ref Expression
df-ufd UFD = {๐‘Ÿ โˆˆ CRing โˆฃ ((AbsValโ€˜๐‘Ÿ) โ‰  โˆ… โˆง โˆ€๐‘– โˆˆ (PrmIdealโ€˜๐‘Ÿ)(๐‘– โˆฉ (RPrimeโ€˜๐‘Ÿ)) โ‰  โˆ…)}
Distinct variable group:   ๐‘–,๐‘Ÿ

Detailed syntax breakdown of Definition df-ufd
StepHypRef Expression
1 cufd 32313 . 2 class UFD
2 vr . . . . . . 7 setvar ๐‘Ÿ
32cv 1541 . . . . . 6 class ๐‘Ÿ
4 cabv 20318 . . . . . 6 class AbsVal
53, 4cfv 6500 . . . . 5 class (AbsValโ€˜๐‘Ÿ)
6 c0 4286 . . . . 5 class โˆ…
75, 6wne 2940 . . . 4 wff (AbsValโ€˜๐‘Ÿ) โ‰  โˆ…
8 vi . . . . . . . 8 setvar ๐‘–
98cv 1541 . . . . . . 7 class ๐‘–
10 crpm 20151 . . . . . . . 8 class RPrime
113, 10cfv 6500 . . . . . . 7 class (RPrimeโ€˜๐‘Ÿ)
129, 11cin 3913 . . . . . 6 class (๐‘– โˆฉ (RPrimeโ€˜๐‘Ÿ))
1312, 6wne 2940 . . . . 5 wff (๐‘– โˆฉ (RPrimeโ€˜๐‘Ÿ)) โ‰  โˆ…
14 cprmidl 32262 . . . . . 6 class PrmIdeal
153, 14cfv 6500 . . . . 5 class (PrmIdealโ€˜๐‘Ÿ)
1613, 8, 15wral 3061 . . . 4 wff โˆ€๐‘– โˆˆ (PrmIdealโ€˜๐‘Ÿ)(๐‘– โˆฉ (RPrimeโ€˜๐‘Ÿ)) โ‰  โˆ…
177, 16wa 397 . . 3 wff ((AbsValโ€˜๐‘Ÿ) โ‰  โˆ… โˆง โˆ€๐‘– โˆˆ (PrmIdealโ€˜๐‘Ÿ)(๐‘– โˆฉ (RPrimeโ€˜๐‘Ÿ)) โ‰  โˆ…)
18 ccrg 19973 . . 3 class CRing
1917, 2, 18crab 3406 . 2 class {๐‘Ÿ โˆˆ CRing โˆฃ ((AbsValโ€˜๐‘Ÿ) โ‰  โˆ… โˆง โˆ€๐‘– โˆˆ (PrmIdealโ€˜๐‘Ÿ)(๐‘– โˆฉ (RPrimeโ€˜๐‘Ÿ)) โ‰  โˆ…)}
201, 19wceq 1542 1 wff UFD = {๐‘Ÿ โˆˆ CRing โˆฃ ((AbsValโ€˜๐‘Ÿ) โ‰  โˆ… โˆง โˆ€๐‘– โˆˆ (PrmIdealโ€˜๐‘Ÿ)(๐‘– โˆฉ (RPrimeโ€˜๐‘Ÿ)) โ‰  โˆ…)}
Colors of variables: wff setvar class
This definition is referenced by:  isufd  32315
  Copyright terms: Public domain W3C validator