![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-rspec | Structured version Visualization version GIF version |
Description: Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
Ref | Expression |
---|---|
df-rspec | ⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | crspec 33297 | . 2 class Spec | |
2 | vr | . . 3 setvar 𝑟 | |
3 | crg 20123 | . . 3 class Ring | |
4 | 2 | cv 1532 | . . . . 5 class 𝑟 |
5 | cidlsrg 33045 | . . . . 5 class IDLsrg | |
6 | 4, 5 | cfv 6533 | . . . 4 class (IDLsrg‘𝑟) |
7 | cprmidl 32984 | . . . . 5 class PrmIdeal | |
8 | 4, 7 | cfv 6533 | . . . 4 class (PrmIdeal‘𝑟) |
9 | cress 17169 | . . . 4 class ↾s | |
10 | 6, 8, 9 | co 7401 | . . 3 class ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟)) |
11 | 2, 3, 10 | cmpt 5221 | . 2 class (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))) |
12 | 1, 11 | wceq 1533 | 1 wff Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))) |
Colors of variables: wff setvar class |
This definition is referenced by: rspecval 33299 |
Copyright terms: Public domain | W3C validator |