Step | Hyp | Ref
| Expression |
1 | | scmatmhm.m |
. . . 4
β’ π = (mulGrpβπ
) |
2 | 1 | ringmgp 20133 |
. . 3
β’ (π
β Ring β π β Mnd) |
3 | 2 | adantl 482 |
. 2
β’ ((π β Fin β§ π
β Ring) β π β Mnd) |
4 | | scmatrhmval.a |
. . . 4
β’ π΄ = (π Mat π
) |
5 | | eqid 2732 |
. . . 4
β’
(Baseβπ΄) =
(Baseβπ΄) |
6 | | scmatrhmval.k |
. . . 4
β’ πΎ = (Baseβπ
) |
7 | | eqid 2732 |
. . . 4
β’
(0gβπ
) = (0gβπ
) |
8 | | scmatrhmval.c |
. . . 4
β’ πΆ = (π ScMat π
) |
9 | 4, 5, 6, 7, 8 | scmatsrng 22242 |
. . 3
β’ ((π β Fin β§ π
β Ring) β πΆ β (SubRingβπ΄)) |
10 | | scmatghm.s |
. . . 4
β’ π = (π΄ βΎs πΆ) |
11 | 10 | subrgring 20464 |
. . 3
β’ (πΆ β (SubRingβπ΄) β π β Ring) |
12 | | scmatmhm.t |
. . . 4
β’ π = (mulGrpβπ) |
13 | 12 | ringmgp 20133 |
. . 3
β’ (π β Ring β π β Mnd) |
14 | 9, 11, 13 | 3syl 18 |
. 2
β’ ((π β Fin β§ π
β Ring) β π β Mnd) |
15 | | scmatrhmval.o |
. . . . 5
β’ 1 =
(1rβπ΄) |
16 | | scmatrhmval.t |
. . . . 5
β’ β = (
Β·π βπ΄) |
17 | | scmatrhmval.f |
. . . . 5
β’ πΉ = (π₯ β πΎ β¦ (π₯ β 1 )) |
18 | 6, 4, 15, 16, 17, 8 | scmatf 22251 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β πΉ:πΎβΆπΆ) |
19 | 4, 8, 10 | scmatstrbas 22248 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β
(Baseβπ) = πΆ) |
20 | 19 | feq3d 6704 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β (πΉ:πΎβΆ(Baseβπ) β πΉ:πΎβΆπΆ)) |
21 | 18, 20 | mpbird 256 |
. . 3
β’ ((π β Fin β§ π
β Ring) β πΉ:πΎβΆ(Baseβπ)) |
22 | | eqid 2732 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
23 | | eqid 2732 |
. . . . . . 7
β’
(.rβπ΄) = (.rβπ΄) |
24 | 4, 6, 7, 15, 16, 22, 23 | scmatscmiddistr 22230 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((π¦ β 1
)(.rβπ΄)(π§ β 1 )) = ((π¦(.rβπ
)π§) β 1 )) |
25 | 10, 23 | ressmulr 17256 |
. . . . . . . . 9
β’ (πΆ β (SubRingβπ΄) β
(.rβπ΄) =
(.rβπ)) |
26 | 9, 25 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β
(.rβπ΄) =
(.rβπ)) |
27 | 26 | adantr 481 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (.rβπ΄) = (.rβπ)) |
28 | 27 | oveqd 7428 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((π¦ β 1
)(.rβπ΄)(π§ β 1 )) = ((π¦ β 1
)(.rβπ)(π§ β 1 ))) |
29 | 24, 28 | eqtr3d 2774 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((π¦(.rβπ
)π§) β 1 ) = ((π¦ β 1
)(.rβπ)(π§ β 1 ))) |
30 | | simpr 485 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β π
β Ring) |
31 | 30 | adantr 481 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β π
β Ring) |
32 | 30 | anim1i 615 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (π
β Ring β§ (π¦ β πΎ β§ π§ β πΎ))) |
33 | | 3anass 1095 |
. . . . . . . 8
β’ ((π
β Ring β§ π¦ β πΎ β§ π§ β πΎ) β (π
β Ring β§ (π¦ β πΎ β§ π§ β πΎ))) |
34 | 32, 33 | sylibr 233 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (π
β Ring β§ π¦ β πΎ β§ π§ β πΎ)) |
35 | 6, 22 | ringcl 20144 |
. . . . . . 7
β’ ((π
β Ring β§ π¦ β πΎ β§ π§ β πΎ) β (π¦(.rβπ
)π§) β πΎ) |
36 | 34, 35 | syl 17 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (π¦(.rβπ
)π§) β πΎ) |
37 | 6, 4, 15, 16, 17 | scmatrhmval 22249 |
. . . . . 6
β’ ((π
β Ring β§ (π¦(.rβπ
)π§) β πΎ) β (πΉβ(π¦(.rβπ
)π§)) = ((π¦(.rβπ
)π§) β 1 )) |
38 | 31, 36, 37 | syl2anc 584 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (πΉβ(π¦(.rβπ
)π§)) = ((π¦(.rβπ
)π§) β 1 )) |
39 | 6, 4, 15, 16, 17 | scmatrhmval 22249 |
. . . . . . 7
β’ ((π
β Ring β§ π¦ β πΎ) β (πΉβπ¦) = (π¦ β 1 )) |
40 | 39 | ad2ant2lr 746 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (πΉβπ¦) = (π¦ β 1 )) |
41 | 6, 4, 15, 16, 17 | scmatrhmval 22249 |
. . . . . . 7
β’ ((π
β Ring β§ π§ β πΎ) β (πΉβπ§) = (π§ β 1 )) |
42 | 41 | ad2ant2l 744 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (πΉβπ§) = (π§ β 1 )) |
43 | 40, 42 | oveq12d 7429 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((πΉβπ¦)(.rβπ)(πΉβπ§)) = ((π¦ β 1
)(.rβπ)(π§ β 1 ))) |
44 | 29, 38, 43 | 3eqtr4d 2782 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (πΉβ(π¦(.rβπ
)π§)) = ((πΉβπ¦)(.rβπ)(πΉβπ§))) |
45 | 44 | ralrimivva 3200 |
. . 3
β’ ((π β Fin β§ π
β Ring) β
βπ¦ β πΎ βπ§ β πΎ (πΉβ(π¦(.rβπ
)π§)) = ((πΉβπ¦)(.rβπ)(πΉβπ§))) |
46 | | eqid 2732 |
. . . . . . 7
β’
(1rβπ
) = (1rβπ
) |
47 | 6, 46 | ringidcl 20154 |
. . . . . 6
β’ (π
β Ring β
(1rβπ
)
β πΎ) |
48 | 6, 4, 15, 16, 17 | scmatrhmval 22249 |
. . . . . 6
β’ ((π
β Ring β§
(1rβπ
)
β πΎ) β (πΉβ(1rβπ
)) = ((1rβπ
) β 1 )) |
49 | 30, 47, 48 | syl2anc2 585 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β (πΉβ(1rβπ
)) = ((1rβπ
) β 1 )) |
50 | 4 | matsca2 22142 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β π
= (Scalarβπ΄)) |
51 | 50 | fveq2d 6895 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β
(1rβπ
) =
(1rβ(Scalarβπ΄))) |
52 | 51 | oveq1d 7426 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β
((1rβπ
)
β
1 ) =
((1rβ(Scalarβπ΄)) β 1 )) |
53 | 4 | matlmod 22151 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β π΄ β LMod) |
54 | 4 | matring 22165 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
55 | 5, 15 | ringidcl 20154 |
. . . . . . . 8
β’ (π΄ β Ring β 1 β
(Baseβπ΄)) |
56 | 54, 55 | syl 17 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β 1 β
(Baseβπ΄)) |
57 | | eqid 2732 |
. . . . . . . 8
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
58 | | eqid 2732 |
. . . . . . . 8
β’
(1rβ(Scalarβπ΄)) =
(1rβ(Scalarβπ΄)) |
59 | 5, 57, 16, 58 | lmodvs1 20644 |
. . . . . . 7
β’ ((π΄ β LMod β§ 1 β
(Baseβπ΄)) β
((1rβ(Scalarβπ΄)) β 1 ) = 1 ) |
60 | 53, 56, 59 | syl2anc 584 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β
((1rβ(Scalarβπ΄)) β 1 ) = 1 ) |
61 | 52, 60 | eqtrd 2772 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β
((1rβπ
)
β
1 ) =
1
) |
62 | 49, 61 | eqtrd 2772 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β (πΉβ(1rβπ
)) = 1 ) |
63 | 10, 15 | subrg1 20472 |
. . . . 5
β’ (πΆ β (SubRingβπ΄) β 1 =
(1rβπ)) |
64 | 9, 63 | syl 17 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β 1 =
(1rβπ)) |
65 | 62, 64 | eqtrd 2772 |
. . 3
β’ ((π β Fin β§ π
β Ring) β (πΉβ(1rβπ
)) = (1rβπ)) |
66 | 21, 45, 65 | 3jca 1128 |
. 2
β’ ((π β Fin β§ π
β Ring) β (πΉ:πΎβΆ(Baseβπ) β§ βπ¦ β πΎ βπ§ β πΎ (πΉβ(π¦(.rβπ
)π§)) = ((πΉβπ¦)(.rβπ)(πΉβπ§)) β§ (πΉβ(1rβπ
)) = (1rβπ))) |
67 | 1, 6 | mgpbas 20034 |
. . 3
β’ πΎ = (Baseβπ) |
68 | | eqid 2732 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
69 | 12, 68 | mgpbas 20034 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
70 | 1, 22 | mgpplusg 20032 |
. . 3
β’
(.rβπ
) = (+gβπ) |
71 | | eqid 2732 |
. . . 4
β’
(.rβπ) = (.rβπ) |
72 | 12, 71 | mgpplusg 20032 |
. . 3
β’
(.rβπ) = (+gβπ) |
73 | 1, 46 | ringidval 20077 |
. . 3
β’
(1rβπ
) = (0gβπ) |
74 | | eqid 2732 |
. . . 4
β’
(1rβπ) = (1rβπ) |
75 | 12, 74 | ringidval 20077 |
. . 3
β’
(1rβπ) = (0gβπ) |
76 | 67, 69, 70, 72, 73, 75 | ismhm 18707 |
. 2
β’ (πΉ β (π MndHom π) β ((π β Mnd β§ π β Mnd) β§ (πΉ:πΎβΆ(Baseβπ) β§ βπ¦ β πΎ βπ§ β πΎ (πΉβ(π¦(.rβπ
)π§)) = ((πΉβπ¦)(.rβπ)(πΉβπ§)) β§ (πΉβ(1rβπ
)) = (1rβπ)))) |
77 | 3, 14, 66, 76 | syl21anbrc 1344 |
1
β’ ((π β Fin β§ π
β Ring) β πΉ β (π MndHom π)) |