Step | Hyp | Ref
| Expression |
1 | | chpmatfval.c |
. 2
โข ๐ถ = (๐ CharPlyMat ๐
) |
2 | | df-chpmat 22199 |
. . . 4
โข
CharPlyMat = (๐ โ Fin,
๐ โ V โฆ (๐ โ (Baseโ(๐ Mat ๐)) โฆ ((๐ maDet (Poly1โ๐))โ(((var1โ๐)(
ยท๐ โ(๐ Mat (Poly1โ๐)))(1rโ(๐ Mat
(Poly1โ๐))))(-gโ(๐ Mat (Poly1โ๐)))((๐ matToPolyMat ๐)โ๐))))) |
3 | 2 | a1i 11 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ CharPlyMat = (๐ โ Fin, ๐ โ V โฆ (๐ โ (Baseโ(๐ Mat ๐)) โฆ ((๐ maDet (Poly1โ๐))โ(((var1โ๐)(
ยท๐ โ(๐ Mat (Poly1โ๐)))(1rโ(๐ Mat
(Poly1โ๐))))(-gโ(๐ Mat (Poly1โ๐)))((๐ matToPolyMat ๐)โ๐)))))) |
4 | | oveq12 7370 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ Mat ๐) = (๐ Mat ๐
)) |
5 | | chpmatfval.a |
. . . . . . . 8
โข ๐ด = (๐ Mat ๐
) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ Mat ๐) = ๐ด) |
7 | 6 | fveq2d 6850 |
. . . . . 6
โข ((๐ = ๐ โง ๐ = ๐
) โ (Baseโ(๐ Mat ๐)) = (Baseโ๐ด)) |
8 | | chpmatfval.b |
. . . . . 6
โข ๐ต = (Baseโ๐ด) |
9 | 7, 8 | eqtr4di 2791 |
. . . . 5
โข ((๐ = ๐ โง ๐ = ๐
) โ (Baseโ(๐ Mat ๐)) = ๐ต) |
10 | | simpl 484 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ ๐ = ๐) |
11 | | simpr 486 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐
) โ ๐ = ๐
) |
12 | 11 | fveq2d 6850 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (Poly1โ๐) =
(Poly1โ๐
)) |
13 | | chpmatfval.p |
. . . . . . . . 9
โข ๐ = (Poly1โ๐
) |
14 | 12, 13 | eqtr4di 2791 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (Poly1โ๐) = ๐) |
15 | 10, 14 | oveq12d 7379 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ maDet (Poly1โ๐)) = (๐ maDet ๐)) |
16 | | chpmatfval.d |
. . . . . . 7
โข ๐ท = (๐ maDet ๐) |
17 | 15, 16 | eqtr4di 2791 |
. . . . . 6
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ maDet (Poly1โ๐)) = ๐ท) |
18 | | fveq2 6846 |
. . . . . . . . . . . . 13
โข (๐ = ๐
โ (Poly1โ๐) =
(Poly1โ๐
)) |
19 | 18 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ = ๐ โง ๐ = ๐
) โ (Poly1โ๐) =
(Poly1โ๐
)) |
20 | 19, 13 | eqtr4di 2791 |
. . . . . . . . . . 11
โข ((๐ = ๐ โง ๐ = ๐
) โ (Poly1โ๐) = ๐) |
21 | 10, 20 | oveq12d 7379 |
. . . . . . . . . 10
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ Mat (Poly1โ๐)) = (๐ Mat ๐)) |
22 | | chpmatfval.y |
. . . . . . . . . 10
โข ๐ = (๐ Mat ๐) |
23 | 21, 22 | eqtr4di 2791 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ Mat (Poly1โ๐)) = ๐) |
24 | 23 | fveq2d 6850 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (-gโ(๐ Mat
(Poly1โ๐))) = (-gโ๐)) |
25 | | chpmatfval.s |
. . . . . . . 8
โข โ =
(-gโ๐) |
26 | 24, 25 | eqtr4di 2791 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ (-gโ(๐ Mat
(Poly1โ๐))) = โ ) |
27 | 23 | fveq2d 6850 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (
ยท๐ โ(๐ Mat (Poly1โ๐))) = (
ยท๐ โ๐)) |
28 | | chpmatfval.m |
. . . . . . . . 9
โข ยท = (
ยท๐ โ๐) |
29 | 27, 28 | eqtr4di 2791 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (
ยท๐ โ(๐ Mat (Poly1โ๐))) = ยท ) |
30 | | fveq2 6846 |
. . . . . . . . . 10
โข (๐ = ๐
โ (var1โ๐) = (var1โ๐
)) |
31 | | chpmatfval.x |
. . . . . . . . . 10
โข ๐ = (var1โ๐
) |
32 | 30, 31 | eqtr4di 2791 |
. . . . . . . . 9
โข (๐ = ๐
โ (var1โ๐) = ๐) |
33 | 32 | adantl 483 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (var1โ๐) = ๐) |
34 | 23 | fveq2d 6850 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (1rโ(๐ Mat
(Poly1โ๐))) = (1rโ๐)) |
35 | | chpmatfval.i |
. . . . . . . . 9
โข 1 =
(1rโ๐) |
36 | 34, 35 | eqtr4di 2791 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (1rโ(๐ Mat
(Poly1โ๐))) = 1 ) |
37 | 29, 33, 36 | oveq123d 7382 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ ((var1โ๐)(
ยท๐ โ(๐ Mat (Poly1โ๐)))(1rโ(๐ Mat
(Poly1โ๐)))) = (๐ ยท 1 )) |
38 | | oveq12 7370 |
. . . . . . . . 9
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ matToPolyMat ๐) = (๐ matToPolyMat ๐
)) |
39 | | chpmatfval.t |
. . . . . . . . 9
โข ๐ = (๐ matToPolyMat ๐
) |
40 | 38, 39 | eqtr4di 2791 |
. . . . . . . 8
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ matToPolyMat ๐) = ๐) |
41 | 40 | fveq1d 6848 |
. . . . . . 7
โข ((๐ = ๐ โง ๐ = ๐
) โ ((๐ matToPolyMat ๐)โ๐) = (๐โ๐)) |
42 | 26, 37, 41 | oveq123d 7382 |
. . . . . 6
โข ((๐ = ๐ โง ๐ = ๐
) โ (((var1โ๐)(
ยท๐ โ(๐ Mat (Poly1โ๐)))(1rโ(๐ Mat
(Poly1โ๐))))(-gโ(๐ Mat (Poly1โ๐)))((๐ matToPolyMat ๐)โ๐)) = ((๐ ยท 1 ) โ (๐โ๐))) |
43 | 17, 42 | fveq12d 6853 |
. . . . 5
โข ((๐ = ๐ โง ๐ = ๐
) โ ((๐ maDet (Poly1โ๐))โ(((var1โ๐)(
ยท๐ โ(๐ Mat (Poly1โ๐)))(1rโ(๐ Mat
(Poly1โ๐))))(-gโ(๐ Mat (Poly1โ๐)))((๐ matToPolyMat ๐)โ๐))) = (๐ทโ((๐ ยท 1 ) โ (๐โ๐)))) |
44 | 9, 43 | mpteq12dv 5200 |
. . . 4
โข ((๐ = ๐ โง ๐ = ๐
) โ (๐ โ (Baseโ(๐ Mat ๐)) โฆ ((๐ maDet (Poly1โ๐))โ(((var1โ๐)(
ยท๐ โ(๐ Mat (Poly1โ๐)))(1rโ(๐ Mat
(Poly1โ๐))))(-gโ(๐ Mat (Poly1โ๐)))((๐ matToPolyMat ๐)โ๐)))) = (๐ โ ๐ต โฆ (๐ทโ((๐ ยท 1 ) โ (๐โ๐))))) |
45 | 44 | adantl 483 |
. . 3
โข (((๐ โ Fin โง ๐
โ ๐) โง (๐ = ๐ โง ๐ = ๐
)) โ (๐ โ (Baseโ(๐ Mat ๐)) โฆ ((๐ maDet (Poly1โ๐))โ(((var1โ๐)(
ยท๐ โ(๐ Mat (Poly1โ๐)))(1rโ(๐ Mat
(Poly1โ๐))))(-gโ(๐ Mat (Poly1โ๐)))((๐ matToPolyMat ๐)โ๐)))) = (๐ โ ๐ต โฆ (๐ทโ((๐ ยท 1 ) โ (๐โ๐))))) |
46 | | simpl 484 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐ โ Fin) |
47 | | elex 3465 |
. . . 4
โข (๐
โ ๐ โ ๐
โ V) |
48 | 47 | adantl 483 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐
โ V) |
49 | 8 | fvexi 6860 |
. . . 4
โข ๐ต โ V |
50 | | mptexg 7175 |
. . . 4
โข (๐ต โ V โ (๐ โ ๐ต โฆ (๐ทโ((๐ ยท 1 ) โ (๐โ๐)))) โ V) |
51 | 49, 50 | mp1i 13 |
. . 3
โข ((๐ โ Fin โง ๐
โ ๐) โ (๐ โ ๐ต โฆ (๐ทโ((๐ ยท 1 ) โ (๐โ๐)))) โ V) |
52 | 3, 45, 46, 48, 51 | ovmpod 7511 |
. 2
โข ((๐ โ Fin โง ๐
โ ๐) โ (๐ CharPlyMat ๐
) = (๐ โ ๐ต โฆ (๐ทโ((๐ ยท 1 ) โ (๐โ๐))))) |
53 | 1, 52 | eqtrid 2785 |
1
โข ((๐ โ Fin โง ๐
โ ๐) โ ๐ถ = (๐ โ ๐ต โฆ (๐ทโ((๐ ยท 1 ) โ (๐โ๐))))) |