Step | Hyp | Ref
| Expression |
1 | | idlsrgtset.3 |
. 2
β’ π½ = ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) |
2 | | idlsrgtset.2 |
. . . . . . 7
β’ πΌ = (LIdealβπ
) |
3 | 2 | fvexi 6860 |
. . . . . 6
β’ πΌ β V |
4 | 3 | mptex 7177 |
. . . . 5
β’ (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β V |
5 | 4 | rnex 7853 |
. . . 4
β’ ran
(π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β V |
6 | | eqid 2733 |
. . . . . 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 32299 |
. . . . 5
β’
({β¨(Baseβndx), πΌβ©, β¨(+gβndx),
(LSSumβπ
)β©,
β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π(LSSumβ(mulGrpβπ
))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©}) Struct β¨1, ;10β© |
8 | | tsetid 17242 |
. . . . 5
β’ TopSet =
Slot (TopSetβndx) |
9 | | snsspr1 4778 |
. . . . . 6
β’
{β¨(TopSetβndx), ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©} β {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©} |
10 | | ssun2 4137 |
. . . . . 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 3957 |
. . . . 5
β’
{β¨(TopSetβndx), ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©} β ({β¨(Baseβndx),
πΌβ©,
β¨(+gβndx), (LSSumβπ
)β©, β¨(.rβndx),
(π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π(LSSumβ(mulGrpβπ
))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©}) |
12 | 7, 8, 11 | strfv 17084 |
. . . 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 2733 |
. . . . . 6
β’
(LSSumβπ
) =
(LSSumβπ
) |
16 | | eqid 2733 |
. . . . . 6
β’
(mulGrpβπ
) =
(mulGrpβπ
) |
17 | | eqid 2733 |
. . . . . 6
β’
(LSSumβ(mulGrpβπ
)) = (LSSumβ(mulGrpβπ
)) |
18 | 2, 15, 16, 17 | idlsrgval 32300 |
. . . . 5
β’ (π
β π β (IDLsrgβπ
) = ({β¨(Baseβndx), πΌβ©,
β¨(+gβndx), (LSSumβπ
)β©, β¨(.rβndx),
(π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π(LSSumβ(mulGrpβπ
))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©})) |
19 | 14, 18 | eqtrid 2785 |
. . . 4
β’ (π
β π β π = ({β¨(Baseβndx), πΌβ©,
β¨(+gβndx), (LSSumβπ
)β©, β¨(.rβndx),
(π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π(LSSumβ(mulGrpβπ
))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©})) |
20 | 19 | fveq2d 6850 |
. . 3
β’ (π
β π β (TopSetβπ) = (TopSetβ({β¨(Baseβndx),
πΌβ©,
β¨(+gβndx), (LSSumβπ
)β©, β¨(.rβndx),
(π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π(LSSumβ(mulGrpβπ
))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©}))) |
21 | 13, 20 | eqtr4id 2792 |
. 2
β’ (π
β π β ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) = (TopSetβπ)) |
22 | 1, 21 | eqtrid 2785 |
1
β’ (π
β π β π½ = (TopSetβπ)) |