| Step | Hyp | Ref
| Expression |
|---|
| 1 | | ixpsnval 8898 |
. . 3
β’ (π β π β Xπ₯ β {π} (Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = {π β£ (π Fn {π} β§ (πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)))}) |
| 2 | 1 | adantl 481 |
. 2
β’ ((π
β π β§ π β π) β Xπ₯ β {π} (Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = {π β£ (π Fn {π} β§ (πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)))}) |
| 3 | | csbfv2g 6940 |
. . . . . . . . 9
β’ (π β π β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseββ¦π / π₯β¦(({π} Γ {(ringLModβπ
)})βπ₯))) |
| 4 | | csbfv2g 6940 |
. . . . . . . . . . 11
β’ (π β π β β¦π / π₯β¦(({π} Γ {(ringLModβπ
)})βπ₯) = (({π} Γ {(ringLModβπ
)})ββ¦π / π₯β¦π₯)) |
| 5 | | csbvarg 4431 |
. . . . . . . . . . . 12
β’ (π β π β β¦π / π₯β¦π₯ = π) |
| 6 | 5 | fveq2d 6895 |
. . . . . . . . . . 11
β’ (π β π β (({π} Γ {(ringLModβπ
)})ββ¦π / π₯β¦π₯) = (({π} Γ {(ringLModβπ
)})βπ)) |
| 7 | 4, 6 | eqtrd 2771 |
. . . . . . . . . 10
β’ (π β π β β¦π / π₯β¦(({π} Γ {(ringLModβπ
)})βπ₯) = (({π} Γ {(ringLModβπ
)})βπ)) |
| 8 | 7 | fveq2d 6895 |
. . . . . . . . 9
β’ (π β π β (Baseββ¦π / π₯β¦(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβ(({π} Γ {(ringLModβπ
)})βπ))) |
| 9 | 3, 8 | eqtrd 2771 |
. . . . . . . 8
β’ (π β π β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβ(({π} Γ {(ringLModβπ
)})βπ))) |
| 10 | 9 | adantl 481 |
. . . . . . 7
β’ ((π
β π β§ π β π) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβ(({π} Γ {(ringLModβπ
)})βπ))) |
| 11 | | fvexd 6906 |
. . . . . . . . . . . 12
β’ (π
β π β (ringLModβπ
) β V) |
| 12 | 11 | anim1ci 615 |
. . . . . . . . . . 11
β’ ((π
β π β§ π β π) β (π β π β§ (ringLModβπ
) β V)) |
| 13 | | xpsng 7139 |
. . . . . . . . . . 11
β’ ((π β π β§ (ringLModβπ
) β V) β ({π} Γ {(ringLModβπ
)}) = {β¨π, (ringLModβπ
)β©}) |
| 14 | 12, 13 | syl 17 |
. . . . . . . . . 10
β’ ((π
β π β§ π β π) β ({π} Γ {(ringLModβπ
)}) = {β¨π, (ringLModβπ
)β©}) |
| 15 | 14 | fveq1d 6893 |
. . . . . . . . 9
β’ ((π
β π β§ π β π) β (({π} Γ {(ringLModβπ
)})βπ) = ({β¨π, (ringLModβπ
)β©}βπ)) |
| 16 | | fvsng 7180 |
. . . . . . . . . 10
β’ ((π β π β§ (ringLModβπ
) β V) β ({β¨π, (ringLModβπ
)β©}βπ) = (ringLModβπ
)) |
| 17 | 12, 16 | syl 17 |
. . . . . . . . 9
β’ ((π
β π β§ π β π) β ({β¨π, (ringLModβπ
)β©}βπ) = (ringLModβπ
)) |
| 18 | 15, 17 | eqtrd 2771 |
. . . . . . . 8
β’ ((π
β π β§ π β π) β (({π} Γ {(ringLModβπ
)})βπ) = (ringLModβπ
)) |
| 19 | 18 | fveq2d 6895 |
. . . . . . 7
β’ ((π
β π β§ π β π) β (Baseβ(({π} Γ {(ringLModβπ
)})βπ)) = (Baseβ(ringLModβπ
))) |
| 20 | 10, 19 | eqtrd 2771 |
. . . . . 6
β’ ((π
β π β§ π β π) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβ(ringLModβπ
))) |
| 21 | | rlmbas 20963 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβ(ringLModβπ
)) |
| 22 | 20, 21 | eqtr4di 2789 |
. . . . 5
β’ ((π
β π β§ π β π) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβπ
)) |
| 23 | 22 | eleq2d 2818 |
. . . 4
β’ ((π
β π β§ π β π) β ((πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) β (πβπ) β (Baseβπ
))) |
| 24 | 23 | anbi2d 628 |
. . 3
β’ ((π
β π β§ π β π) β ((π Fn {π} β§ (πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯))) β (π Fn {π} β§ (πβπ) β (Baseβπ
)))) |
| 25 | 24 | abbidv 2800 |
. 2
β’ ((π
β π β§ π β π) β {π β£ (π Fn {π} β§ (πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)))} = {π β£ (π Fn {π} β§ (πβπ) β (Baseβπ
))}) |
| 26 | 2, 25 | eqtrd 2771 |
1
β’ ((π
β π β§ π β π) β Xπ₯ β {π} (Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = {π β£ (π Fn {π} β§ (πβπ) β (Baseβπ
))}) |
