Detailed syntax breakdown of Definition df-idlsrg
Step | Hyp | Ref
| Expression |
1 | | cidlsrg 31004 |
. 2
class
IDLsrg |
2 | | vr |
. . 3
setvar 𝑟 |
3 | | crg 19290 |
. . 3
class
Ring |
4 | | vb |
. . . 4
setvar 𝑏 |
5 | 2 | cv 1535 |
. . . . 5
class 𝑟 |
6 | | clidl 19935 |
. . . . 5
class
LIdeal |
7 | 5, 6 | cfv 6348 |
. . . 4
class
(LIdeal‘𝑟) |
8 | | cnx 16473 |
. . . . . . . 8
class
ndx |
9 | | cbs 16476 |
. . . . . . . 8
class
Base |
10 | 8, 9 | cfv 6348 |
. . . . . . 7
class
(Base‘ndx) |
11 | 4 | cv 1535 |
. . . . . . 7
class 𝑏 |
12 | 10, 11 | cop 4566 |
. . . . . 6
class
〈(Base‘ndx), 𝑏〉 |
13 | | cplusg 16558 |
. . . . . . . 8
class
+g |
14 | 8, 13 | cfv 6348 |
. . . . . . 7
class
(+g‘ndx) |
15 | | vi |
. . . . . . . 8
setvar 𝑖 |
16 | | vj |
. . . . . . . 8
setvar 𝑗 |
17 | | cplusf 17842 |
. . . . . . . . . 10
class
+𝑓 |
18 | 5, 17 | cfv 6348 |
. . . . . . . . 9
class
(+𝑓‘𝑟) |
19 | 15 | cv 1535 |
. . . . . . . . . 10
class 𝑖 |
20 | 16 | cv 1535 |
. . . . . . . . . 10
class 𝑗 |
21 | 19, 20 | cxp 5546 |
. . . . . . . . 9
class (𝑖 × 𝑗) |
22 | 18, 21 | cima 5551 |
. . . . . . . 8
class
((+𝑓‘𝑟) “ (𝑖 × 𝑗)) |
23 | 15, 16, 11, 11, 22 | cmpo 7151 |
. . . . . . 7
class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗))) |
24 | 14, 23 | cop 4566 |
. . . . . 6
class
〈(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))〉 |
25 | | cmulr 16559 |
. . . . . . . 8
class
.r |
26 | 8, 25 | cfv 6348 |
. . . . . . 7
class
(.r‘ndx) |
27 | | cmgp 19232 |
. . . . . . . . . . . 12
class
mulGrp |
28 | 5, 27 | cfv 6348 |
. . . . . . . . . . 11
class
(mulGrp‘𝑟) |
29 | 28, 17 | cfv 6348 |
. . . . . . . . . 10
class
(+𝑓‘(mulGrp‘𝑟)) |
30 | 29, 21 | cima 5551 |
. . . . . . . . 9
class
((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗)) |
31 | | crsp 19936 |
. . . . . . . . . 10
class
RSpan |
32 | 5, 31 | cfv 6348 |
. . . . . . . . 9
class
(RSpan‘𝑟) |
33 | 30, 32 | cfv 6348 |
. . . . . . . 8
class
((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))) |
34 | 15, 16, 11, 11, 33 | cmpo 7151 |
. . . . . . 7
class (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗)))) |
35 | 26, 34 | cop 4566 |
. . . . . 6
class
〈(.r‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))〉 |
36 | 12, 24, 35 | ctp 4564 |
. . . . 5
class
{〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))〉} |
37 | | cts 16564 |
. . . . . . . 8
class
TopSet |
38 | 8, 37 | cfv 6348 |
. . . . . . 7
class
(TopSet‘ndx) |
39 | 20, 19 | wss 3929 |
. . . . . . . . . . 11
wff 𝑗 ⊆ 𝑖 |
40 | | cprmidl 30973 |
. . . . . . . . . . . 12
class
PrmIdeal |
41 | 5, 40 | cfv 6348 |
. . . . . . . . . . 11
class
(PrmIdeal‘𝑟) |
42 | 39, 16, 41 | crab 3141 |
. . . . . . . . . 10
class {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖} |
43 | 11, 42 | cdif 3926 |
. . . . . . . . 9
class (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}) |
44 | 15, 11, 43 | cmpt 5139 |
. . . . . . . 8
class (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖})) |
45 | 44 | crn 5549 |
. . . . . . 7
class ran
(𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖})) |
46 | 38, 45 | cop 4566 |
. . . . . 6
class
〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))〉 |
47 | | cple 16565 |
. . . . . . . 8
class
le |
48 | 8, 47 | cfv 6348 |
. . . . . . 7
class
(le‘ndx) |
49 | 19, 20 | cpr 4562 |
. . . . . . . . . 10
class {𝑖, 𝑗} |
50 | 49, 11 | wss 3929 |
. . . . . . . . 9
wff {𝑖, 𝑗} ⊆ 𝑏 |
51 | 19, 20 | wss 3929 |
. . . . . . . . 9
wff 𝑖 ⊆ 𝑗 |
52 | 50, 51 | wa 398 |
. . . . . . . 8
wff ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗) |
53 | 52, 15, 16 | copab 5121 |
. . . . . . 7
class
{〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)} |
54 | 48, 53 | cop 4566 |
. . . . . 6
class
〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉 |
55 | 46, 54 | cpr 4562 |
. . . . 5
class
{〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉} |
56 | 36, 55 | cun 3927 |
. . . 4
class
({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))〉} ∪ {〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗}
⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉}) |
57 | 4, 7, 56 | csb 3876 |
. . 3
class
⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))〉} ∪ {〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗}
⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉}) |
58 | 2, 3, 57 | cmpt 5139 |
. 2
class (𝑟 ∈ Ring ↦
⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))〉} ∪ {〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗}
⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉})) |
59 | 1, 58 | wceq 1536 |
1
wff IDLsrg =
(𝑟 ∈ Ring ↦
⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((+𝑓‘𝑟) “ (𝑖 × 𝑗)))〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘((+𝑓‘(mulGrp‘𝑟)) “ (𝑖 × 𝑗))))〉} ∪ {〈(TopSet‘ndx), ran (𝑖 ∈ 𝑏 ↦ (𝑏 ∖ {𝑗 ∈ (PrmIdeal‘𝑟) ∣ 𝑗 ⊆ 𝑖}))〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗}
⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉})) |