Step | Hyp | Ref
| Expression |
1 | | matassa.a |
. . 3
β’ π΄ = (π Mat π
) |
2 | | eqid 2733 |
. . 3
β’
(Baseβπ
) =
(Baseβπ
) |
3 | 1, 2 | matbas2 21923 |
. 2
β’ ((π β Fin β§ π
β CRing) β
((Baseβπ
)
βm (π
Γ π)) =
(Baseβπ΄)) |
4 | 1 | matsca2 21922 |
. 2
β’ ((π β Fin β§ π
β CRing) β π
= (Scalarβπ΄)) |
5 | | eqidd 2734 |
. 2
β’ ((π β Fin β§ π
β CRing) β
(Baseβπ
) =
(Baseβπ
)) |
6 | | eqidd 2734 |
. 2
β’ ((π β Fin β§ π
β CRing) β (
Β·π βπ΄) = ( Β·π
βπ΄)) |
7 | | eqid 2733 |
. . 3
β’ (π
maMul β¨π, π, πβ©) = (π
maMul β¨π, π, πβ©) |
8 | 1, 7 | matmulr 21940 |
. 2
β’ ((π β Fin β§ π
β CRing) β (π
maMul β¨π, π, πβ©) = (.rβπ΄)) |
9 | | crngring 20068 |
. . 3
β’ (π
β CRing β π
β Ring) |
10 | 1 | matlmod 21931 |
. . 3
β’ ((π β Fin β§ π
β Ring) β π΄ β LMod) |
11 | 9, 10 | sylan2 594 |
. 2
β’ ((π β Fin β§ π
β CRing) β π΄ β LMod) |
12 | 1 | matring 21945 |
. . 3
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
13 | 9, 12 | sylan2 594 |
. 2
β’ ((π β Fin β§ π
β CRing) β π΄ β Ring) |
14 | 9 | ad2antlr 726 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β π
β Ring) |
15 | | simpll 766 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β π β Fin) |
16 | | eqid 2733 |
. . . 4
β’
(.rβπ
) = (.rβπ
) |
17 | | simpr1 1195 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β π₯ β (Baseβπ
)) |
18 | | simpr2 1196 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β π¦ β ((Baseβπ
) βm (π Γ π))) |
19 | | simpr3 1197 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β π§ β ((Baseβπ
) βm (π Γ π))) |
20 | 2, 14, 7, 15, 15, 15, 16, 17, 18, 19 | mamuvs1 21905 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β ((((π Γ π) Γ {π₯}) βf
(.rβπ
)π¦)(π
maMul β¨π, π, πβ©)π§) = (((π Γ π) Γ {π₯}) βf
(.rβπ
)(π¦(π
maMul β¨π, π, πβ©)π§))) |
21 | 3 | adantr 482 |
. . . . . 6
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β ((Baseβπ
) βm (π Γ π)) = (Baseβπ΄)) |
22 | 18, 21 | eleqtrd 2836 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β π¦ β (Baseβπ΄)) |
23 | | eqid 2733 |
. . . . . 6
β’
(Baseβπ΄) =
(Baseβπ΄) |
24 | | eqid 2733 |
. . . . . 6
β’ (
Β·π βπ΄) = ( Β·π
βπ΄) |
25 | | eqid 2733 |
. . . . . 6
β’ (π Γ π) = (π Γ π) |
26 | 1, 23, 2, 24, 16, 25 | matvsca2 21930 |
. . . . 5
β’ ((π₯ β (Baseβπ
) β§ π¦ β (Baseβπ΄)) β (π₯( Β·π
βπ΄)π¦) = (((π Γ π) Γ {π₯}) βf
(.rβπ
)π¦)) |
27 | 17, 22, 26 | syl2anc 585 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β (π₯( Β·π
βπ΄)π¦) = (((π Γ π) Γ {π₯}) βf
(.rβπ
)π¦)) |
28 | 27 | oveq1d 7424 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β ((π₯( Β·π
βπ΄)π¦)(π
maMul β¨π, π, πβ©)π§) = ((((π Γ π) Γ {π₯}) βf
(.rβπ
)π¦)(π
maMul β¨π, π, πβ©)π§)) |
29 | 2, 14, 7, 15, 15, 15, 18, 19 | mamucl 21901 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β (π¦(π
maMul β¨π, π, πβ©)π§) β ((Baseβπ
) βm (π Γ π))) |
30 | 29, 21 | eleqtrd 2836 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β (π¦(π
maMul β¨π, π, πβ©)π§) β (Baseβπ΄)) |
31 | 1, 23, 2, 24, 16, 25 | matvsca2 21930 |
. . . 4
β’ ((π₯ β (Baseβπ
) β§ (π¦(π
maMul β¨π, π, πβ©)π§) β (Baseβπ΄)) β (π₯( Β·π
βπ΄)(π¦(π
maMul β¨π, π, πβ©)π§)) = (((π Γ π) Γ {π₯}) βf
(.rβπ
)(π¦(π
maMul β¨π, π, πβ©)π§))) |
32 | 17, 30, 31 | syl2anc 585 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β (π₯( Β·π
βπ΄)(π¦(π
maMul β¨π, π, πβ©)π§)) = (((π Γ π) Γ {π₯}) βf
(.rβπ
)(π¦(π
maMul β¨π, π, πβ©)π§))) |
33 | 20, 28, 32 | 3eqtr4d 2783 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β ((π₯( Β·π
βπ΄)π¦)(π
maMul β¨π, π, πβ©)π§) = (π₯( Β·π
βπ΄)(π¦(π
maMul β¨π, π, πβ©)π§))) |
34 | | simplr 768 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β π
β CRing) |
35 | 34, 2, 16, 7, 15, 15, 15, 18, 17, 19 | mamuvs2 21906 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β (π¦(π
maMul β¨π, π, πβ©)(((π Γ π) Γ {π₯}) βf
(.rβπ
)π§)) = (((π Γ π) Γ {π₯}) βf
(.rβπ
)(π¦(π
maMul β¨π, π, πβ©)π§))) |
36 | 19, 21 | eleqtrd 2836 |
. . . . 5
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β π§ β (Baseβπ΄)) |
37 | 1, 23, 2, 24, 16, 25 | matvsca2 21930 |
. . . . 5
β’ ((π₯ β (Baseβπ
) β§ π§ β (Baseβπ΄)) β (π₯( Β·π
βπ΄)π§) = (((π Γ π) Γ {π₯}) βf
(.rβπ
)π§)) |
38 | 17, 36, 37 | syl2anc 585 |
. . . 4
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β (π₯( Β·π
βπ΄)π§) = (((π Γ π) Γ {π₯}) βf
(.rβπ
)π§)) |
39 | 38 | oveq2d 7425 |
. . 3
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β (π¦(π
maMul β¨π, π, πβ©)(π₯( Β·π
βπ΄)π§)) = (π¦(π
maMul β¨π, π, πβ©)(((π Γ π) Γ {π₯}) βf
(.rβπ
)π§))) |
40 | 35, 39, 32 | 3eqtr4d 2783 |
. 2
β’ (((π β Fin β§ π
β CRing) β§ (π₯ β (Baseβπ
) β§ π¦ β ((Baseβπ
) βm (π Γ π)) β§ π§ β ((Baseβπ
) βm (π Γ π)))) β (π¦(π
maMul β¨π, π, πβ©)(π₯( Β·π
βπ΄)π§)) = (π₯( Β·π
βπ΄)(π¦(π
maMul β¨π, π, πβ©)π§))) |
41 | 3, 4, 5, 6, 8, 11,
13, 33, 40 | isassad 21419 |
1
β’ ((π β Fin β§ π
β CRing) β π΄ β AssAlg) |