Step | Hyp | Ref
| Expression |
1 | | scmatrhmval.k |
. 2
β’ πΎ = (Baseβπ
) |
2 | | eqid 2733 |
. 2
β’
(Baseβπ) =
(Baseβπ) |
3 | | eqid 2733 |
. 2
β’
(+gβπ
) = (+gβπ
) |
4 | | eqid 2733 |
. 2
β’
(+gβπ) = (+gβπ) |
5 | | ringgrp 20061 |
. . 3
β’ (π
β Ring β π
β Grp) |
6 | 5 | adantl 483 |
. 2
β’ ((π β Fin β§ π
β Ring) β π
β Grp) |
7 | | scmatrhmval.a |
. . . 4
β’ π΄ = (π Mat π
) |
8 | | eqid 2733 |
. . . 4
β’
(Baseβπ΄) =
(Baseβπ΄) |
9 | | eqid 2733 |
. . . 4
β’
(0gβπ
) = (0gβπ
) |
10 | | scmatrhmval.c |
. . . 4
β’ πΆ = (π ScMat π
) |
11 | 7, 8, 1, 9, 10 | scmatsgrp 22021 |
. . 3
β’ ((π β Fin β§ π
β Ring) β πΆ β (SubGrpβπ΄)) |
12 | | scmatghm.s |
. . . 4
β’ π = (π΄ βΎs πΆ) |
13 | 12 | subggrp 19009 |
. . 3
β’ (πΆ β (SubGrpβπ΄) β π β Grp) |
14 | 11, 13 | syl 17 |
. 2
β’ ((π β Fin β§ π
β Ring) β π β Grp) |
15 | | scmatrhmval.o |
. . . 4
β’ 1 =
(1rβπ΄) |
16 | | scmatrhmval.t |
. . . 4
β’ β = (
Β·π βπ΄) |
17 | | scmatrhmval.f |
. . . 4
β’ πΉ = (π₯ β πΎ β¦ (π₯ β 1 )) |
18 | 1, 7, 15, 16, 17, 10 | scmatf 22031 |
. . 3
β’ ((π β Fin β§ π
β Ring) β πΉ:πΎβΆπΆ) |
19 | 7, 10, 12 | scmatstrbas 22028 |
. . . 4
β’ ((π β Fin β§ π
β Ring) β
(Baseβπ) = πΆ) |
20 | 19 | feq3d 6705 |
. . 3
β’ ((π β Fin β§ π
β Ring) β (πΉ:πΎβΆ(Baseβπ) β πΉ:πΎβΆπΆ)) |
21 | 18, 20 | mpbird 257 |
. 2
β’ ((π β Fin β§ π
β Ring) β πΉ:πΎβΆ(Baseβπ)) |
22 | 7 | matsca2 21922 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β π
= (Scalarβπ΄)) |
23 | 10 | ovexi 7443 |
. . . . . . . . . 10
β’ πΆ β V |
24 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Scalarβπ΄) =
(Scalarβπ΄) |
25 | 12, 24 | resssca 17288 |
. . . . . . . . . 10
β’ (πΆ β V β
(Scalarβπ΄) =
(Scalarβπ)) |
26 | 23, 25 | mp1i 13 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β
(Scalarβπ΄) =
(Scalarβπ)) |
27 | 22, 26 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β π
= (Scalarβπ)) |
28 | 27 | fveq2d 6896 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β
(+gβπ
) =
(+gβ(Scalarβπ))) |
29 | 28 | oveqd 7426 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β (π¦(+gβπ
)π§) = (π¦(+gβ(Scalarβπ))π§)) |
30 | 29 | oveq1d 7424 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β ((π¦(+gβπ
)π§) β 1 ) = ((π¦(+gβ(Scalarβπ))π§) β 1 )) |
31 | 30 | adantr 482 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((π¦(+gβπ
)π§) β 1 ) = ((π¦(+gβ(Scalarβπ))π§) β 1 )) |
32 | 7 | matlmod 21931 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β π΄ β LMod) |
33 | 7, 10 | scmatlss 22027 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β πΆ β (LSubSpβπ΄)) |
34 | | eqid 2733 |
. . . . . . . 8
β’
(LSubSpβπ΄) =
(LSubSpβπ΄) |
35 | 12, 34 | lsslmod 20571 |
. . . . . . 7
β’ ((π΄ β LMod β§ πΆ β (LSubSpβπ΄)) β π β LMod) |
36 | 32, 33, 35 | syl2anc 585 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β π β LMod) |
37 | 36 | adantr 482 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β π β LMod) |
38 | 27 | fveq2d 6896 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring) β
(Baseβπ
) =
(Baseβ(Scalarβπ))) |
39 | 1, 38 | eqtrid 2785 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β πΎ =
(Baseβ(Scalarβπ))) |
40 | 39 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β (π¦ β πΎ β π¦ β (Baseβ(Scalarβπ)))) |
41 | 40 | biimpd 228 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β (π¦ β πΎ β π¦ β (Baseβ(Scalarβπ)))) |
42 | 41 | adantrd 493 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β ((π¦ β πΎ β§ π§ β πΎ) β π¦ β (Baseβ(Scalarβπ)))) |
43 | 42 | imp 408 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β π¦ β (Baseβ(Scalarβπ))) |
44 | 39 | eleq2d 2820 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β (π§ β πΎ β π§ β (Baseβ(Scalarβπ)))) |
45 | 44 | biimpd 228 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β (π§ β πΎ β π§ β (Baseβ(Scalarβπ)))) |
46 | 45 | adantld 492 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β ((π¦ β πΎ β§ π§ β πΎ) β π§ β (Baseβ(Scalarβπ)))) |
47 | 46 | imp 408 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β π§ β (Baseβ(Scalarβπ))) |
48 | 7, 8, 1, 9, 10 | scmatid 22016 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β
(1rβπ΄)
β πΆ) |
49 | 15 | a1i 11 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β 1 =
(1rβπ΄)) |
50 | 48, 49, 19 | 3eltr4d 2849 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring) β 1 β
(Baseβπ)) |
51 | 50 | adantr 482 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β 1 β (Baseβπ)) |
52 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
53 | 12, 16 | ressvsca 17289 |
. . . . . . 7
β’ (πΆ β V β β = (
Β·π βπ)) |
54 | 23, 53 | ax-mp 5 |
. . . . . 6
β’ β = (
Β·π βπ) |
55 | | eqid 2733 |
. . . . . 6
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
56 | | eqid 2733 |
. . . . . 6
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
57 | 2, 4, 52, 54, 55, 56 | lmodvsdir 20496 |
. . . . 5
β’ ((π β LMod β§ (π¦ β
(Baseβ(Scalarβπ)) β§ π§ β (Baseβ(Scalarβπ)) β§ 1 β (Baseβπ))) β ((π¦(+gβ(Scalarβπ))π§) β 1 ) = ((π¦ β 1
)(+gβπ)(π§ β 1 ))) |
58 | 37, 43, 47, 51, 57 | syl13anc 1373 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((π¦(+gβ(Scalarβπ))π§) β 1 ) = ((π¦ β 1
)(+gβπ)(π§ β 1 ))) |
59 | 31, 58 | eqtrd 2773 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((π¦(+gβπ
)π§) β 1 ) = ((π¦ β 1
)(+gβπ)(π§ β 1 ))) |
60 | | simpr 486 |
. . . . 5
β’ ((π β Fin β§ π
β Ring) β π
β Ring) |
61 | 60 | adantr 482 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β π
β Ring) |
62 | 60 | anim1i 616 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (π
β Ring β§ (π¦ β πΎ β§ π§ β πΎ))) |
63 | | 3anass 1096 |
. . . . . 6
β’ ((π
β Ring β§ π¦ β πΎ β§ π§ β πΎ) β (π
β Ring β§ (π¦ β πΎ β§ π§ β πΎ))) |
64 | 62, 63 | sylibr 233 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (π
β Ring β§ π¦ β πΎ β§ π§ β πΎ)) |
65 | 1, 3 | ringacl 20095 |
. . . . 5
β’ ((π
β Ring β§ π¦ β πΎ β§ π§ β πΎ) β (π¦(+gβπ
)π§) β πΎ) |
66 | 64, 65 | syl 17 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (π¦(+gβπ
)π§) β πΎ) |
67 | 1, 7, 15, 16, 17 | scmatrhmval 22029 |
. . . 4
β’ ((π
β Ring β§ (π¦(+gβπ
)π§) β πΎ) β (πΉβ(π¦(+gβπ
)π§)) = ((π¦(+gβπ
)π§) β 1 )) |
68 | 61, 66, 67 | syl2anc 585 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (πΉβ(π¦(+gβπ
)π§)) = ((π¦(+gβπ
)π§) β 1 )) |
69 | 1, 7, 15, 16, 17 | scmatrhmval 22029 |
. . . . 5
β’ ((π
β Ring β§ π¦ β πΎ) β (πΉβπ¦) = (π¦ β 1 )) |
70 | 69 | ad2ant2lr 747 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (πΉβπ¦) = (π¦ β 1 )) |
71 | 1, 7, 15, 16, 17 | scmatrhmval 22029 |
. . . . 5
β’ ((π
β Ring β§ π§ β πΎ) β (πΉβπ§) = (π§ β 1 )) |
72 | 71 | ad2ant2l 745 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (πΉβπ§) = (π§ β 1 )) |
73 | 70, 72 | oveq12d 7427 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((πΉβπ¦)(+gβπ)(πΉβπ§)) = ((π¦ β 1
)(+gβπ)(π§ β 1 ))) |
74 | 59, 68, 73 | 3eqtr4d 2783 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π¦ β πΎ β§ π§ β πΎ)) β (πΉβ(π¦(+gβπ
)π§)) = ((πΉβπ¦)(+gβπ)(πΉβπ§))) |
75 | 1, 2, 3, 4, 6, 14,
21, 74 | isghmd 19101 |
1
β’ ((π β Fin β§ π
β Ring) β πΉ β (π
GrpHom π)) |