Step | Hyp | Ref
| Expression |
1 | | chfacfisf.0 |
. . . 4
โข 0 =
(0gโ๐) |
2 | 1 | fvexi 6860 |
. . 3
โข 0 โ
V |
3 | 2 | a1i 11 |
. 2
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ 0 โ V) |
4 | | ovexd 7396 |
. 2
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ ((๐ โ ๐) ยท (๐บโ๐)) โ V) |
5 | | nnnn0 12428 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ0) |
6 | | peano2nn0 12461 |
. . . . 5
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
7 | 5, 6 | syl 17 |
. . . 4
โข (๐ โ โ โ (๐ + 1) โ
โ0) |
8 | 7 | ad2antrl 727 |
. . 3
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ + 1) โ
โ0) |
9 | | vex 3451 |
. . . . . . 7
โข ๐ โ V |
10 | | csbov12g 7405 |
. . . . . . . 8
โข (๐ โ V โ
โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = (โฆ๐ / ๐โฆ(๐ โ ๐) ยท
โฆ๐ / ๐โฆ(๐บโ๐))) |
11 | | csbov1g 7406 |
. . . . . . . . . 10
โข (๐ โ V โ
โฆ๐ / ๐โฆ(๐ โ ๐) = (โฆ๐ / ๐โฆ๐ โ ๐)) |
12 | | csbvarg 4395 |
. . . . . . . . . . 11
โข (๐ โ V โ
โฆ๐ / ๐โฆ๐ = ๐) |
13 | 12 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ โ V โ
(โฆ๐ / ๐โฆ๐ โ ๐) = (๐ โ ๐)) |
14 | 11, 13 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ V โ
โฆ๐ / ๐โฆ(๐ โ ๐) = (๐ โ ๐)) |
15 | | csbfv 6896 |
. . . . . . . . . 10
โข
โฆ๐ /
๐โฆ(๐บโ๐) = (๐บโ๐) |
16 | 15 | a1i 11 |
. . . . . . . . 9
โข (๐ โ V โ
โฆ๐ / ๐โฆ(๐บโ๐) = (๐บโ๐)) |
17 | 14, 16 | oveq12d 7379 |
. . . . . . . 8
โข (๐ โ V โ
(โฆ๐ / ๐โฆ(๐ โ ๐) ยท
โฆ๐ / ๐โฆ(๐บโ๐)) = ((๐ โ ๐) ยท (๐บโ๐))) |
18 | 10, 17 | eqtrd 2773 |
. . . . . . 7
โข (๐ โ V โ
โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = ((๐ โ ๐) ยท (๐บโ๐))) |
19 | 9, 18 | mp1i 13 |
. . . . . 6
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = ((๐ โ ๐) ยท (๐บโ๐))) |
20 | | simplll 774 |
. . . . . . 7
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ (๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต)) |
21 | | simpllr 775 |
. . . . . . 7
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) |
22 | 5 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (๐ต โm (0...๐ ))) โ ๐ โ โ0) |
23 | 22 | ad2antlr 726 |
. . . . . . . . . . 11
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ ๐ โ
โ0) |
24 | 23 | nn0zd 12533 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ ๐ โ
โค) |
25 | 24 | adantr 482 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ ๐ โ โค) |
26 | | 2z 12543 |
. . . . . . . . . 10
โข 2 โ
โค |
27 | 26 | a1i 11 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ 2 โ โค) |
28 | 25, 27 | zaddcld 12619 |
. . . . . . . 8
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ (๐ + 2) โ โค) |
29 | | simplr 768 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ ๐ โ โ0) |
30 | 29 | nn0zd 12533 |
. . . . . . . 8
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ ๐ โ โค) |
31 | 8 | nn0zd 12533 |
. . . . . . . . . . 11
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ + 1) โ โค) |
32 | | nn0z 12532 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ ๐ โ
โค) |
33 | | zltp1le 12561 |
. . . . . . . . . . 11
โข (((๐ + 1) โ โค โง ๐ โ โค) โ ((๐ + 1) < ๐ โ ((๐ + 1) + 1) โค ๐)) |
34 | 31, 32, 33 | syl2an 597 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ ((๐ + 1) < ๐ โ ((๐ + 1) + 1) โค ๐)) |
35 | 34 | biimpa 478 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ ((๐ + 1) + 1) โค ๐) |
36 | | nncn 12169 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
37 | | add1p1 12412 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ((๐ + 1) + 1) = (๐ + 2)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((๐ + 1) + 1) = (๐ + 2)) |
39 | 38 | breq1d 5119 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (((๐ + 1) + 1) โค ๐ โ (๐ + 2) โค ๐)) |
40 | 39 | bicomd 222 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ((๐ + 2) โค ๐ โ ((๐ + 1) + 1) โค ๐)) |
41 | 40 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (๐ต โm (0...๐ ))) โ ((๐ + 2) โค ๐ โ ((๐ + 1) + 1) โค ๐)) |
42 | 41 | ad2antlr 726 |
. . . . . . . . . 10
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ ((๐ + 2) โค ๐ โ ((๐ + 1) + 1) โค ๐)) |
43 | 42 | adantr 482 |
. . . . . . . . 9
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ ((๐ + 2) โค ๐ โ ((๐ + 1) + 1) โค ๐)) |
44 | 35, 43 | mpbird 257 |
. . . . . . . 8
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ (๐ + 2) โค ๐) |
45 | | eluz2 12777 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ(๐ + 2)) โ ((๐ + 2) โ โค โง ๐ โ โค โง (๐ + 2) โค ๐)) |
46 | 28, 30, 44, 45 | syl3anbrc 1344 |
. . . . . . 7
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ ๐ โ (โคโฅโ(๐ + 2))) |
47 | | chfacfisf.a |
. . . . . . . 8
โข ๐ด = (๐ Mat ๐
) |
48 | | chfacfisf.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐ด) |
49 | | chfacfisf.p |
. . . . . . . 8
โข ๐ = (Poly1โ๐
) |
50 | | chfacfisf.y |
. . . . . . . 8
โข ๐ = (๐ Mat ๐) |
51 | | chfacfisf.r |
. . . . . . . 8
โข ร =
(.rโ๐) |
52 | | chfacfisf.s |
. . . . . . . 8
โข โ =
(-gโ๐) |
53 | | chfacfisf.t |
. . . . . . . 8
โข ๐ = (๐ matToPolyMat ๐
) |
54 | | chfacfisf.g |
. . . . . . . 8
โข ๐บ = (๐ โ โ0 โฆ if(๐ = 0, ( 0 โ ((๐โ๐) ร (๐โ(๐โ0)))), if(๐ = (๐ + 1), (๐โ(๐โ๐ )), if((๐ + 1) < ๐, 0 , ((๐โ(๐โ(๐ โ 1))) โ ((๐โ๐) ร (๐โ(๐โ๐)))))))) |
55 | | chfacfscmulcl.x |
. . . . . . . 8
โข ๐ = (var1โ๐
) |
56 | | chfacfscmulcl.m |
. . . . . . . 8
โข ยท = (
ยท๐ โ๐) |
57 | | chfacfscmulcl.e |
. . . . . . . 8
โข โ =
(.gโ(mulGrpโ๐)) |
58 | 47, 48, 49, 50, 51, 52, 1, 53, 54, 55, 56, 57 | chfacfscmul0 22230 |
. . . . . . 7
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ ))) โง ๐ โ (โคโฅโ(๐ + 2))) โ ((๐ โ ๐) ยท (๐บโ๐)) = 0 ) |
59 | 20, 21, 46, 58 | syl3anc 1372 |
. . . . . 6
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ ((๐ โ ๐) ยท (๐บโ๐)) = 0 ) |
60 | 19, 59 | eqtrd 2773 |
. . . . 5
โข
(((((๐ โ Fin
โง ๐
โ CRing โง
๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โง (๐ + 1) < ๐) โ โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = 0 ) |
61 | 60 | ex 414 |
. . . 4
โข ((((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โง ๐ โ โ0) โ ((๐ + 1) < ๐ โ โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = 0 )) |
62 | 61 | ralrimiva 3140 |
. . 3
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ โ๐ โ โ0 ((๐ + 1) < ๐ โ โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = 0 )) |
63 | | breq1 5112 |
. . . 4
โข (๐ง = (๐ + 1) โ (๐ง < ๐ โ (๐ + 1) < ๐)) |
64 | 63 | rspceaimv 3587 |
. . 3
โข (((๐ + 1) โ โ0
โง โ๐ โ
โ0 ((๐ +
1) < ๐ โ
โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = 0 )) โ โ๐ง โ โ0
โ๐ โ
โ0 (๐ง <
๐ โ
โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = 0 )) |
65 | 8, 62, 64 | syl2anc 585 |
. 2
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ โ๐ง โ โ0 โ๐ โ โ0
(๐ง < ๐ โ โฆ๐ / ๐โฆ((๐ โ ๐) ยท (๐บโ๐)) = 0 )) |
66 | 3, 4, 65 | mptnn0fsupp 13911 |
1
โข (((๐ โ Fin โง ๐
โ CRing โง ๐ โ ๐ต) โง (๐ โ โ โง ๐ โ (๐ต โm (0...๐ )))) โ (๐ โ โ0 โฆ ((๐ โ ๐) ยท (๐บโ๐))) finSupp 0 ) |