Step | Hyp | Ref
| Expression |
1 | | pm2mpfo.b |
. 2
โข ๐ต = (Baseโ๐ถ) |
2 | | pm2mpfo.l |
. 2
โข ๐ฟ = (Baseโ๐) |
3 | | eqid 2733 |
. 2
โข
(+gโ๐ถ) = (+gโ๐ถ) |
4 | | eqid 2733 |
. 2
โข
(+gโ๐) = (+gโ๐) |
5 | | pm2mpfo.p |
. . . 4
โข ๐ = (Poly1โ๐
) |
6 | | pm2mpfo.c |
. . . 4
โข ๐ถ = (๐ Mat ๐) |
7 | 5, 6 | pmatring 22057 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ Ring) |
8 | | ringgrp 19974 |
. . 3
โข (๐ถ โ Ring โ ๐ถ โ Grp) |
9 | 7, 8 | syl 17 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ Grp) |
10 | | pm2mpfo.a |
. . . . 5
โข ๐ด = (๐ Mat ๐
) |
11 | 10 | matring 21808 |
. . . 4
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
12 | | pm2mpfo.q |
. . . . 5
โข ๐ = (Poly1โ๐ด) |
13 | 12 | ply1ring 21635 |
. . . 4
โข (๐ด โ Ring โ ๐ โ Ring) |
14 | 11, 13 | syl 17 |
. . 3
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ Ring) |
15 | | ringgrp 19974 |
. . 3
โข (๐ โ Ring โ ๐ โ Grp) |
16 | 14, 15 | syl 17 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ Grp) |
17 | | pm2mpfo.m |
. . 3
โข โ = (
ยท๐ โ๐) |
18 | | pm2mpfo.e |
. . 3
โข โ =
(.gโ(mulGrpโ๐)) |
19 | | pm2mpfo.x |
. . 3
โข ๐ = (var1โ๐ด) |
20 | | pm2mpfo.t |
. . 3
โข ๐ = (๐ pMatToMatPoly ๐
) |
21 | 5, 6, 1, 17, 18, 19, 10, 12, 20, 2 | pm2mpf 22163 |
. 2
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐:๐ตโถ๐ฟ) |
22 | | ringmnd 19979 |
. . . . . . . . . . . . . 14
โข (๐ถ โ Ring โ ๐ถ โ Mnd) |
23 | 7, 22 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ถ โ Mnd) |
24 | 23 | anim1i 616 |
. . . . . . . . . . . 12
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ถ โ Mnd โง (๐ โ ๐ต โง ๐ โ ๐ต))) |
25 | | 3anass 1096 |
. . . . . . . . . . . 12
โข ((๐ถ โ Mnd โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ถ โ Mnd โง (๐ โ ๐ต โง ๐ โ ๐ต))) |
26 | 24, 25 | sylibr 233 |
. . . . . . . . . . 11
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ถ โ Mnd โง ๐ โ ๐ต โง ๐ โ ๐ต)) |
27 | 1, 3 | mndcl 18569 |
. . . . . . . . . . 11
โข ((๐ถ โ Mnd โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐(+gโ๐ถ)๐) โ ๐ต) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐(+gโ๐ถ)๐) โ ๐ต) |
29 | 6, 1 | decpmatval 22130 |
. . . . . . . . . 10
โข (((๐(+gโ๐ถ)๐) โ ๐ต โง ๐ โ โ0) โ ((๐(+gโ๐ถ)๐) decompPMat ๐) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐(+gโ๐ถ)๐)๐))โ๐))) |
30 | 28, 29 | sylan 581 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐(+gโ๐ถ)๐) decompPMat ๐) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐(+gโ๐ถ)๐)๐))โ๐))) |
31 | | simplll 774 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ Fin) |
32 | | fvexd 6858 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐๐๐))โ๐) โ V) |
33 | | fvexd 6858 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐๐๐))โ๐) โ V) |
34 | | eqidd 2734 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) |
35 | | eqidd 2734 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) |
36 | 31, 31, 32, 33, 34, 35 | offval22 8021 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) โf
(+gโ๐
)(๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) = (๐ โ ๐, ๐ โ ๐ โฆ (((coe1โ(๐๐๐))โ๐)(+gโ๐
)((coe1โ(๐๐๐))โ๐)))) |
37 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(Baseโ๐
) =
(Baseโ๐
) |
38 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(Baseโ๐ด) =
(Baseโ๐ด) |
39 | | simpllr 775 |
. . . . . . . . . . . 12
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐
โ Ring) |
40 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
41 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
42 | 1 | eleq2i 2826 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐ถ)) |
43 | 42 | biimpi 215 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐ถ)) |
44 | 43 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ (Baseโ๐ถ)) |
45 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
โข
(Baseโ๐) =
(Baseโ๐) |
46 | 6, 45 | matecl 21790 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ (Baseโ๐ถ)) โ (๐๐๐) โ (Baseโ๐)) |
47 | 40, 41, 44, 46 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐๐๐) โ (Baseโ๐)) |
48 | 47 | ex 414 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โ ((๐ โ ๐ โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐))) |
49 | 48 | adantrr 716 |
. . . . . . . . . . . . . . 15
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐ โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐))) |
50 | 49 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐ โ ๐ โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐))) |
51 | 50 | 3impib 1117 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐)) |
52 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ
โ0) |
53 | 52 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐ โ โ0) |
54 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข
(coe1โ(๐๐๐)) = (coe1โ(๐๐๐)) |
55 | 54, 45, 5, 37 | coe1fvalcl 21599 |
. . . . . . . . . . . . 13
โข (((๐๐๐) โ (Baseโ๐) โง ๐ โ โ0) โ
((coe1โ(๐๐๐))โ๐) โ (Baseโ๐
)) |
56 | 51, 53, 55 | syl2anc 585 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐๐๐))โ๐) โ (Baseโ๐
)) |
57 | 10, 37, 38, 31, 39, 56 | matbas2d 21788 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) โ (Baseโ๐ด)) |
58 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
59 | | simprr 772 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
60 | 1 | eleq2i 2826 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐ถ)) |
61 | 60 | biimpi 215 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐ต โ ๐ โ (Baseโ๐ถ)) |
62 | 61 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ (Baseโ๐ถ)) |
63 | 6, 45 | matecl 21790 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ ๐ โง ๐ โ ๐ โง ๐ โ (Baseโ๐ถ)) โ (๐๐๐) โ (Baseโ๐)) |
64 | 58, 59, 62, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐๐๐) โ (Baseโ๐)) |
65 | 64 | ex 414 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต) โ ((๐ โ ๐ โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐))) |
66 | 65 | adantrl 715 |
. . . . . . . . . . . . . . 15
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐ โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐))) |
67 | 66 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐ โ ๐ โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐))) |
68 | 67 | 3impib 1117 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐๐๐) โ (Baseโ๐)) |
69 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข
(coe1โ(๐๐๐)) = (coe1โ(๐๐๐)) |
70 | 69, 45, 5, 37 | coe1fvalcl 21599 |
. . . . . . . . . . . . 13
โข (((๐๐๐) โ (Baseโ๐) โง ๐ โ โ0) โ
((coe1โ(๐๐๐))โ๐) โ (Baseโ๐
)) |
71 | 68, 53, 70 | syl2anc 585 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐๐๐))โ๐) โ (Baseโ๐
)) |
72 | 10, 37, 38, 31, 39, 71 | matbas2d 21788 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) โ (Baseโ๐ด)) |
73 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(+gโ๐ด) = (+gโ๐ด) |
74 | | eqid 2733 |
. . . . . . . . . . . 12
โข
(+gโ๐
) = (+gโ๐
) |
75 | 10, 38, 73, 74 | matplusg2 21792 |
. . . . . . . . . . 11
โข (((๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) โ (Baseโ๐ด) โง (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) โ (Baseโ๐ด)) โ ((๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))(+gโ๐ด)(๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) = ((๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) โf
(+gโ๐
)(๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)))) |
76 | 57, 72, 75 | syl2anc 585 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))(+gโ๐ด)(๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) = ((๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) โf
(+gโ๐
)(๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)))) |
77 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐ต โง ๐ โ ๐ต)) |
78 | 77 | anim1i 616 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง (๐ โ ๐ โง ๐ โ ๐)) โ ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐))) |
79 | 78 | 3impb 1116 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐))) |
80 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
โข
(+gโ๐) = (+gโ๐) |
81 | 6, 1, 3, 80 | matplusgcell 21798 |
. . . . . . . . . . . . . . 15
โข (((๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐(+gโ๐ถ)๐)๐) = ((๐๐๐)(+gโ๐)(๐๐๐))) |
82 | 79, 81 | syl 17 |
. . . . . . . . . . . . . 14
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐(๐(+gโ๐ถ)๐)๐) = ((๐๐๐)(+gโ๐)(๐๐๐))) |
83 | 82 | fveq2d 6847 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ (coe1โ(๐(๐(+gโ๐ถ)๐)๐)) = (coe1โ((๐๐๐)(+gโ๐)(๐๐๐)))) |
84 | 83 | fveq1d 6845 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐(๐(+gโ๐ถ)๐)๐))โ๐) = ((coe1โ((๐๐๐)(+gโ๐)(๐๐๐)))โ๐)) |
85 | 39 | 3ad2ant1 1134 |
. . . . . . . . . . . . 13
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ๐
โ Ring) |
86 | 5, 45, 80, 74 | coe1addfv 21652 |
. . . . . . . . . . . . 13
โข (((๐
โ Ring โง (๐๐๐) โ (Baseโ๐) โง (๐๐๐) โ (Baseโ๐)) โง ๐ โ โ0) โ
((coe1โ((๐๐๐)(+gโ๐)(๐๐๐)))โ๐) = (((coe1โ(๐๐๐))โ๐)(+gโ๐
)((coe1โ(๐๐๐))โ๐))) |
87 | 85, 51, 68, 53, 86 | syl31anc 1374 |
. . . . . . . . . . . 12
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ((๐๐๐)(+gโ๐)(๐๐๐)))โ๐) = (((coe1โ(๐๐๐))โ๐)(+gโ๐
)((coe1โ(๐๐๐))โ๐))) |
88 | 84, 87 | eqtrd 2773 |
. . . . . . . . . . 11
โข
(((((๐ โ Fin
โง ๐
โ Ring) โง
(๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โง ๐ โ ๐ โง ๐ โ ๐) โ ((coe1โ(๐(๐(+gโ๐ถ)๐)๐))โ๐) = (((coe1โ(๐๐๐))โ๐)(+gโ๐
)((coe1โ(๐๐๐))โ๐))) |
89 | 88 | mpoeq3dva 7435 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐(+gโ๐ถ)๐)๐))โ๐)) = (๐ โ ๐, ๐ โ ๐ โฆ (((coe1โ(๐๐๐))โ๐)(+gโ๐
)((coe1โ(๐๐๐))โ๐)))) |
90 | 36, 76, 89 | 3eqtr4rd 2784 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐(๐(+gโ๐ถ)๐)๐))โ๐)) = ((๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))(+gโ๐ด)(๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)))) |
91 | 12 | ply1sca 21640 |
. . . . . . . . . . . . 13
โข (๐ด โ Ring โ ๐ด = (Scalarโ๐)) |
92 | 11, 91 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด = (Scalarโ๐)) |
93 | 92 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ด = (Scalarโ๐)) |
94 | 93 | fveq2d 6847 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ
(+gโ๐ด) =
(+gโ(Scalarโ๐))) |
95 | | simprl 770 |
. . . . . . . . . . . 12
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
96 | 6, 1 | decpmatval 22130 |
. . . . . . . . . . . 12
โข ((๐ โ ๐ต โง ๐ โ โ0) โ (๐ decompPMat ๐) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) |
97 | 95, 96 | sylan 581 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ decompPMat ๐) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) |
98 | 97 | eqcomd 2739 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) = (๐ decompPMat ๐)) |
99 | | simprr 772 |
. . . . . . . . . . . 12
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ ๐ต) |
100 | 6, 1 | decpmatval 22130 |
. . . . . . . . . . . 12
โข ((๐ โ ๐ต โง ๐ โ โ0) โ (๐ decompPMat ๐) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) |
101 | 99, 100 | sylan 581 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ decompPMat ๐) = (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) |
102 | 101 | eqcomd 2739 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐)) = (๐ decompPMat ๐)) |
103 | 94, 98, 102 | oveq123d 7379 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))(+gโ๐ด)(๐ โ ๐, ๐ โ ๐ โฆ ((coe1โ(๐๐๐))โ๐))) = ((๐ decompPMat ๐)(+gโ(Scalarโ๐))(๐ decompPMat ๐))) |
104 | 30, 90, 103 | 3eqtrd 2777 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐(+gโ๐ถ)๐) decompPMat ๐) = ((๐ decompPMat ๐)(+gโ(Scalarโ๐))(๐ decompPMat ๐))) |
105 | 104 | oveq1d 7373 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (((๐(+gโ๐ถ)๐) decompPMat ๐) โ (๐ โ ๐)) = (((๐ decompPMat ๐)(+gโ(Scalarโ๐))(๐ decompPMat ๐)) โ (๐ โ ๐))) |
106 | 12 | ply1lmod 21639 |
. . . . . . . . . 10
โข (๐ด โ Ring โ ๐ โ LMod) |
107 | 11, 106 | syl 17 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ LMod) |
108 | 107 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ LMod) |
109 | | simpl 484 |
. . . . . . . . . . 11
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
110 | 109 | ad2antlr 726 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ ๐ต) |
111 | 5, 6, 1, 10, 38 | decpmatcl 22132 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ โ0) โ (๐ decompPMat ๐) โ (Baseโ๐ด)) |
112 | 39, 110, 52, 111 | syl3anc 1372 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ decompPMat ๐) โ (Baseโ๐ด)) |
113 | 92 | eqcomd 2739 |
. . . . . . . . . . 11
โข ((๐ โ Fin โง ๐
โ Ring) โ
(Scalarโ๐) = ๐ด) |
114 | 113 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ
(Scalarโ๐) = ๐ด) |
115 | 114 | fveq2d 6847 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ
(Baseโ(Scalarโ๐)) = (Baseโ๐ด)) |
116 | 112, 115 | eleqtrrd 2837 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ decompPMat ๐) โ (Baseโ(Scalarโ๐))) |
117 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
118 | 117 | ad2antlr 726 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ ๐ต) |
119 | 5, 6, 1, 10, 38 | decpmatcl 22132 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ โ0) โ (๐ decompPMat ๐) โ (Baseโ๐ด)) |
120 | 39, 118, 52, 119 | syl3anc 1372 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ decompPMat ๐) โ (Baseโ๐ด)) |
121 | 120, 115 | eleqtrrd 2837 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ decompPMat ๐) โ (Baseโ(Scalarโ๐))) |
122 | | eqid 2733 |
. . . . . . . . . 10
โข
(mulGrpโ๐) =
(mulGrpโ๐) |
123 | 122, 2 | mgpbas 19907 |
. . . . . . . . 9
โข ๐ฟ =
(Baseโ(mulGrpโ๐)) |
124 | 122 | ringmgp 19975 |
. . . . . . . . . . 11
โข (๐ โ Ring โ
(mulGrpโ๐) โ
Mnd) |
125 | 14, 124 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ
(mulGrpโ๐) โ
Mnd) |
126 | 125 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ
(mulGrpโ๐) โ
Mnd) |
127 | 19, 12, 2 | vr1cl 21604 |
. . . . . . . . . . 11
โข (๐ด โ Ring โ ๐ โ ๐ฟ) |
128 | 11, 127 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ ๐ฟ) |
129 | 128 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ๐ โ ๐ฟ) |
130 | 123, 18, 126, 52, 129 | mulgnn0cld 18902 |
. . . . . . . 8
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (๐ โ ๐) โ ๐ฟ) |
131 | | eqid 2733 |
. . . . . . . . 9
โข
(Scalarโ๐) =
(Scalarโ๐) |
132 | | eqid 2733 |
. . . . . . . . 9
โข
(Baseโ(Scalarโ๐)) = (Baseโ(Scalarโ๐)) |
133 | | eqid 2733 |
. . . . . . . . 9
โข
(+gโ(Scalarโ๐)) =
(+gโ(Scalarโ๐)) |
134 | 2, 4, 131, 17, 132, 133 | lmodvsdir 20361 |
. . . . . . . 8
โข ((๐ โ LMod โง ((๐ decompPMat ๐) โ (Baseโ(Scalarโ๐)) โง (๐ decompPMat ๐) โ (Baseโ(Scalarโ๐)) โง (๐ โ ๐) โ ๐ฟ)) โ (((๐ decompPMat ๐)(+gโ(Scalarโ๐))(๐ decompPMat ๐)) โ (๐ โ ๐)) = (((๐ decompPMat ๐) โ (๐ โ ๐))(+gโ๐)((๐ decompPMat ๐) โ (๐ โ ๐)))) |
135 | 108, 116,
121, 130, 134 | syl13anc 1373 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (((๐ decompPMat ๐)(+gโ(Scalarโ๐))(๐ decompPMat ๐)) โ (๐ โ ๐)) = (((๐ decompPMat ๐) โ (๐ โ ๐))(+gโ๐)((๐ decompPMat ๐) โ (๐ โ ๐)))) |
136 | 105, 135 | eqtrd 2773 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ (((๐(+gโ๐ถ)๐) decompPMat ๐) โ (๐ โ ๐)) = (((๐ decompPMat ๐) โ (๐ โ ๐))(+gโ๐)((๐ decompPMat ๐) โ (๐ โ ๐)))) |
137 | 136 | mpteq2dva 5206 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ โ0 โฆ (((๐(+gโ๐ถ)๐) decompPMat ๐) โ (๐ โ ๐))) = (๐ โ โ0 โฆ (((๐ decompPMat ๐) โ (๐ โ ๐))(+gโ๐)((๐ decompPMat ๐) โ (๐ โ ๐))))) |
138 | 137 | oveq2d 7374 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ฮฃg (๐ โ โ0
โฆ (((๐(+gโ๐ถ)๐) decompPMat ๐) โ (๐ โ ๐)))) = (๐ ฮฃg (๐ โ โ0
โฆ (((๐ decompPMat
๐) โ (๐ โ ๐))(+gโ๐)((๐ decompPMat ๐) โ (๐ โ ๐)))))) |
139 | | eqid 2733 |
. . . . 5
โข
(0gโ๐) = (0gโ๐) |
140 | | ringcmn 20008 |
. . . . . . 7
โข (๐ โ Ring โ ๐ โ CMnd) |
141 | 14, 140 | syl 17 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ CMnd) |
142 | 141 | adantr 482 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ CMnd) |
143 | | nn0ex 12424 |
. . . . . 6
โข
โ0 โ V |
144 | 143 | a1i 11 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ โ0 โ
V) |
145 | 109 | anim2i 618 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต)) |
146 | | df-3an 1090 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต)) |
147 | 145, 146 | sylibr 233 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต)) |
148 | 5, 6, 1, 17, 18, 19, 10, 12, 2 | pm2mpghmlem1 22178 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ ((๐ decompPMat ๐) โ (๐ โ ๐)) โ ๐ฟ) |
149 | 147, 148 | sylan 581 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐ decompPMat ๐) โ (๐ โ ๐)) โ ๐ฟ) |
150 | 117 | anim2i 618 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต)) |
151 | | df-3an 1090 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ((๐ โ Fin โง ๐
โ Ring) โง ๐ โ ๐ต)) |
152 | 150, 151 | sylibr 233 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต)) |
153 | 5, 6, 1, 17, 18, 19, 10, 12, 2 | pm2mpghmlem1 22178 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง ๐ โ โ0) โ ((๐ decompPMat ๐) โ (๐ โ ๐)) โ ๐ฟ) |
154 | 152, 153 | sylan 581 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โง ๐ โ โ0) โ ((๐ decompPMat ๐) โ (๐ โ ๐)) โ ๐ฟ) |
155 | | eqidd 2734 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))) = (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐)))) |
156 | | eqidd 2734 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))) = (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐)))) |
157 | 5, 6, 1, 17, 18, 19, 10, 12 | pm2mpghmlem2 22177 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))) finSupp (0gโ๐)) |
158 | 147, 157 | syl 17 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))) finSupp (0gโ๐)) |
159 | 5, 6, 1, 17, 18, 19, 10, 12 | pm2mpghmlem2 22177 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))) finSupp (0gโ๐)) |
160 | 152, 159 | syl 17 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐))) finSupp (0gโ๐)) |
161 | 2, 139, 4, 142, 144, 149, 154, 155, 156, 158, 160 | gsummptfsadd 19706 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ฮฃg (๐ โ โ0
โฆ (((๐ decompPMat
๐) โ (๐ โ ๐))(+gโ๐)((๐ decompPMat ๐) โ (๐ โ ๐))))) = ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))(+gโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐)))))) |
162 | 138, 161 | eqtrd 2773 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ฮฃg (๐ โ โ0
โฆ (((๐(+gโ๐ถ)๐) decompPMat ๐) โ (๐ โ ๐)))) = ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))(+gโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐)))))) |
163 | | simpll 766 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐ โ Fin) |
164 | | simplr 768 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ๐
โ Ring) |
165 | 5, 6, 1, 17, 18, 19, 10, 12, 20 | pm2mpfval 22161 |
. . . 4
โข ((๐ โ Fin โง ๐
โ Ring โง (๐(+gโ๐ถ)๐) โ ๐ต) โ (๐โ(๐(+gโ๐ถ)๐)) = (๐ ฮฃg (๐ โ โ0
โฆ (((๐(+gโ๐ถ)๐) decompPMat ๐) โ (๐ โ ๐))))) |
166 | 163, 164,
28, 165 | syl3anc 1372 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐โ(๐(+gโ๐ถ)๐)) = (๐ ฮฃg (๐ โ โ0
โฆ (((๐(+gโ๐ถ)๐) decompPMat ๐) โ (๐ โ ๐))))) |
167 | 5, 6, 1, 17, 18, 19, 10, 12, 20 | pm2mpfval 22161 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐โ๐) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))) |
168 | 163, 164,
95, 167 | syl3anc 1372 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐โ๐) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))) |
169 | 5, 6, 1, 17, 18, 19, 10, 12, 20 | pm2mpfval 22161 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐โ๐) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))) |
170 | 163, 164,
99, 169 | syl3anc 1372 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐โ๐) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))) |
171 | 168, 170 | oveq12d 7376 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐โ๐)(+gโ๐)(๐โ๐)) = ((๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))(+gโ๐)(๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐)))))) |
172 | 162, 166,
171 | 3eqtr4d 2783 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐โ(๐(+gโ๐ถ)๐)) = ((๐โ๐)(+gโ๐)(๐โ๐))) |
173 | 1, 2, 3, 4, 9, 16,
21, 172 | isghmd 19022 |
1
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ (๐ถ GrpHom ๐)) |