Step | Hyp | Ref
| Expression |
1 | | idlsrgplusg.2 |
. . . 4
⊢ ⊕ =
(LSSum‘𝑅) |
2 | 1 | fvexi 6731 |
. . 3
⊢ ⊕ ∈
V |
3 | | eqid 2737 |
. . . . 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 31361 |
. . . 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 16829 |
. . . 4
⊢
+g = Slot (+g‘ndx) |
6 | | snsstp2 4730 |
. . . . 5
⊢
{〈(+g‘ndx), ⊕ 〉} ⊆
{〈(Base‘ndx), (LIdeal‘𝑅)〉, 〈(+g‘ndx),
⊕
〉, 〈(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} |
7 | | ssun1 4086 |
. . . . 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 3910 |
. . . 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 16754 |
. . 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 2737 |
. . . . 5
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) |
13 | | eqid 2737 |
. . . . 5
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
14 | | eqid 2737 |
. . . . 5
⊢
(LSSum‘(mulGrp‘𝑅)) = (LSSum‘(mulGrp‘𝑅)) |
15 | 12, 1, 13, 14 | idlsrgval 31362 |
. . . 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 | syl5eq 2790 |
. . 3
⊢ (𝑅 ∈ 𝑉 → 𝑆 = ({〈(Base‘ndx),
(LIdeal‘𝑅)〉,
〈(+g‘ndx), ⊕ 〉,
〈(.r‘ndx), (𝑖 ∈ (LIdeal‘𝑅), 𝑗 ∈ (LIdeal‘𝑅) ↦ ((RSpan‘𝑅)‘(𝑖(LSSum‘(mulGrp‘𝑅))𝑗)))〉} ∪ {〈(TopSet‘ndx),
ran (𝑖 ∈
(LIdeal‘𝑅) ↦
{𝑗 ∈
(LIdeal‘𝑅) ∣
¬ 𝑖 ⊆ 𝑗})〉, 〈(le‘ndx),
{〈𝑖, 𝑗〉 ∣ ({𝑖, 𝑗} ⊆ (LIdeal‘𝑅) ∧ 𝑖 ⊆ 𝑗)}〉})) |
17 | 16 | fveq2d 6721 |
. 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 2797 |
1
⊢ (𝑅 ∈ 𝑉 → ⊕ =
(+g‘𝑆)) |