Step | Hyp | Ref
| Expression |
1 | | idlsrgplusg.2 |
. . . 4
⊢ ⊕ =
(LSSum‘𝑅) |
2 | 1 | fvexi 6860 |
. . 3
⊢ ⊕ ∈
V |
3 | | eqid 2733 |
. . . . 5
⊢
({⟨(Base‘ndx), (LIdeal‘𝑅)⟩, ⟨(+g‘ndx),
⊕
⟩, ⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩}) = ({⟨(Base‘ndx),
(LIdeal‘𝑅)⟩,
⟨(+g‘ndx), ⊕ ⟩,
⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩}) |
4 | 3 | idlsrgstr 32299 |
. . . 4
⊢
({⟨(Base‘ndx), (LIdeal‘𝑅)⟩, ⟨(+g‘ndx),
⊕
⟩, ⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩}) Struct ⟨1, ;10⟩ |
5 | | plusgid 17168 |
. . . 4
⊢
+g = Slot (+g‘ndx) |
6 | | snsstp2 4781 |
. . . . 5
⊢
{⟨(+g‘ndx), ⊕ ⟩} ⊆
{⟨(Base‘ndx), (LIdeal‘𝑅)⟩, ⟨(+g‘ndx),
⊕
⟩, ⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} |
7 | | ssun1 4136 |
. . . . 5
⊢
{⟨(Base‘ndx), (LIdeal‘𝑅)⟩, ⟨(+g‘ndx),
⊕
⟩, ⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ⊆ ({⟨(Base‘ndx),
(LIdeal‘𝑅)⟩,
⟨(+g‘ndx), ⊕ ⟩,
⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩}) |
8 | 6, 7 | sstri 3957 |
. . . 4
⊢
{⟨(+g‘ndx), ⊕ ⟩} ⊆
({⟨(Base‘ndx), (LIdeal‘𝑅)⟩, ⟨(+g‘ndx),
⊕
⟩, ⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩}) |
9 | 4, 5, 8 | strfv 17084 |
. . 3
⊢ ( ⊕ ∈
V → ⊕ =
(+g‘({⟨(Base‘ndx), (LIdeal‘𝑅)⟩, ⟨(+g‘ndx),
⊕
⟩, ⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩}))) |
10 | 2, 9 | ax-mp 5 |
. 2
⊢ ⊕ =
(+g‘({⟨(Base‘ndx), (LIdeal‘𝑅)⟩, ⟨(+g‘ndx),
⊕
⟩, ⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩})) |
11 | | idlsrgplusg.1 |
. . . 4
⊢ 𝑆 = (IDLsrg‘𝑅) |
12 | | eqid 2733 |
. . . . 5
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
13 | | eqid 2733 |
. . . . 5
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
14 | | eqid 2733 |
. . . . 5
⊢
(LSSum‘(mulGrp‘𝑅)) = (LSSum‘(mulGrp‘𝑅)) |
15 | 12, 1, 13, 14 | idlsrgval 32300 |
. . . 4
⊢ (𝑅 ∈ 𝑉 → (IDLsrg‘𝑅) = ({⟨(Base‘ndx),
(LIdeal‘𝑅)⟩,
⟨(+g‘ndx), ⊕ ⟩,
⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩})) |
16 | 11, 15 | eqtrid 2785 |
. . 3
⊢ (𝑅 ∈ 𝑉 → 𝑆 = ({⟨(Base‘ndx),
(LIdeal‘𝑅)⟩,
⟨(+g‘ndx), ⊕ ⟩,
⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩})) |
17 | 16 | fveq2d 6850 |
. 2
⊢ (𝑅 ∈ 𝑉 → (+g‘𝑆) =
(+g‘({⟨(Base‘ndx), (LIdeal‘𝑅)⟩, ⟨(+g‘ndx),
⊕
⟩, ⟨(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))⟩} ∪ {⟨(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})⟩, ⟨(le‘ndx),
{⟨𝑖, 𝑗⟩ ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}⟩}))) |
18 | 10, 17 | eqtr4id 2792 |
1
⊢ (𝑅 ∈ 𝑉 → ⊕ =
(+g‘𝑆)) |