Step | Hyp | Ref
| Expression |
1 | | chfacfisfcpmat.s |
. . . . . . . 8
β’ π = (π ConstPolyMat π
) |
2 | | chfacfisf.p |
. . . . . . . 8
β’ π = (Poly1βπ
) |
3 | | chfacfisf.y |
. . . . . . . 8
β’ π = (π Mat π) |
4 | 1, 2, 3 | cpmatsubgpmat 22213 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring) β π β (SubGrpβπ)) |
5 | 4 | 3adant3 1132 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β π β (SubGrpβπ)) |
6 | 5 | adantr 481 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β π β (SubGrpβπ)) |
7 | | subgsubm 19022 |
. . . . . . 7
β’ (π β (SubGrpβπ) β π β (SubMndβπ)) |
8 | | chfacfisf.0 |
. . . . . . . 8
β’ 0 =
(0gβπ) |
9 | 8 | subm0cl 18688 |
. . . . . . 7
β’ (π β (SubMndβπ) β 0 β π) |
10 | 5, 7, 9 | 3syl 18 |
. . . . . 6
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β 0 β π) |
11 | 10 | adantr 481 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β 0 β π) |
12 | 1, 2, 3 | cpmatsrgpmat 22214 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring) β π β (SubRingβπ)) |
13 | 12 | 3adant3 1132 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β π β (SubRingβπ)) |
14 | 13 | adantr 481 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β π β (SubRingβπ)) |
15 | | chfacfisf.t |
. . . . . . . 8
β’ π = (π matToPolyMat π
) |
16 | | chfacfisf.a |
. . . . . . . 8
β’ π΄ = (π Mat π
) |
17 | | chfacfisf.b |
. . . . . . . 8
β’ π΅ = (Baseβπ΄) |
18 | 1, 15, 16, 17 | m2cpm 22234 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (πβπ) β π) |
19 | 18 | adantr 481 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (πβπ) β π) |
20 | | 3simpa 1148 |
. . . . . . . . 9
β’ ((π β Fin β§ π
β Ring β§ π β π΅) β (π β Fin β§ π
β Ring)) |
21 | | elmapi 8839 |
. . . . . . . . . . 11
β’ (π β (π΅ βm (0...π )) β π:(0...π )βΆπ΅) |
22 | 21 | adantl 482 |
. . . . . . . . . 10
β’ ((π β β β§ π β (π΅ βm (0...π ))) β π:(0...π )βΆπ΅) |
23 | | nnnn0 12475 |
. . . . . . . . . . . . 13
β’ (π β β β π β
β0) |
24 | | nn0uz 12860 |
. . . . . . . . . . . . 13
β’
β0 = (β€β₯β0) |
25 | 23, 24 | eleqtrdi 2843 |
. . . . . . . . . . . 12
β’ (π β β β π β
(β€β₯β0)) |
26 | | eluzfz1 13504 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β0) β 0 β (0...π )) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β 0 β
(0...π )) |
28 | 27 | adantr 481 |
. . . . . . . . . 10
β’ ((π β β β§ π β (π΅ βm (0...π ))) β 0 β (0...π )) |
29 | 22, 28 | ffvelcdmd 7084 |
. . . . . . . . 9
β’ ((π β β β§ π β (π΅ βm (0...π ))) β (πβ0) β π΅) |
30 | 20, 29 | anim12i 613 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β ((π β Fin β§ π
β Ring) β§ (πβ0) β π΅)) |
31 | | df-3an 1089 |
. . . . . . . 8
β’ ((π β Fin β§ π
β Ring β§ (πβ0) β π΅) β ((π β Fin β§ π
β Ring) β§ (πβ0) β π΅)) |
32 | 30, 31 | sylibr 233 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π β Fin β§ π
β Ring β§ (πβ0) β π΅)) |
33 | 1, 15, 16, 17 | m2cpm 22234 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring β§ (πβ0) β π΅) β (πβ(πβ0)) β π) |
34 | 32, 33 | syl 17 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (πβ(πβ0)) β π) |
35 | | chfacfisf.r |
. . . . . . 7
β’ Γ =
(.rβπ) |
36 | 35 | subrgmcl 20367 |
. . . . . 6
β’ ((π β (SubRingβπ) β§ (πβπ) β π β§ (πβ(πβ0)) β π) β ((πβπ) Γ (πβ(πβ0))) β π) |
37 | 14, 19, 34, 36 | syl3anc 1371 |
. . . . 5
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β ((πβπ) Γ (πβ(πβ0))) β π) |
38 | | chfacfisf.s |
. . . . . 6
β’ β =
(-gβπ) |
39 | 38 | subgsubcl 19011 |
. . . . 5
β’ ((π β (SubGrpβπ) β§ 0 β π β§ ((πβπ) Γ (πβ(πβ0))) β π) β ( 0 β ((πβπ) Γ (πβ(πβ0)))) β π) |
40 | 6, 11, 37, 39 | syl3anc 1371 |
. . . 4
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β ( 0 β ((πβπ) Γ (πβ(πβ0)))) β π) |
41 | 40 | ad2antrr 724 |
. . 3
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π = 0) β ( 0 β ((πβπ) Γ (πβ(πβ0)))) β π) |
42 | | simpl1 1191 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β π β Fin) |
43 | | simpl2 1192 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β π
β Ring) |
44 | 22 | adantl 482 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β π:(0...π )βΆπ΅) |
45 | | eluzfz2 13505 |
. . . . . . . . . 10
β’ (π β
(β€β₯β0) β π β (0...π )) |
46 | 25, 45 | syl 17 |
. . . . . . . . 9
β’ (π β β β π β (0...π )) |
47 | 46 | ad2antrl 726 |
. . . . . . . 8
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β π β (0...π )) |
48 | 44, 47 | ffvelcdmd 7084 |
. . . . . . 7
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (πβπ ) β π΅) |
49 | 1, 15, 16, 17 | m2cpm 22234 |
. . . . . . 7
β’ ((π β Fin β§ π
β Ring β§ (πβπ ) β π΅) β (πβ(πβπ )) β π) |
50 | 42, 43, 48, 49 | syl3anc 1371 |
. . . . . 6
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (πβ(πβπ )) β π) |
51 | 50 | adantr 481 |
. . . . 5
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β (πβ(πβπ )) β π) |
52 | 51 | ad2antrr 724 |
. . . 4
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π = (π + 1)) β (πβ(πβπ )) β π) |
53 | 11 | ad4antr 730 |
. . . . 5
β’
(((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ Β¬ π = (π + 1)) β§ (π + 1) < π) β 0 β π) |
54 | | nn0re 12477 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β π β
β) |
55 | 54 | adantl 482 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β π β
β) |
56 | | peano2nn 12220 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
β) |
57 | 56 | nnred 12223 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π + 1) β
β) |
58 | 57 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (π + 1) β
β) |
59 | 55, 58 | lenltd 11356 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β (π β€ (π + 1) β Β¬ (π + 1) < π)) |
60 | | nesym 2997 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) β π β Β¬ π = (π + 1)) |
61 | | ltlen 11311 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ (π + 1) β β) β
(π < (π + 1) β (π β€ (π + 1) β§ (π + 1) β π))) |
62 | 54, 57, 61 | syl2anr 597 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ π β β0)
β (π < (π + 1) β (π β€ (π + 1) β§ (π + 1) β π))) |
63 | 62 | biimprd 247 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ π β β0)
β ((π β€ (π + 1) β§ (π + 1) β π) β π < (π + 1))) |
64 | 63 | expcomd 417 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ π β β0)
β ((π + 1) β π β (π β€ (π + 1) β π < (π + 1)))) |
65 | 60, 64 | biimtrrid 242 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β0)
β (Β¬ π = (π + 1) β (π β€ (π + 1) β π < (π + 1)))) |
66 | 65 | com23 86 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β0)
β (π β€ (π + 1) β (Β¬ π = (π + 1) β π < (π + 1)))) |
67 | 59, 66 | sylbird 259 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β0)
β (Β¬ (π + 1) <
π β (Β¬ π = (π + 1) β π < (π + 1)))) |
68 | 67 | impcomd 412 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β0)
β ((Β¬ π = (π + 1) β§ Β¬ (π + 1) < π) β π < (π + 1))) |
69 | 68 | ex 413 |
. . . . . . . . . 10
β’ (π β β β (π β β0
β ((Β¬ π = (π + 1) β§ Β¬ (π + 1) < π) β π < (π + 1)))) |
70 | 69 | ad2antrl 726 |
. . . . . . . . 9
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π β β0 β ((Β¬
π = (π + 1) β§ Β¬ (π + 1) < π) β π < (π + 1)))) |
71 | 70 | imp 407 |
. . . . . . . 8
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β ((Β¬
π = (π + 1) β§ Β¬ (π + 1) < π) β π < (π + 1))) |
72 | 71 | adantr 481 |
. . . . . . 7
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β ((Β¬ π = (π + 1) β§ Β¬ (π + 1) < π) β π < (π + 1))) |
73 | 5 | ad4antr 730 |
. . . . . . . . 9
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β π β (SubGrpβπ)) |
74 | 20 | ad4antr 730 |
. . . . . . . . . . 11
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β (π β Fin β§ π
β Ring)) |
75 | 22 | ad4antlr 731 |
. . . . . . . . . . . 12
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β π:(0...π )βΆπ΅) |
76 | | neqne 2948 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π = 0 β π β 0) |
77 | 76 | anim2i 617 |
. . . . . . . . . . . . . . . 16
β’ ((π β β0
β§ Β¬ π = 0) β
(π β
β0 β§ π
β 0)) |
78 | | elnnne0 12482 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π β β0
β§ π β
0)) |
79 | 77, 78 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((π β β0
β§ Β¬ π = 0) β
π β
β) |
80 | | nnm1nn0 12509 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π β 1) β
β0) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ Β¬ π = 0) β
(π β 1) β
β0) |
82 | 81 | ad4ant23 751 |
. . . . . . . . . . . . 13
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β (π β 1) β
β0) |
83 | 23 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β (π΅ βm (0...π ))) β π β β0) |
84 | 83 | ad4antlr 731 |
. . . . . . . . . . . . 13
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β π β β0) |
85 | 62 | simprbda 499 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β π β€ (π + 1)) |
86 | 55 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β π β β) |
87 | | 1red 11211 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β 1 β
β) |
88 | | nnre 12215 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β) |
89 | 88 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β π β β) |
90 | 86, 87, 89 | lesubaddd 11807 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β ((π β 1) β€ π β π β€ (π + 1))) |
91 | 85, 90 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β (π β 1) β€ π ) |
92 | 91 | exp31 420 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π β β0
β (π < (π + 1) β (π β 1) β€ π ))) |
93 | 92 | ad2antrl 726 |
. . . . . . . . . . . . . . . 16
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π β β0 β (π < (π + 1) β (π β 1) β€ π ))) |
94 | 93 | imp 407 |
. . . . . . . . . . . . . . 15
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β (π < (π + 1) β (π β 1) β€ π )) |
95 | 94 | adantr 481 |
. . . . . . . . . . . . . 14
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β (π < (π + 1) β (π β 1) β€ π )) |
96 | 95 | imp 407 |
. . . . . . . . . . . . 13
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β (π β 1) β€ π ) |
97 | | elfz2nn0 13588 |
. . . . . . . . . . . . 13
β’ ((π β 1) β (0...π ) β ((π β 1) β β0 β§
π β
β0 β§ (π β 1) β€ π )) |
98 | 82, 84, 96, 97 | syl3anbrc 1343 |
. . . . . . . . . . . 12
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β (π β 1) β (0...π )) |
99 | 75, 98 | ffvelcdmd 7084 |
. . . . . . . . . . 11
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β (πβ(π β 1)) β π΅) |
100 | | df-3an 1089 |
. . . . . . . . . . 11
β’ ((π β Fin β§ π
β Ring β§ (πβ(π β 1)) β π΅) β ((π β Fin β§ π
β Ring) β§ (πβ(π β 1)) β π΅)) |
101 | 74, 99, 100 | sylanbrc 583 |
. . . . . . . . . 10
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β (π β Fin β§ π
β Ring β§ (πβ(π β 1)) β π΅)) |
102 | 1, 15, 16, 17 | m2cpm 22234 |
. . . . . . . . . 10
β’ ((π β Fin β§ π
β Ring β§ (πβ(π β 1)) β π΅) β (πβ(πβ(π β 1))) β π) |
103 | 101, 102 | syl 17 |
. . . . . . . . 9
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β (πβ(πβ(π β 1))) β π) |
104 | 14 | ad2antrr 724 |
. . . . . . . . . . 11
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β π β (SubRingβπ)) |
105 | 19 | ad2antrr 724 |
. . . . . . . . . . 11
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β (πβπ) β π) |
106 | 20, 83 | anim12i 613 |
. . . . . . . . . . . . . . 15
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β ((π β Fin β§ π
β Ring) β§ π β
β0)) |
107 | | df-3an 1089 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§ π
β Ring β§ π β β0)
β ((π β Fin β§
π
β Ring) β§ π β
β0)) |
108 | 106, 107 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π β Fin β§ π
β Ring β§ π β
β0)) |
109 | 108 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β (π β Fin β§ π
β Ring β§ π β
β0)) |
110 | 109 | simp1d 1142 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β π β Fin) |
111 | 109 | simp2d 1143 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β π
β Ring) |
112 | 44 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β π:(0...π )βΆπ΅) |
113 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β π β β0) |
114 | 23 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β π β β0) |
115 | | nn0z 12579 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β π β
β€) |
116 | | nnz 12575 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β€) |
117 | | zleltp1 12609 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β€ β§ π β β€) β (π β€ π β π < (π + 1))) |
118 | 115, 116,
117 | syl2anr 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ π β β0)
β (π β€ π β π < (π + 1))) |
119 | 118 | biimpar 478 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β π β€ π ) |
120 | | elfz2nn0 13588 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π ) β (π β β0 β§ π β β0
β§ π β€ π )) |
121 | 113, 114,
119, 120 | syl3anbrc 1343 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β0)
β§ π < (π + 1)) β π β (0...π )) |
122 | 121 | exp31 420 |
. . . . . . . . . . . . . . 15
β’ (π β β β (π β β0
β (π < (π + 1) β π β (0...π )))) |
123 | 122 | ad2antrl 726 |
. . . . . . . . . . . . . 14
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β (π β β0 β (π < (π + 1) β π β (0...π )))) |
124 | 123 | imp31 418 |
. . . . . . . . . . . . 13
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β π β (0...π )) |
125 | 112, 124 | ffvelcdmd 7084 |
. . . . . . . . . . . 12
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β (πβπ) β π΅) |
126 | 1, 15, 16, 17 | m2cpm 22234 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π
β Ring β§ (πβπ) β π΅) β (πβ(πβπ)) β π) |
127 | 110, 111,
125, 126 | syl3anc 1371 |
. . . . . . . . . . 11
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β (πβ(πβπ)) β π) |
128 | 35 | subrgmcl 20367 |
. . . . . . . . . . 11
β’ ((π β (SubRingβπ) β§ (πβπ) β π β§ (πβ(πβπ)) β π) β ((πβπ) Γ (πβ(πβπ))) β π) |
129 | 104, 105,
127, 128 | syl3anc 1371 |
. . . . . . . . . 10
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ π < (π + 1)) β ((πβπ) Γ (πβ(πβπ))) β π) |
130 | 129 | adantlr 713 |
. . . . . . . . 9
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β ((πβπ) Γ (πβ(πβπ))) β π) |
131 | 38 | subgsubcl 19011 |
. . . . . . . . 9
β’ ((π β (SubGrpβπ) β§ (πβ(πβ(π β 1))) β π β§ ((πβπ) Γ (πβ(πβπ))) β π) β ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))) β π) |
132 | 73, 103, 130, 131 | syl3anc 1371 |
. . . . . . . 8
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ π < (π + 1)) β ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))) β π) |
133 | 132 | ex 413 |
. . . . . . 7
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β (π < (π + 1) β ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))) β π)) |
134 | 72, 133 | syld 47 |
. . . . . 6
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β ((Β¬ π = (π + 1) β§ Β¬ (π + 1) < π) β ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))) β π)) |
135 | 134 | impl 456 |
. . . . 5
β’
(((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ Β¬ π = (π + 1)) β§ Β¬ (π + 1) < π) β ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))) β π) |
136 | 53, 135 | ifclda 4562 |
. . . 4
β’
((((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β§ Β¬ π = (π + 1)) β if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))) β π) |
137 | 52, 136 | ifclda 4562 |
. . 3
β’
(((((π β Fin
β§ π
β Ring β§
π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β§ Β¬
π = 0) β if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))) β π) |
138 | 41, 137 | ifclda 4562 |
. 2
β’ ((((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β§ π β β0) β if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ))))))) β π) |
139 | | chfacfisf.g |
. 2
β’ πΊ = (π β β0 β¦ if(π = 0, ( 0 β ((πβπ) Γ (πβ(πβ0)))), if(π = (π + 1), (πβ(πβπ )), if((π + 1) < π, 0 , ((πβ(πβ(π β 1))) β ((πβπ) Γ (πβ(πβπ)))))))) |
140 | 138, 139 | fmptd 7110 |
1
β’ (((π β Fin β§ π
β Ring β§ π β π΅) β§ (π β β β§ π β (π΅ βm (0...π )))) β πΊ:β0βΆπ) |