Proof of Theorem idlsrgmulr
Step | Hyp | Ref
| Expression |
1 | | idlsrgmulr.2 |
. . . . 5
⊢ 𝐵 = (LIdeal‘𝑅) |
2 | 1 | fvexi 6665 |
. . . 4
⊢ 𝐵 ∈ V |
3 | 2, 2 | mpoex 7775 |
. . 3
⊢ (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) ∈ V |
4 | | eqid 2759 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(LSSum‘𝑅)〉,
〈(.r‘ndx), (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉}) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉}) |
5 | 4 | idlsrgstr 31153 |
. . . 4
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(LSSum‘𝑅)〉,
〈(.r‘ndx), (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉}) Struct 〈1, ;10〉 |
6 | | mulrid 16659 |
. . . 4
⊢
.r = Slot (.r‘ndx) |
7 | | snsstp3 4701 |
. . . . 5
⊢
{〈(.r‘ndx), (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ⊆ {〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} |
8 | | ssun1 4073 |
. . . . 5
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(LSSum‘𝑅)〉,
〈(.r‘ndx), (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ⊆ ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉}) |
9 | 7, 8 | sstri 3897 |
. . . 4
⊢
{〈(.r‘ndx), (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ⊆ ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉}) |
10 | 5, 6, 9 | strfv 16574 |
. . 3
⊢ ((𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) ∈ V → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(LSSum‘𝑅)〉,
〈(.r‘ndx), (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉}))) |
11 | 3, 10 | ax-mp 5 |
. 2
⊢ (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(LSSum‘𝑅)〉,
〈(.r‘ndx), (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉})) |
12 | | idlsrgmulr.1 |
. . . 4
⊢ 𝑆 = (IDLsrg‘𝑅) |
13 | | eqid 2759 |
. . . . 5
⊢
(LSSum‘𝑅) =
(LSSum‘𝑅) |
14 | | idlsrgmulr.3 |
. . . . 5
⊢ 𝐺 = (mulGrp‘𝑅) |
15 | | idlsrgmulr.4 |
. . . . 5
⊢ ⊗ =
(LSSum‘𝐺) |
16 | 1, 13, 14, 15 | idlsrgval 31154 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (IDLsrg‘𝑅) = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉})) |
17 | 12, 16 | syl5eq 2806 |
. . 3
⊢ (𝑅 ∈ 𝑉 → 𝑆 = ({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉})) |
18 | 17 | fveq2d 6655 |
. 2
⊢ (𝑅 ∈ 𝑉 → (.r‘𝑆) =
(.r‘({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(LSSum‘𝑅)〉,
〈(.r‘ndx), (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐵 ↦ {𝑗 ∈ 𝐵 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐵 ∧ 𝑖 ⊆ 𝑗)}〉}))) |
19 | 11, 18 | eqtr4id 2813 |
1
⊢ (𝑅 ∈ 𝑉 → (𝑖 ∈ 𝐵, 𝑗 ∈ 𝐵 ↦ ((RSpan‘𝑅)‘(𝑖 ⊗ 𝑗))) = (.r‘𝑆)) |