Step | Hyp | Ref
| Expression |
1 | | mat2pmatbas.b |
. 2
β’ π΅ = (Baseβπ΄) |
2 | | mat2pmatbas0.h |
. 2
β’ π» = (BaseβπΆ) |
3 | | eqid 2724 |
. 2
β’
(+gβπ΄) = (+gβπ΄) |
4 | | eqid 2724 |
. 2
β’
(+gβπΆ) = (+gβπΆ) |
5 | | mat2pmatbas.a |
. . 3
β’ π΄ = (π Mat π
) |
6 | 5 | matgrp 22254 |
. 2
β’ ((π β Fin β§ π
β Ring) β π΄ β Grp) |
7 | | mat2pmatbas.p |
. . . 4
β’ π = (Poly1βπ
) |
8 | | mat2pmatbas.c |
. . . 4
β’ πΆ = (π Mat π) |
9 | 7, 8 | pmatring 22516 |
. . 3
β’ ((π β Fin β§ π
β Ring) β πΆ β Ring) |
10 | | ringgrp 20133 |
. . 3
β’ (πΆ β Ring β πΆ β Grp) |
11 | 9, 10 | syl 17 |
. 2
β’ ((π β Fin β§ π
β Ring) β πΆ β Grp) |
12 | | mat2pmatbas.t |
. . 3
β’ π = (π matToPolyMat π
) |
13 | 12, 5, 1, 7, 8, 2 | mat2pmatf 22552 |
. 2
β’ ((π β Fin β§ π
β Ring) β π:π΅βΆπ») |
14 | | eqid 2724 |
. . . . . 6
β’
(Baseβπ) =
(Baseβπ) |
15 | | simpl 482 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β π β Fin) |
16 | 15 | adantr 480 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β π β Fin) |
17 | 7 | ply1ring 22089 |
. . . . . . 7
β’ (π
β Ring β π β Ring) |
18 | 17 | ad2antlr 724 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β π β Ring) |
19 | | simp1lr 1234 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β π
β Ring) |
20 | | eqid 2724 |
. . . . . . . 8
β’
(Baseβπ
) =
(Baseβπ
) |
21 | | simp2 1134 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β π β π) |
22 | | simp3 1135 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β π β π) |
23 | | simp1rl 1235 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β π₯ β π΅) |
24 | 5, 20, 1, 21, 22, 23 | matecld 22250 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (ππ₯π) β (Baseβπ
)) |
25 | | eqid 2724 |
. . . . . . . 8
β’
(algScβπ) =
(algScβπ) |
26 | 7, 25, 20, 14 | ply1sclcl 22127 |
. . . . . . 7
β’ ((π
β Ring β§ (ππ₯π) β (Baseβπ
)) β ((algScβπ)β(ππ₯π)) β (Baseβπ)) |
27 | 19, 24, 26 | syl2anc 583 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((algScβπ)β(ππ₯π)) β (Baseβπ)) |
28 | 8, 14, 2, 16, 18, 27 | matbas2d 22247 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π, π β π β¦ ((algScβπ)β(ππ₯π))) β π») |
29 | | simp1rr 1236 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β π¦ β π΅) |
30 | 5, 20, 1, 21, 22, 29 | matecld 22250 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (ππ¦π) β (Baseβπ
)) |
31 | 7, 25, 20, 14 | ply1sclcl 22127 |
. . . . . . 7
β’ ((π
β Ring β§ (ππ¦π) β (Baseβπ
)) β ((algScβπ)β(ππ¦π)) β (Baseβπ)) |
32 | 19, 30, 31 | syl2anc 583 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((algScβπ)β(ππ¦π)) β (Baseβπ)) |
33 | 8, 14, 2, 16, 18, 32 | matbas2d 22247 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π, π β π β¦ ((algScβπ)β(ππ¦π))) β π») |
34 | | eqid 2724 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
35 | 8, 2, 4, 34 | matplusg2 22251 |
. . . . 5
β’ (((π β π, π β π β¦ ((algScβπ)β(ππ₯π))) β π» β§ (π β π, π β π β¦ ((algScβπ)β(ππ¦π))) β π») β ((π β π, π β π β¦ ((algScβπ)β(ππ₯π)))(+gβπΆ)(π β π, π β π β¦ ((algScβπ)β(ππ¦π)))) = ((π β π, π β π β¦ ((algScβπ)β(ππ₯π))) βf
(+gβπ)(π β π, π β π β¦ ((algScβπ)β(ππ¦π))))) |
36 | 28, 33, 35 | syl2anc 583 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π, π β π β¦ ((algScβπ)β(ππ₯π)))(+gβπΆ)(π β π, π β π β¦ ((algScβπ)β(ππ¦π)))) = ((π β π, π β π β¦ ((algScβπ)β(ππ₯π))) βf
(+gβπ)(π β π, π β π β¦ ((algScβπ)β(ππ¦π))))) |
37 | | fvexd 6896 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((algScβπ)β(ππ₯π)) β V) |
38 | | fvexd 6896 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((algScβπ)β(ππ¦π)) β V) |
39 | | eqidd 2725 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π, π β π β¦ ((algScβπ)β(ππ₯π))) = (π β π, π β π β¦ ((algScβπ)β(ππ₯π)))) |
40 | | eqidd 2725 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π, π β π β¦ ((algScβπ)β(ππ¦π))) = (π β π, π β π β¦ ((algScβπ)β(ππ¦π)))) |
41 | 16, 16, 37, 38, 39, 40 | offval22 8068 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π, π β π β¦ ((algScβπ)β(ππ₯π))) βf
(+gβπ)(π β π, π β π β¦ ((algScβπ)β(ππ¦π)))) = (π β π, π β π β¦ (((algScβπ)β(ππ₯π))(+gβπ)((algScβπ)β(ππ¦π))))) |
42 | | simpr 484 |
. . . . . . . . . . 11
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯ β π΅ β§ π¦ β π΅)) |
43 | 42 | 3ad2ant1 1130 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (π₯ β π΅ β§ π¦ β π΅)) |
44 | | 3simpc 1147 |
. . . . . . . . . 10
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (π β π β§ π β π)) |
45 | | eqid 2724 |
. . . . . . . . . . 11
β’
(+gβπ
) = (+gβπ
) |
46 | 5, 1, 3, 45 | matplusgcell 22257 |
. . . . . . . . . 10
β’ (((π₯ β π΅ β§ π¦ β π΅) β§ (π β π β§ π β π)) β (π(π₯(+gβπ΄)π¦)π) = ((ππ₯π)(+gβπ
)(ππ¦π))) |
47 | 43, 44, 46 | syl2anc 583 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (π(π₯(+gβπ΄)π¦)π) = ((ππ₯π)(+gβπ
)(ππ¦π))) |
48 | 7 | ply1sca 22094 |
. . . . . . . . . . . . . 14
β’ (π
β Ring β π
= (Scalarβπ)) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β π
= (Scalarβπ)) |
50 | 49 | fveq2d 6885 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β Ring) β
(+gβπ
) =
(+gβ(Scalarβπ))) |
51 | 50 | oveqd 7418 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring) β ((ππ₯π)(+gβπ
)(ππ¦π)) = ((ππ₯π)(+gβ(Scalarβπ))(ππ¦π))) |
52 | 51 | adantr 480 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((ππ₯π)(+gβπ
)(ππ¦π)) = ((ππ₯π)(+gβ(Scalarβπ))(ππ¦π))) |
53 | 52 | 3ad2ant1 1130 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((ππ₯π)(+gβπ
)(ππ¦π)) = ((ππ₯π)(+gβ(Scalarβπ))(ππ¦π))) |
54 | 47, 53 | eqtrd 2764 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (π(π₯(+gβπ΄)π¦)π) = ((ππ₯π)(+gβ(Scalarβπ))(ππ¦π))) |
55 | 54 | fveq2d 6885 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((algScβπ)β(π(π₯(+gβπ΄)π¦)π)) = ((algScβπ)β((ππ₯π)(+gβ(Scalarβπ))(ππ¦π)))) |
56 | | eqid 2724 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
57 | 18 | 3ad2ant1 1130 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β π β Ring) |
58 | 7 | ply1lmod 22093 |
. . . . . . . . . . 11
β’ (π
β Ring β π β LMod) |
59 | 58 | ad2antlr 724 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β π β LMod) |
60 | 59 | 3ad2ant1 1130 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β π β LMod) |
61 | 25, 56, 57, 60 | asclghm 21745 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (algScβπ) β ((Scalarβπ) GrpHom π)) |
62 | 49 | eqcomd 2730 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π
β Ring) β
(Scalarβπ) = π
) |
63 | 62 | fveq2d 6885 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β Ring) β
(Baseβ(Scalarβπ)) = (Baseβπ
)) |
64 | 63 | eleq2d 2811 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring) β ((ππ₯π) β (Baseβ(Scalarβπ)) β (ππ₯π) β (Baseβπ
))) |
65 | 64 | adantr 480 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((ππ₯π) β (Baseβ(Scalarβπ)) β (ππ₯π) β (Baseβπ
))) |
66 | 65 | 3ad2ant1 1130 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((ππ₯π) β (Baseβ(Scalarβπ)) β (ππ₯π) β (Baseβπ
))) |
67 | 24, 66 | mpbird 257 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (ππ₯π) β (Baseβ(Scalarβπ))) |
68 | 63 | eleq2d 2811 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring) β ((ππ¦π) β (Baseβ(Scalarβπ)) β (ππ¦π) β (Baseβπ
))) |
69 | 68 | adantr 480 |
. . . . . . . . . 10
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((ππ¦π) β (Baseβ(Scalarβπ)) β (ππ¦π) β (Baseβπ
))) |
70 | 69 | 3ad2ant1 1130 |
. . . . . . . . 9
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((ππ¦π) β (Baseβ(Scalarβπ)) β (ππ¦π) β (Baseβπ
))) |
71 | 30, 70 | mpbird 257 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (ππ¦π) β (Baseβ(Scalarβπ))) |
72 | | eqid 2724 |
. . . . . . . . 9
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
73 | | eqid 2724 |
. . . . . . . . 9
β’
(+gβ(Scalarβπ)) =
(+gβ(Scalarβπ)) |
74 | 72, 73, 34 | ghmlin 19136 |
. . . . . . . 8
β’
(((algScβπ)
β ((Scalarβπ)
GrpHom π) β§ (ππ₯π) β (Baseβ(Scalarβπ)) β§ (ππ¦π) β (Baseβ(Scalarβπ))) β ((algScβπ)β((ππ₯π)(+gβ(Scalarβπ))(ππ¦π))) = (((algScβπ)β(ππ₯π))(+gβπ)((algScβπ)β(ππ¦π)))) |
75 | 61, 67, 71, 74 | syl3anc 1368 |
. . . . . . 7
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β ((algScβπ)β((ππ₯π)(+gβ(Scalarβπ))(ππ¦π))) = (((algScβπ)β(ππ₯π))(+gβπ)((algScβπ)β(ππ¦π)))) |
76 | 55, 75 | eqtr2d 2765 |
. . . . . 6
β’ ((((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β§ π β π β§ π β π) β (((algScβπ)β(ππ₯π))(+gβπ)((algScβπ)β(ππ¦π))) = ((algScβπ)β(π(π₯(+gβπ΄)π¦)π))) |
77 | 76 | mpoeq3dva 7478 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π, π β π β¦ (((algScβπ)β(ππ₯π))(+gβπ)((algScβπ)β(ππ¦π)))) = (π β π, π β π β¦ ((algScβπ)β(π(π₯(+gβπ΄)π¦)π)))) |
78 | 41, 77 | eqtrd 2764 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β π, π β π β¦ ((algScβπ)β(ππ₯π))) βf
(+gβπ)(π β π, π β π β¦ ((algScβπ)β(ππ¦π)))) = (π β π, π β π β¦ ((algScβπ)β(π(π₯(+gβπ΄)π¦)π)))) |
79 | 36, 78 | eqtr2d 2765 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β π, π β π β¦ ((algScβπ)β(π(π₯(+gβπ΄)π¦)π))) = ((π β π, π β π β¦ ((algScβπ)β(ππ₯π)))(+gβπΆ)(π β π, π β π β¦ ((algScβπ)β(ππ¦π))))) |
80 | | simpl 482 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β Fin β§ π
β Ring)) |
81 | 5 | matring 22267 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring) β π΄ β Ring) |
82 | | ringmnd 20138 |
. . . . . . . . 9
β’ (π΄ β Ring β π΄ β Mnd) |
83 | 81, 82 | syl 17 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β π΄ β Mnd) |
84 | 83 | anim1i 614 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π΄ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅))) |
85 | | 3anass 1092 |
. . . . . . 7
β’ ((π΄ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π΄ β Mnd β§ (π₯ β π΅ β§ π¦ β π΅))) |
86 | 84, 85 | sylibr 233 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π΄ β Mnd β§ π₯ β π΅ β§ π¦ β π΅)) |
87 | 1, 3 | mndcl 18665 |
. . . . . 6
β’ ((π΄ β Mnd β§ π₯ β π΅ β§ π¦ β π΅) β (π₯(+gβπ΄)π¦) β π΅) |
88 | 86, 87 | syl 17 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ΄)π¦) β π΅) |
89 | | df-3an 1086 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ (π₯(+gβπ΄)π¦) β π΅) β ((π β Fin β§ π
β Ring) β§ (π₯(+gβπ΄)π¦) β π΅)) |
90 | 80, 88, 89 | sylanbrc 582 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β Fin β§ π
β Ring β§ (π₯(+gβπ΄)π¦) β π΅)) |
91 | 12, 5, 1, 7, 25 | mat2pmatval 22548 |
. . . 4
β’ ((π β Fin β§ π
β Ring β§ (π₯(+gβπ΄)π¦) β π΅) β (πβ(π₯(+gβπ΄)π¦)) = (π β π, π β π β¦ ((algScβπ)β(π(π₯(+gβπ΄)π¦)π)))) |
92 | 90, 91 | syl 17 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβ(π₯(+gβπ΄)π¦)) = (π β π, π β π β¦ ((algScβπ)β(π(π₯(+gβπ΄)π¦)π)))) |
93 | | simpl 482 |
. . . . . . 7
β’ ((π₯ β π΅ β§ π¦ β π΅) β π₯ β π΅) |
94 | 93 | anim2i 616 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β Fin β§ π
β Ring) β§ π₯ β π΅)) |
95 | | df-3an 1086 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π₯ β π΅) β ((π β Fin β§ π
β Ring) β§ π₯ β π΅)) |
96 | 94, 95 | sylibr 233 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β Fin β§ π
β Ring β§ π₯ β π΅)) |
97 | 12, 5, 1, 7, 25 | mat2pmatval 22548 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π₯ β π΅) β (πβπ₯) = (π β π, π β π β¦ ((algScβπ)β(ππ₯π)))) |
98 | 96, 97 | syl 17 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβπ₯) = (π β π, π β π β¦ ((algScβπ)β(ππ₯π)))) |
99 | | simpr 484 |
. . . . . . 7
β’ ((π₯ β π΅ β§ π¦ β π΅) β π¦ β π΅) |
100 | 99 | anim2i 616 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((π β Fin β§ π
β Ring) β§ π¦ β π΅)) |
101 | | df-3an 1086 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π¦ β π΅) β ((π β Fin β§ π
β Ring) β§ π¦ β π΅)) |
102 | 100, 101 | sylibr 233 |
. . . . 5
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (π β Fin β§ π
β Ring β§ π¦ β π΅)) |
103 | 12, 5, 1, 7, 25 | mat2pmatval 22548 |
. . . . 5
β’ ((π β Fin β§ π
β Ring β§ π¦ β π΅) β (πβπ¦) = (π β π, π β π β¦ ((algScβπ)β(ππ¦π)))) |
104 | 102, 103 | syl 17 |
. . . 4
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβπ¦) = (π β π, π β π β¦ ((algScβπ)β(ππ¦π)))) |
105 | 98, 104 | oveq12d 7419 |
. . 3
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β ((πβπ₯)(+gβπΆ)(πβπ¦)) = ((π β π, π β π β¦ ((algScβπ)β(ππ₯π)))(+gβπΆ)(π β π, π β π β¦ ((algScβπ)β(ππ¦π))))) |
106 | 79, 92, 105 | 3eqtr4d 2774 |
. 2
β’ (((π β Fin β§ π
β Ring) β§ (π₯ β π΅ β§ π¦ β π΅)) β (πβ(π₯(+gβπ΄)π¦)) = ((πβπ₯)(+gβπΆ)(πβπ¦))) |
107 | 1, 2, 3, 4, 6, 11,
13, 106 | isghmd 19140 |
1
β’ ((π β Fin β§ π
β Ring) β π β (π΄ GrpHom πΆ)) |