Step | Hyp | Ref
| Expression |
1 | | idlsrgbas.2 |
. . . 4
โข ๐ผ = (LIdealโ๐
) |
2 | 1 | fvexi 6860 |
. . 3
โข ๐ผ โ V |
3 | | eqid 2733 |
. . . . 5
โข
({โจ(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), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ}) |
4 | 3 | idlsrgstr 32299 |
. . . 4
โข
({โจ(Baseโndx), ๐ผโฉ, โจ(+gโndx),
(LSSumโ๐
)โฉ,
โจ(.rโndx), (๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โช {โจ(TopSetโndx),
ran (๐ โ ๐ผ โฆ {๐ โ ๐ผ โฃ ยฌ ๐ โ ๐})โฉ, โจ(leโndx), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ}) Struct โจ1, ;10โฉ |
5 | | baseid 17094 |
. . . 4
โข Base =
Slot (Baseโndx) |
6 | | snsstp1 4780 |
. . . . 5
โข
{โจ(Baseโndx), ๐ผโฉ} โ {โจ(Baseโndx),
๐ผโฉ,
โจ(+gโndx), (LSSumโ๐
)โฉ, โจ(.rโndx),
(๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} |
7 | | ssun1 4136 |
. . . . 5
โข
{โจ(Baseโndx), ๐ผโฉ, โจ(+gโndx),
(LSSumโ๐
)โฉ,
โจ(.rโndx), (๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โ ({โจ(Baseโndx),
๐ผโฉ,
โจ(+gโndx), (LSSumโ๐
)โฉ, โจ(.rโndx),
(๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โช {โจ(TopSetโndx),
ran (๐ โ ๐ผ โฆ {๐ โ ๐ผ โฃ ยฌ ๐ โ ๐})โฉ, โจ(leโndx), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ}) |
8 | 6, 7 | sstri 3957 |
. . . 4
โข
{โจ(Baseโndx), ๐ผโฉ} โ ({โจ(Baseโndx),
๐ผโฉ,
โจ(+gโndx), (LSSumโ๐
)โฉ, โจ(.rโndx),
(๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โช {โจ(TopSetโndx),
ran (๐ โ ๐ผ โฆ {๐ โ ๐ผ โฃ ยฌ ๐ โ ๐})โฉ, โจ(leโndx), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ}) |
9 | 4, 5, 8 | strfv 17084 |
. . 3
โข (๐ผ โ V โ ๐ผ =
(Baseโ({โจ(Baseโndx), ๐ผโฉ, โจ(+gโndx),
(LSSumโ๐
)โฉ,
โจ(.rโndx), (๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โช {โจ(TopSetโndx),
ran (๐ โ ๐ผ โฆ {๐ โ ๐ผ โฃ ยฌ ๐ โ ๐})โฉ, โจ(leโndx), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ}))) |
10 | 2, 9 | ax-mp 5 |
. 2
โข ๐ผ =
(Baseโ({โจ(Baseโndx), ๐ผโฉ, โจ(+gโndx),
(LSSumโ๐
)โฉ,
โจ(.rโndx), (๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โช {โจ(TopSetโndx),
ran (๐ โ ๐ผ โฆ {๐ โ ๐ผ โฃ ยฌ ๐ โ ๐})โฉ, โจ(leโndx), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ})) |
11 | | idlsrgbas.1 |
. . . 4
โข ๐ = (IDLsrgโ๐
) |
12 | | eqid 2733 |
. . . . 5
โข
(LSSumโ๐
) =
(LSSumโ๐
) |
13 | | eqid 2733 |
. . . . 5
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
14 | | eqid 2733 |
. . . . 5
โข
(LSSumโ(mulGrpโ๐
)) = (LSSumโ(mulGrpโ๐
)) |
15 | 1, 12, 13, 14 | idlsrgval 32300 |
. . . 4
โข (๐
โ ๐ โ (IDLsrgโ๐
) = ({โจ(Baseโndx), ๐ผโฉ,
โจ(+gโndx), (LSSumโ๐
)โฉ, โจ(.rโndx),
(๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โช {โจ(TopSetโndx),
ran (๐ โ ๐ผ โฆ {๐ โ ๐ผ โฃ ยฌ ๐ โ ๐})โฉ, โจ(leโndx), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ})) |
16 | 11, 15 | eqtrid 2785 |
. . 3
โข (๐
โ ๐ โ ๐ = ({โจ(Baseโndx), ๐ผโฉ,
โจ(+gโndx), (LSSumโ๐
)โฉ, โจ(.rโndx),
(๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โช {โจ(TopSetโndx),
ran (๐ โ ๐ผ โฆ {๐ โ ๐ผ โฃ ยฌ ๐ โ ๐})โฉ, โจ(leโndx), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ})) |
17 | 16 | fveq2d 6850 |
. 2
โข (๐
โ ๐ โ (Baseโ๐) = (Baseโ({โจ(Baseโndx),
๐ผโฉ,
โจ(+gโndx), (LSSumโ๐
)โฉ, โจ(.rโndx),
(๐ โ ๐ผ, ๐ โ ๐ผ โฆ ((RSpanโ๐
)โ(๐(LSSumโ(mulGrpโ๐
))๐)))โฉ} โช {โจ(TopSetโndx),
ran (๐ โ ๐ผ โฆ {๐ โ ๐ผ โฃ ยฌ ๐ โ ๐})โฉ, โจ(leโndx), {โจ๐, ๐โฉ โฃ ({๐, ๐} โ ๐ผ โง ๐ โ ๐)}โฉ}))) |
18 | 10, 17 | eqtr4id 2792 |
1
โข (๐
โ ๐ โ ๐ผ = (Baseโ๐)) |