Step | Hyp | Ref
| Expression |
1 | | elex 3426 |
. 2
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
2 | | fvexd 6732 |
. . . 4
⊢ (𝑟 = 𝑅 → (LIdeal‘𝑟) ∈ V) |
3 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 𝑏 = (LIdeal‘𝑟)) |
4 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 𝑟 = 𝑅) |
5 | 4 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (LIdeal‘𝑟) = (LIdeal‘𝑅)) |
6 | 3, 5 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 𝑏 = (LIdeal‘𝑅)) |
7 | | idlsrgval.1 |
. . . . . . . 8
⊢ 𝐼 = (LIdeal‘𝑅) |
8 | 6, 7 | eqtr4di 2796 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 𝑏 = 𝐼) |
9 | 8 | opeq2d 4791 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 〈(Base‘ndx), 𝑏〉 = 〈(Base‘ndx),
𝐼〉) |
10 | 4 | fveq2d 6721 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (LSSum‘𝑟) = (LSSum‘𝑅)) |
11 | | idlsrgval.2 |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝑅) |
12 | 10, 11 | eqtr4di 2796 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (LSSum‘𝑟) = ⊕ ) |
13 | 12 | opeq2d 4791 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 〈(+g‘ndx),
(LSSum‘𝑟)〉 =
〈(+g‘ndx), ⊕
〉) |
14 | 4 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (RSpan‘𝑟) = (RSpan‘𝑅)) |
15 | 4 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (mulGrp‘𝑟) = (mulGrp‘𝑅)) |
16 | | idlsrgval.3 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (mulGrp‘𝑅) |
17 | 15, 16 | eqtr4di 2796 |
. . . . . . . . . . . 12
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (mulGrp‘𝑟) = 𝐺) |
18 | 17 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (LSSum‘(mulGrp‘𝑟)) = (LSSum‘𝐺)) |
19 | | idlsrgval.4 |
. . . . . . . . . . 11
⊢ ⊗ =
(LSSum‘𝐺) |
20 | 18, 19 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (LSSum‘(mulGrp‘𝑟)) = ⊗ ) |
21 | 20 | oveqd 7230 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (𝑖(LSSum‘(mulGrp‘𝑟))𝑗) = (𝑖 ⊗ 𝑗)) |
22 | 14, 21 | fveq12d 6724 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)) = ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) |
23 | 8, 8, 22 | mpoeq123dv 7286 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))) |
24 | 23 | opeq2d 4791 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉 = 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉) |
25 | 9, 13, 24 | tpeq123d 4664 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → {〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), (LSSum‘𝑟)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} = {〈(Base‘ndx), 𝐼〉,
〈(+g‘ndx), ⊕ 〉,
〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉}) |
26 | 8 | rabeqdv 3395 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗} = {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) |
27 | 8, 26 | mpteq12dv 5140 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗}) = (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})) |
28 | 27 | rneqd 5807 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗}) = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})) |
29 | 28 | opeq2d 4791 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 〈(TopSet‘ndx), ran
(𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉 = 〈(TopSet‘ndx), ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉) |
30 | 8 | sseq2d 3933 |
. . . . . . . . 9
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → ({𝑖, 𝑗} ⊆ 𝑏 ↔ {𝑖, 𝑗} ⊆ 𝐼)) |
31 | 30 | anbi1d 633 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → (({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗) ↔ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗))) |
32 | 31 | opabbidv 5119 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)} = {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}) |
33 | 32 | opeq2d 4791 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉 = 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉) |
34 | 29, 33 | preq12d 4657 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → {〈(TopSet‘ndx), ran
(𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉} = {〈(TopSet‘ndx), ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}) |
35 | 25, 34 | uneq12d 4078 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (LIdeal‘𝑟)) → ({〈(Base‘ndx), 𝑏〉,
〈(+g‘ndx), (LSSum‘𝑟)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉}) = ({〈(Base‘ndx), 𝐼〉,
〈(+g‘ndx), ⊕ 〉,
〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉})) |
36 | 2, 35 | csbied 3849 |
. . 3
⊢ (𝑟 = 𝑅 → ⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (LSSum‘𝑟)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉}) = ({〈(Base‘ndx), 𝐼〉,
〈(+g‘ndx), ⊕ 〉,
〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉})) |
37 | | df-idlsrg 31360 |
. . 3
⊢ IDLsrg =
(𝑟 ∈ V ↦
⦋(LIdeal‘𝑟) / 𝑏⦌({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (LSSum‘𝑟)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝑏, 𝑗 ∈ 𝑏 ↦ ((RSpan‘𝑟)‘(𝑖(LSSum‘(mulGrp‘𝑟))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝑏 ↦ {𝑗 ∈ 𝑏 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝑏 ∧ 𝑖 ⊆ 𝑗)}〉})) |
38 | | tpex 7532 |
. . . 4
⊢
{〈(Base‘ndx), 𝐼〉, 〈(+g‘ndx),
⊕
〉, 〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∈ V |
39 | | prex 5325 |
. . . 4
⊢
{〈(TopSet‘ndx), ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉} ∈ V |
40 | 38, 39 | unex 7531 |
. . 3
⊢
({〈(Base‘ndx), 𝐼〉, 〈(+g‘ndx),
⊕
〉, 〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}) ∈ V |
41 | 36, 37, 40 | fvmpt 6818 |
. 2
⊢ (𝑅 ∈ V →
(IDLsrg‘𝑅) =
({〈(Base‘ndx), 𝐼〉, 〈(+g‘ndx),
⊕
〉, 〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉})) |
42 | 1, 41 | syl 17 |
1
⊢ (𝑅 ∈ 𝑉 → (IDLsrg‘𝑅) = ({〈(Base‘ndx), 𝐼〉,
〈(+g‘ndx), ⊕ 〉,
〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉})) |