Proof of Theorem idlsrgtset
Step | Hyp | Ref
| Expression |
1 | | idlsrgtset.3 |
. 2
⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) |
2 | | idlsrgtset.2 |
. . . . . . 7
⊢ 𝐼 = (LIdeal‘𝑅) |
3 | 2 | fvexi 6665 |
. . . . . 6
⊢ 𝐼 ∈ V |
4 | 3 | mptex 6970 |
. . . . 5
⊢ (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ∈ V |
5 | 4 | rnex 7615 |
. . . 4
⊢ ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ∈ V |
6 | | eqid 2759 |
. . . . . 6
⊢
({〈(Base‘ndx), 𝐼〉, 〈(+g‘ndx),
(LSSum‘𝑅)〉,
〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}) = ({〈(Base‘ndx), 𝐼〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}) |
7 | 6 | idlsrgstr 31153 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐼〉, 〈(+g‘ndx),
(LSSum‘𝑅)〉,
〈(.r‘ndx), (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}) Struct 〈1, ;10〉 |
8 | | tsetid 16703 |
. . . . 5
⊢ TopSet =
Slot (TopSet‘ndx) |
9 | | snsspr1 4697 |
. . . . . 6
⊢
{〈(TopSet‘ndx), ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉} ⊆ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉} |
10 | | ssun2 4074 |
. . . . . 6
⊢
{〈(TopSet‘ndx), ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉} ⊆ ({〈(Base‘ndx),
𝐼〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}) |
11 | 9, 10 | sstri 3897 |
. . . . 5
⊢
{〈(TopSet‘ndx), ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉} ⊆ ({〈(Base‘ndx),
𝐼〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}) |
12 | 7, 8, 11 | strfv 16574 |
. . . 4
⊢ (ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ∈ V → ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) = (TopSet‘({〈(Base‘ndx),
𝐼〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}))) |
13 | 5, 12 | ax-mp 5 |
. . 3
⊢ ran
(𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) = (TopSet‘({〈(Base‘ndx),
𝐼〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉})) |
14 | | idlsrgtset.1 |
. . . . 5
⊢ 𝑆 = (IDLsrg‘𝑅) |
15 | | eqid 2759 |
. . . . . 6
⊢
(LSSum‘𝑅) =
(LSSum‘𝑅) |
16 | | eqid 2759 |
. . . . . 6
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
17 | | eqid 2759 |
. . . . . 6
⊢
(LSSum‘(mulGrp‘𝑅)) = (LSSum‘(mulGrp‘𝑅)) |
18 | 2, 15, 16, 17 | idlsrgval 31154 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → (IDLsrg‘𝑅) = ({〈(Base‘ndx), 𝐼〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉})) |
19 | 14, 18 | syl5eq 2806 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → 𝑆 = ({〈(Base‘ndx), 𝐼〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉})) |
20 | 19 | fveq2d 6655 |
. . 3
⊢ (𝑅 ∈ 𝑉 → (TopSet‘𝑆) = (TopSet‘({〈(Base‘ndx),
𝐼〉,
〈(+g‘ndx), (LSSum‘𝑅)〉, 〈(.r‘ndx),
(𝑖 ∈ 𝐼, 𝑗 ∈ 𝐼 ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx), {〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ 𝐼 ∧ 𝑖 ⊆ 𝑗)}〉}))) |
21 | 13, 20 | eqtr4id 2813 |
. 2
⊢ (𝑅 ∈ 𝑉 → ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) = (TopSet‘𝑆)) |
22 | 1, 21 | syl5eq 2806 |
1
⊢ (𝑅 ∈ 𝑉 → 𝐽 = (TopSet‘𝑆)) |