Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. 2
β’ (π
β π β π
β V) |
2 | | fvexd 6854 |
. . . 4
β’ (π = π
β (LIdealβπ) β V) |
3 | | simpr 485 |
. . . . . . . . 9
β’ ((π = π
β§ π = (LIdealβπ)) β π = (LIdealβπ)) |
4 | | simpl 483 |
. . . . . . . . . 10
β’ ((π = π
β§ π = (LIdealβπ)) β π = π
) |
5 | 4 | fveq2d 6843 |
. . . . . . . . 9
β’ ((π = π
β§ π = (LIdealβπ)) β (LIdealβπ) = (LIdealβπ
)) |
6 | 3, 5 | eqtrd 2777 |
. . . . . . . 8
β’ ((π = π
β§ π = (LIdealβπ)) β π = (LIdealβπ
)) |
7 | | idlsrgval.1 |
. . . . . . . 8
β’ πΌ = (LIdealβπ
) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . . 7
β’ ((π = π
β§ π = (LIdealβπ)) β π = πΌ) |
9 | 8 | opeq2d 4835 |
. . . . . 6
β’ ((π = π
β§ π = (LIdealβπ)) β β¨(Baseβndx), πβ© = β¨(Baseβndx),
πΌβ©) |
10 | 4 | fveq2d 6843 |
. . . . . . . 8
β’ ((π = π
β§ π = (LIdealβπ)) β (LSSumβπ) = (LSSumβπ
)) |
11 | | idlsrgval.2 |
. . . . . . . 8
β’ β =
(LSSumβπ
) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . 7
β’ ((π = π
β§ π = (LIdealβπ)) β (LSSumβπ) = β ) |
13 | 12 | opeq2d 4835 |
. . . . . 6
β’ ((π = π
β§ π = (LIdealβπ)) β β¨(+gβndx),
(LSSumβπ)β© =
β¨(+gβndx), β
β©) |
14 | 4 | fveq2d 6843 |
. . . . . . . . 9
β’ ((π = π
β§ π = (LIdealβπ)) β (RSpanβπ) = (RSpanβπ
)) |
15 | 4 | fveq2d 6843 |
. . . . . . . . . . . . 13
β’ ((π = π
β§ π = (LIdealβπ)) β (mulGrpβπ) = (mulGrpβπ
)) |
16 | | idlsrgval.3 |
. . . . . . . . . . . . 13
β’ πΊ = (mulGrpβπ
) |
17 | 15, 16 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ ((π = π
β§ π = (LIdealβπ)) β (mulGrpβπ) = πΊ) |
18 | 17 | fveq2d 6843 |
. . . . . . . . . . 11
β’ ((π = π
β§ π = (LIdealβπ)) β (LSSumβ(mulGrpβπ)) = (LSSumβπΊ)) |
19 | | idlsrgval.4 |
. . . . . . . . . . 11
β’ β =
(LSSumβπΊ) |
20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . 10
β’ ((π = π
β§ π = (LIdealβπ)) β (LSSumβ(mulGrpβπ)) = β ) |
21 | 20 | oveqd 7368 |
. . . . . . . . 9
β’ ((π = π
β§ π = (LIdealβπ)) β (π(LSSumβ(mulGrpβπ))π) = (π β π)) |
22 | 14, 21 | fveq12d 6846 |
. . . . . . . 8
β’ ((π = π
β§ π = (LIdealβπ)) β ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)) = ((RSpanβπ
)β(π β π))) |
23 | 8, 8, 22 | mpoeq123dv 7426 |
. . . . . . 7
β’ ((π = π
β§ π = (LIdealβπ)) β (π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π))) = (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))) |
24 | 23 | opeq2d 4835 |
. . . . . 6
β’ ((π = π
β§ π = (LIdealβπ)) β β¨(.rβndx),
(π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β© = β¨(.rβndx),
(π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))β©) |
25 | 9, 13, 24 | tpeq123d 4707 |
. . . . 5
β’ ((π = π
β§ π = (LIdealβπ)) β {β¨(Baseβndx), πβ©,
β¨(+gβndx), (LSSumβπ)β©, β¨(.rβndx),
(π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} = {β¨(Baseβndx), πΌβ©,
β¨(+gβndx), β β©,
β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))β©}) |
26 | 8 | rabeqdv 3420 |
. . . . . . . . 9
β’ ((π = π
β§ π = (LIdealβπ)) β {π β π β£ Β¬ π β π} = {π β πΌ β£ Β¬ π β π}) |
27 | 8, 26 | mpteq12dv 5194 |
. . . . . . . 8
β’ ((π = π
β§ π = (LIdealβπ)) β (π β π β¦ {π β π β£ Β¬ π β π}) = (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})) |
28 | 27 | rneqd 5891 |
. . . . . . 7
β’ ((π = π
β§ π = (LIdealβπ)) β ran (π β π β¦ {π β π β£ Β¬ π β π}) = ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})) |
29 | 28 | opeq2d 4835 |
. . . . . 6
β’ ((π = π
β§ π = (LIdealβπ)) β β¨(TopSetβndx), ran
(π β π β¦ {π β π β£ Β¬ π β π})β© = β¨(TopSetβndx), ran
(π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©) |
30 | 8 | sseq2d 3974 |
. . . . . . . . 9
β’ ((π = π
β§ π = (LIdealβπ)) β ({π, π} β π β {π, π} β πΌ)) |
31 | 30 | anbi1d 630 |
. . . . . . . 8
β’ ((π = π
β§ π = (LIdealβπ)) β (({π, π} β π β§ π β π) β ({π, π} β πΌ β§ π β π))) |
32 | 31 | opabbidv 5169 |
. . . . . . 7
β’ ((π = π
β§ π = (LIdealβπ)) β {β¨π, πβ© β£ ({π, π} β π β§ π β π)} = {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}) |
33 | 32 | opeq2d 4835 |
. . . . . 6
β’ ((π = π
β§ π = (LIdealβπ)) β β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β© = β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©) |
34 | 29, 33 | preq12d 4700 |
. . . . 5
β’ ((π = π
β§ π = (LIdealβπ)) β {β¨(TopSetβndx), ran
(π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©} = {β¨(TopSetβndx), ran
(π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©}) |
35 | 25, 34 | uneq12d 4122 |
. . . 4
β’ ((π = π
β§ π = (LIdealβπ)) β ({β¨(Baseβndx), πβ©,
β¨(+gβndx), (LSSumβπ)β©, β¨(.rβndx),
(π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©}) = ({β¨(Baseβndx), πΌβ©,
β¨(+gβndx), β β©,
β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©})) |
36 | 2, 35 | csbied 3891 |
. . 3
β’ (π = π
β β¦(LIdealβπ) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (LSSumβπ)β©, β¨(.rβndx),
(π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©}) = ({β¨(Baseβndx), πΌβ©,
β¨(+gβndx), β β©,
β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©})) |
37 | | df-idlsrg 32065 |
. . 3
β’ IDLsrg =
(π β V β¦
β¦(LIdealβπ) / πβ¦({β¨(Baseβndx),
πβ©,
β¨(+gβndx), (LSSumβπ)β©, β¨(.rβndx),
(π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} βͺ {β¨(TopSetβndx),
ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©})) |
38 | | tpex 7673 |
. . . 4
β’
{β¨(Baseβndx), πΌβ©, β¨(+gβndx),
β
β©, β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))β©} β V |
39 | | prex 5387 |
. . . 4
β’
{β¨(TopSetβndx), ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©} β V |
40 | 38, 39 | unex 7672 |
. . 3
β’
({β¨(Baseβndx), πΌβ©, β¨(+gβndx),
β
β©, β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©}) β V |
41 | 36, 37, 40 | fvmpt 6945 |
. 2
β’ (π
β V β
(IDLsrgβπ
) =
({β¨(Baseβndx), πΌβ©, β¨(+gβndx),
β
β©, β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©})) |
42 | 1, 41 | syl 17 |
1
β’ (π
β π β (IDLsrgβπ
) = ({β¨(Baseβndx), πΌβ©,
β¨(+gβndx), β β©,
β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ
)β(π β π)))β©} βͺ {β¨(TopSetβndx),
ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©})) |