Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ ๐ โ Fin) |
2 | | simplr 768 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ ๐
โ Ring) |
3 | | simprl 770 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ ๐ โ ๐ต) |
4 | | pm2mpval.p |
. . . . . 6
โข ๐ = (Poly1โ๐
) |
5 | | pm2mpval.c |
. . . . . 6
โข ๐ถ = (๐ Mat ๐) |
6 | | pm2mpval.b |
. . . . . 6
โข ๐ต = (Baseโ๐ถ) |
7 | | pm2mpval.m |
. . . . . 6
โข โ = (
ยท๐ โ๐) |
8 | | pm2mpval.e |
. . . . . 6
โข โ =
(.gโ(mulGrpโ๐)) |
9 | | pm2mpval.x |
. . . . . 6
โข ๐ = (var1โ๐ด) |
10 | | pm2mpval.a |
. . . . . 6
โข ๐ด = (๐ Mat ๐
) |
11 | | pm2mpval.q |
. . . . . 6
โข ๐ = (Poly1โ๐ด) |
12 | | pm2mpval.t |
. . . . . 6
โข ๐ = (๐ pMatToMatPoly ๐
) |
13 | 4, 5, 6, 7, 8, 9, 10, 11, 12 | pm2mpfval 22161 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐โ๐) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))) |
14 | 1, 2, 3, 13 | syl3anc 1372 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ (๐โ๐) = (๐ ฮฃg (๐ โ โ0
โฆ ((๐ decompPMat
๐) โ (๐ โ ๐))))) |
15 | 14 | fveq2d 6847 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ
(coe1โ(๐โ๐)) = (coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐)))))) |
16 | 15 | fveq1d 6845 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ
((coe1โ(๐โ๐))โ๐พ) = ((coe1โ(๐ ฮฃg
(๐ โ
โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐)))))โ๐พ)) |
17 | | eqid 2733 |
. . 3
โข
(Baseโ๐) =
(Baseโ๐) |
18 | 10 | matring 21808 |
. . . 4
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ด โ Ring) |
19 | 18 | adantr 482 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ ๐ด โ Ring) |
20 | | eqid 2733 |
. . 3
โข
(Baseโ๐ด) =
(Baseโ๐ด) |
21 | | eqid 2733 |
. . 3
โข
(0gโ๐ด) = (0gโ๐ด) |
22 | 2 | adantr 482 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โง ๐ โ โ0)
โ ๐
โ
Ring) |
23 | 3 | adantr 482 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โง ๐ โ โ0)
โ ๐ โ ๐ต) |
24 | | simpr 486 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โง ๐ โ โ0)
โ ๐ โ
โ0) |
25 | 4, 5, 6, 10, 20 | decpmatcl 22132 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต โง ๐ โ โ0) โ (๐ decompPMat ๐) โ (Baseโ๐ด)) |
26 | 22, 23, 24, 25 | syl3anc 1372 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โง ๐ โ โ0)
โ (๐ decompPMat ๐) โ (Baseโ๐ด)) |
27 | 26 | ralrimiva 3140 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ
โ๐ โ
โ0 (๐
decompPMat ๐) โ
(Baseโ๐ด)) |
28 | 4, 5, 6, 10, 21 | decpmatfsupp 22134 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (๐ โ โ0 โฆ (๐ decompPMat ๐)) finSupp (0gโ๐ด)) |
29 | 28 | ad2ant2lr 747 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ (๐ โ โ0
โฆ (๐ decompPMat ๐)) finSupp
(0gโ๐ด)) |
30 | | simpr 486 |
. . . 4
โข ((๐ โ ๐ต โง ๐พ โ โ0) โ ๐พ โ
โ0) |
31 | 30 | adantl 483 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ ๐พ โ
โ0) |
32 | 11, 17, 9, 8, 19, 20, 7, 21, 27, 29, 31 | gsummoncoe1 21691 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ
((coe1โ(๐
ฮฃg (๐ โ โ0 โฆ ((๐ decompPMat ๐) โ (๐ โ ๐)))))โ๐พ) = โฆ๐พ / ๐โฆ(๐ decompPMat ๐)) |
33 | | csbov2g 7404 |
. . . . 5
โข (๐พ โ โ0
โ โฆ๐พ /
๐โฆ(๐ decompPMat ๐) = (๐ decompPMat โฆ๐พ / ๐โฆ๐)) |
34 | | csbvarg 4392 |
. . . . . 6
โข (๐พ โ โ0
โ โฆ๐พ /
๐โฆ๐ = ๐พ) |
35 | 34 | oveq2d 7374 |
. . . . 5
โข (๐พ โ โ0
โ (๐ decompPMat
โฆ๐พ / ๐โฆ๐) = (๐ decompPMat ๐พ)) |
36 | 33, 35 | eqtrd 2773 |
. . . 4
โข (๐พ โ โ0
โ โฆ๐พ /
๐โฆ(๐ decompPMat ๐) = (๐ decompPMat ๐พ)) |
37 | 36 | adantl 483 |
. . 3
โข ((๐ โ ๐ต โง ๐พ โ โ0) โ
โฆ๐พ / ๐โฆ(๐ decompPMat ๐) = (๐ decompPMat ๐พ)) |
38 | 37 | adantl 483 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ
โฆ๐พ / ๐โฆ(๐ decompPMat ๐) = (๐ decompPMat ๐พ)) |
39 | 16, 32, 38 | 3eqtrd 2777 |
1
โข (((๐ โ Fin โง ๐
โ Ring) โง (๐ โ ๐ต โง ๐พ โ โ0)) โ
((coe1โ(๐โ๐))โ๐พ) = (๐ decompPMat ๐พ)) |