Step | Hyp | Ref
| Expression |
1 | | chmatcl.h |
. . . 4
โข ๐ป = ((๐ ยท 1 ) โ (๐โ๐)) |
2 | 1 | oveqi 7316 |
. . 3
โข (๐ผ๐ป๐ฝ) = (๐ผ((๐ ยท 1 ) โ (๐โ๐))๐ฝ) |
3 | | chmatcl.p |
. . . . . . 7
โข ๐ = (Poly1โ๐
) |
4 | 3 | ply1ring 21460 |
. . . . . 6
โข (๐
โ Ring โ ๐ โ Ring) |
5 | 4 | 3ad2ant2 1134 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ Ring) |
6 | 5 | adantr 482 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐ โ Ring) |
7 | 4 | anim2i 618 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐ โ Fin โง ๐ โ Ring)) |
8 | 7 | 3adant3 1132 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐ โ Fin โง ๐ โ Ring)) |
9 | | chmatcl.x |
. . . . . . . 8
โข ๐ = (var1โ๐
) |
10 | | eqid 2736 |
. . . . . . . 8
โข
(Baseโ๐) =
(Baseโ๐) |
11 | 9, 3, 10 | vr1cl 21429 |
. . . . . . 7
โข (๐
โ Ring โ ๐ โ (Baseโ๐)) |
12 | 11 | 3ad2ant2 1134 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ (Baseโ๐)) |
13 | | chmatcl.y |
. . . . . . . . 9
โข ๐ = (๐ Mat ๐) |
14 | 3, 13 | pmatring 21882 |
. . . . . . . 8
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ Ring) |
15 | 14 | 3adant3 1132 |
. . . . . . 7
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ Ring) |
16 | | eqid 2736 |
. . . . . . . 8
โข
(Baseโ๐) =
(Baseโ๐) |
17 | | chmatcl.1 |
. . . . . . . 8
โข 1 =
(1rโ๐) |
18 | 16, 17 | ringidcl 19848 |
. . . . . . 7
โข (๐ โ Ring โ 1 โ
(Baseโ๐)) |
19 | 15, 18 | syl 17 |
. . . . . 6
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ 1 โ (Baseโ๐)) |
20 | | chmatcl.m |
. . . . . . 7
โข ยท = (
ยท๐ โ๐) |
21 | 10, 13, 16, 20 | matvscl 21621 |
. . . . . 6
โข (((๐ โ Fin โง ๐ โ Ring) โง (๐ โ (Baseโ๐) โง 1 โ (Baseโ๐))) โ (๐ ยท 1 ) โ (Baseโ๐)) |
22 | 8, 12, 19, 21 | syl12anc 835 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐ ยท 1 ) โ (Baseโ๐)) |
23 | 22 | adantr 482 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ ยท 1 ) โ (Baseโ๐)) |
24 | | chmatcl.t |
. . . . . 6
โข ๐ = (๐ matToPolyMat ๐
) |
25 | | chmatcl.a |
. . . . . 6
โข ๐ด = (๐ Mat ๐
) |
26 | | chmatcl.b |
. . . . . 6
โข ๐ต = (Baseโ๐ด) |
27 | 24, 25, 26, 3, 13 | mat2pmatbas 21916 |
. . . . 5
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐โ๐) โ (Baseโ๐)) |
28 | 27 | adantr 482 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐โ๐) โ (Baseโ๐)) |
29 | | simpr 486 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ โ ๐ โง ๐ฝ โ ๐)) |
30 | | chmatcl.s |
. . . . 5
โข โ =
(-gโ๐) |
31 | | chmatval.s |
. . . . 5
โข โผ =
(-gโ๐) |
32 | 13, 16, 30, 31 | matsubgcell 21624 |
. . . 4
โข ((๐ โ Ring โง ((๐ ยท 1 ) โ (Baseโ๐) โง (๐โ๐) โ (Baseโ๐)) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ((๐ ยท 1 ) โ (๐โ๐))๐ฝ) = ((๐ผ(๐ ยท 1 )๐ฝ) โผ (๐ผ(๐โ๐)๐ฝ))) |
33 | 6, 23, 28, 29, 32 | syl121anc 1375 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ((๐ ยท 1 ) โ (๐โ๐))๐ฝ) = ((๐ผ(๐ ยท 1 )๐ฝ) โผ (๐ผ(๐โ๐)๐ฝ))) |
34 | 2, 33 | eqtrid 2788 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ๐ป๐ฝ) = ((๐ผ(๐ ยท 1 )๐ฝ) โผ (๐ผ(๐โ๐)๐ฝ))) |
35 | 17 | a1i 11 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ 1 =
(1rโ๐)) |
36 | 35 | oveq2d 7319 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ ยท 1 ) = (๐ ยท
(1rโ๐))) |
37 | | simpl 484 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ Fin) |
38 | 4 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ Ring) |
39 | 11 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐
โ Ring) โ ๐ โ (Baseโ๐)) |
40 | 37, 38, 39 | 3jca 1128 |
. . . . . . . . 9
โข ((๐ โ Fin โง ๐
โ Ring) โ (๐ โ Fin โง ๐ โ Ring โง ๐ โ (Baseโ๐))) |
41 | 40 | 3adant3 1132 |
. . . . . . . 8
โข ((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โ (๐ โ Fin โง ๐ โ Ring โง ๐ โ (Baseโ๐))) |
42 | 41 | adantr 482 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ โ Fin โง ๐ โ Ring โง ๐ โ (Baseโ๐))) |
43 | | chmatval.0 |
. . . . . . . 8
โข 0 =
(0gโ๐) |
44 | 13, 10, 20, 43 | matsc 21640 |
. . . . . . 7
โข ((๐ โ Fin โง ๐ โ Ring โง ๐ โ (Baseโ๐)) โ (๐ ยท
(1rโ๐)) =
(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ๐, 0 ))) |
45 | 42, 44 | syl 17 |
. . . . . 6
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ ยท
(1rโ๐)) =
(๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ๐, 0 ))) |
46 | 36, 45 | eqtrd 2776 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ ยท 1 ) = (๐ โ ๐, ๐ โ ๐ โฆ if(๐ = ๐, ๐, 0 ))) |
47 | | eqeq12 2753 |
. . . . . . 7
โข ((๐ = ๐ผ โง ๐ = ๐ฝ) โ (๐ = ๐ โ ๐ผ = ๐ฝ)) |
48 | 47 | ifbid 4488 |
. . . . . 6
โข ((๐ = ๐ผ โง ๐ = ๐ฝ) โ if(๐ = ๐, ๐, 0 ) = if(๐ผ = ๐ฝ, ๐, 0 )) |
49 | 48 | adantl 483 |
. . . . 5
โข ((((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โง (๐ = ๐ผ โง ๐ = ๐ฝ)) โ if(๐ = ๐, ๐, 0 ) = if(๐ผ = ๐ฝ, ๐, 0 )) |
50 | | simprl 769 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐ผ โ ๐) |
51 | | simpr 486 |
. . . . . 6
โข ((๐ผ โ ๐ โง ๐ฝ โ ๐) โ ๐ฝ โ ๐) |
52 | 51 | adantl 483 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ๐ฝ โ ๐) |
53 | 9 | fvexi 6814 |
. . . . . . 7
โข ๐ โ V |
54 | 43 | fvexi 6814 |
. . . . . . 7
โข 0 โ
V |
55 | 53, 54 | ifex 4515 |
. . . . . 6
โข if(๐ผ = ๐ฝ, ๐, 0 ) โ
V |
56 | 55 | a1i 11 |
. . . . 5
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ if(๐ผ = ๐ฝ, ๐, 0 ) โ
V) |
57 | 46, 49, 50, 52, 56 | ovmpod 7453 |
. . . 4
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ(๐ ยท 1 )๐ฝ) = if(๐ผ = ๐ฝ, ๐, 0 )) |
58 | 57 | oveq1d 7318 |
. . 3
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ((๐ผ(๐ ยท 1 )๐ฝ) โผ (๐ผ(๐โ๐)๐ฝ)) = (if(๐ผ = ๐ฝ, ๐, 0 ) โผ (๐ผ(๐โ๐)๐ฝ))) |
59 | | ovif 7400 |
. . 3
โข (if(๐ผ = ๐ฝ, ๐, 0 ) โผ (๐ผ(๐โ๐)๐ฝ)) = if(๐ผ = ๐ฝ, (๐ โผ (๐ผ(๐โ๐)๐ฝ)), ( 0 โผ (๐ผ(๐โ๐)๐ฝ))) |
60 | 58, 59 | eqtrdi 2792 |
. 2
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ ((๐ผ(๐ ยท 1 )๐ฝ) โผ (๐ผ(๐โ๐)๐ฝ)) = if(๐ผ = ๐ฝ, (๐ โผ (๐ผ(๐โ๐)๐ฝ)), ( 0 โผ (๐ผ(๐โ๐)๐ฝ)))) |
61 | 34, 60 | eqtrd 2776 |
1
โข (((๐ โ Fin โง ๐
โ Ring โง ๐ โ ๐ต) โง (๐ผ โ ๐ โง ๐ฝ โ ๐)) โ (๐ผ๐ป๐ฝ) = if(๐ผ = ๐ฝ, (๐ โผ (๐ผ(๐โ๐)๐ฝ)), ( 0 โผ (๐ผ(๐โ๐)๐ฝ)))) |