Step | Hyp | Ref
| Expression |
1 | | ixpsnval 8841 |
. . 3
β’ (π β π β Xπ₯ β {π} (Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = {π β£ (π Fn {π} β§ (πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)))}) |
2 | 1 | adantl 483 |
. 2
β’ ((π
β π β§ π β π) β Xπ₯ β {π} (Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = {π β£ (π Fn {π} β§ (πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)))}) |
3 | | csbfv2g 6892 |
. . . . . . . . 9
β’ (π β π β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseββ¦π / π₯β¦(({π} Γ {(ringLModβπ
)})βπ₯))) |
4 | | csbfv2g 6892 |
. . . . . . . . . . 11
β’ (π β π β β¦π / π₯β¦(({π} Γ {(ringLModβπ
)})βπ₯) = (({π} Γ {(ringLModβπ
)})ββ¦π / π₯β¦π₯)) |
5 | | csbvarg 4392 |
. . . . . . . . . . . 12
β’ (π β π β β¦π / π₯β¦π₯ = π) |
6 | 5 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (π β π β (({π} Γ {(ringLModβπ
)})ββ¦π / π₯β¦π₯) = (({π} Γ {(ringLModβπ
)})βπ)) |
7 | 4, 6 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β π β β¦π / π₯β¦(({π} Γ {(ringLModβπ
)})βπ₯) = (({π} Γ {(ringLModβπ
)})βπ)) |
8 | 7 | fveq2d 6847 |
. . . . . . . . 9
β’ (π β π β (Baseββ¦π / π₯β¦(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβ(({π} Γ {(ringLModβπ
)})βπ))) |
9 | 3, 8 | eqtrd 2773 |
. . . . . . . 8
β’ (π β π β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβ(({π} Γ {(ringLModβπ
)})βπ))) |
10 | 9 | adantl 483 |
. . . . . . 7
β’ ((π
β π β§ π β π) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβ(({π} Γ {(ringLModβπ
)})βπ))) |
11 | | fvexd 6858 |
. . . . . . . . . . . 12
β’ (π
β π β (ringLModβπ
) β V) |
12 | 11 | anim1ci 617 |
. . . . . . . . . . 11
β’ ((π
β π β§ π β π) β (π β π β§ (ringLModβπ
) β V)) |
13 | | xpsng 7086 |
. . . . . . . . . . 11
β’ ((π β π β§ (ringLModβπ
) β V) β ({π} Γ {(ringLModβπ
)}) = {β¨π, (ringLModβπ
)β©}) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
β’ ((π
β π β§ π β π) β ({π} Γ {(ringLModβπ
)}) = {β¨π, (ringLModβπ
)β©}) |
15 | 14 | fveq1d 6845 |
. . . . . . . . 9
β’ ((π
β π β§ π β π) β (({π} Γ {(ringLModβπ
)})βπ) = ({β¨π, (ringLModβπ
)β©}βπ)) |
16 | | fvsng 7127 |
. . . . . . . . . 10
β’ ((π β π β§ (ringLModβπ
) β V) β ({β¨π, (ringLModβπ
)β©}βπ) = (ringLModβπ
)) |
17 | 12, 16 | syl 17 |
. . . . . . . . 9
β’ ((π
β π β§ π β π) β ({β¨π, (ringLModβπ
)β©}βπ) = (ringLModβπ
)) |
18 | 15, 17 | eqtrd 2773 |
. . . . . . . 8
β’ ((π
β π β§ π β π) β (({π} Γ {(ringLModβπ
)})βπ) = (ringLModβπ
)) |
19 | 18 | fveq2d 6847 |
. . . . . . 7
β’ ((π
β π β§ π β π) β (Baseβ(({π} Γ {(ringLModβπ
)})βπ)) = (Baseβ(ringLModβπ
))) |
20 | 10, 19 | eqtrd 2773 |
. . . . . 6
β’ ((π
β π β§ π β π) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβ(ringLModβπ
))) |
21 | | rlmbas 20680 |
. . . . . 6
β’
(Baseβπ
) =
(Baseβ(ringLModβπ
)) |
22 | 20, 21 | eqtr4di 2791 |
. . . . 5
β’ ((π
β π β§ π β π) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = (Baseβπ
)) |
23 | 22 | eleq2d 2820 |
. . . 4
β’ ((π
β π β§ π β π) β ((πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) β (πβπ) β (Baseβπ
))) |
24 | 23 | anbi2d 630 |
. . 3
β’ ((π
β π β§ π β π) β ((π Fn {π} β§ (πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯))) β (π Fn {π} β§ (πβπ) β (Baseβπ
)))) |
25 | 24 | abbidv 2802 |
. 2
β’ ((π
β π β§ π β π) β {π β£ (π Fn {π} β§ (πβπ) β β¦π / π₯β¦(Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)))} = {π β£ (π Fn {π} β§ (πβπ) β (Baseβπ
))}) |
26 | 2, 25 | eqtrd 2773 |
1
β’ ((π
β π β§ π β π) β Xπ₯ β {π} (Baseβ(({π} Γ {(ringLModβπ
)})βπ₯)) = {π β£ (π Fn {π} β§ (πβπ) β (Baseβπ
))}) |