Step | Hyp | Ref
| Expression |
1 | | simpl2 1193 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐
โ Ring) |
2 | | pmatcollpw1.c |
. . . 4
โข ๐ถ = (๐ Mat ๐) |
3 | | eqid 2733 |
. . . 4
โข
(Baseโ๐) =
(Baseโ๐) |
4 | | pmatcollpw1.b |
. . . 4
โข ๐ต = (Baseโ๐ถ) |
5 | | simprl 770 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
6 | | simprr 772 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
7 | | simpl3 1194 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐ต) |
8 | 2, 3, 4, 5, 6, 7 | matecld 21791 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐๐๐) โ (Baseโ๐)) |
9 | | pmatcollpw1.p |
. . . 4
โข ๐ = (Poly1โ๐
) |
10 | | pmatcollpw1.x |
. . . 4
โข ๐ = (var1โ๐
) |
11 | | pmatcollpw1.m |
. . . 4
โข ร = (
ยท๐ โ๐) |
12 | | eqid 2733 |
. . . 4
โข
(mulGrpโ๐) =
(mulGrpโ๐) |
13 | | eqid 2733 |
. . . 4
โข
(.gโ(mulGrpโ๐)) =
(.gโ(mulGrpโ๐)) |
14 | | eqid 2733 |
. . . 4
โข
(coe1โ(๐๐๐)) = (coe1โ(๐๐๐)) |
15 | 9, 10, 3, 11, 12, 13, 14 | ply1coe 21683 |
. . 3
โข ((๐
โ Ring โง (๐๐๐) โ (Baseโ๐)) โ (๐๐๐) = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐๐๐))โ๐) ร (๐(.gโ(mulGrpโ๐))๐))))) |
16 | 1, 8, 15 | syl2anc 585 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐๐๐) = (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐๐๐))โ๐) ร (๐(.gโ(mulGrpโ๐))๐))))) |
17 | 1 | adantr 482 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ โ0) โ ๐
โ Ring) |
18 | 7 | adantr 482 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ โ0) โ ๐ โ ๐ต) |
19 | | simpr 486 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ โ0) โ ๐ โ
โ0) |
20 | | simpr 486 |
. . . . . . . 8
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ โ ๐ โง ๐ โ ๐)) |
21 | 20 | adantr 482 |
. . . . . . 7
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ โ0) โ (๐ โ ๐ โง ๐ โ ๐)) |
22 | 9, 2, 4 | decpmate 22131 |
. . . . . . 7
โข (((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ โ0) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐(๐ decompPMat ๐)๐) = ((coe1โ(๐๐๐))โ๐)) |
23 | 17, 18, 19, 21, 22 | syl31anc 1374 |
. . . . . 6
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ โ0) โ (๐(๐ decompPMat ๐)๐) = ((coe1โ(๐๐๐))โ๐)) |
24 | 23 | eqcomd 2739 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ โ0) โ
((coe1โ(๐๐๐))โ๐) = (๐(๐ decompPMat ๐)๐)) |
25 | | pmatcollpw1.e |
. . . . . . . 8
โข โ =
(.gโ(mulGrpโ๐)) |
26 | 25 | eqcomi 2742 |
. . . . . . 7
โข
(.gโ(mulGrpโ๐)) = โ |
27 | 26 | oveqi 7371 |
. . . . . 6
โข (๐(.gโ(mulGrpโ๐))๐) = (๐ โ ๐) |
28 | 27 | a1i 11 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ โ0) โ (๐(.gโ(mulGrpโ๐))๐) = (๐ โ ๐)) |
29 | 24, 28 | oveq12d 7376 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โง ๐ โ โ0) โ
(((coe1โ(๐๐๐))โ๐) ร (๐(.gโ(mulGrpโ๐))๐)) = ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐))) |
30 | 29 | mpteq2dva 5206 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ โ โ0 โฆ
(((coe1โ(๐๐๐))โ๐) ร (๐(.gโ(mulGrpโ๐))๐))) = (๐ โ โ0 โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐)))) |
31 | 30 | oveq2d 7374 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐ ฮฃg (๐ โ โ0
โฆ (((coe1โ(๐๐๐))โ๐) ร (๐(.gโ(mulGrpโ๐))๐)))) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐))))) |
32 | 16, 31 | eqtrd 2773 |
1
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ โ ๐ โง ๐ โ ๐)) โ (๐๐๐) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐(๐ decompPMat ๐)๐) ร (๐ โ ๐))))) |