Metamath Proof Explorer

Theorem chfacfisf

Description: The "characteristic factor function" is a function from the nonnegative integers to polynomial matrices. (Contributed by AV, 8-Nov-2019)

Ref Expression
Hypotheses chfacfisf.a 
|- A = ( N Mat R )
chfacfisf.b 
|- B = ( Base ` A )
chfacfisf.p 
|- P = ( Poly1 ` R )
chfacfisf.y 
|- Y = ( N Mat P )
chfacfisf.r 
|- .X. = ( .r ` Y )
chfacfisf.s 
|- .- = ( -g ` Y )
chfacfisf.0 
|- .0. = ( 0g ` Y )
chfacfisf.t 
|- T = ( N matToPolyMat R )
chfacfisf.g 
|- G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
Assertion chfacfisf 
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> ( Base ` Y ) )

Proof

Step Hyp Ref Expression
1 chfacfisf.a 
 |-  A = ( N Mat R )
2 chfacfisf.b 
 |-  B = ( Base ` A )
3 chfacfisf.p 
 |-  P = ( Poly1 ` R )
4 chfacfisf.y 
 |-  Y = ( N Mat P )
5 chfacfisf.r 
 |-  .X. = ( .r ` Y )
6 chfacfisf.s 
 |-  .- = ( -g ` Y )
7 chfacfisf.0 
 |-  .0. = ( 0g ` Y )
8 chfacfisf.t 
 |-  T = ( N matToPolyMat R )
9 chfacfisf.g 
 |-  G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
10 3 4 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
11 10 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Y e. Ring )
12 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
13 11 12 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Y e. Grp )
14 13 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Grp )
15 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
16 15 7 ring0cl 
 |-  ( Y e. Ring -> .0. e. ( Base ` Y ) )
17 11 16 syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .0. e. ( Base ` Y ) )
18 17 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> .0. e. ( Base ` Y ) )
19 11 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
20 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
21 20 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. ( Base ` Y ) )
22 3simpa 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
23 elmapi 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
24 23 adantl 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
25 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
26 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
27 25 26 eleqtrdi 
 |-  ( s e. NN -> s e. ( ZZ>= ` 0 ) )
28 eluzfz1 
 |-  ( s e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... s ) )
29 27 28 syl 
 |-  ( s e. NN -> 0 e. ( 0 ... s ) )
30 29 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> 0 e. ( 0 ... s ) )
31 24 30 ffvelcdmd 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( b ` 0 ) e. B )
32 22 31 anim12i 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ ( b ` 0 ) e. B ) )
33 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ ( b ` 0 ) e. B ) )
34 32 33 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) )
35 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
36 34 35 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` 0 ) ) e. ( Base ` Y ) )
37 15 5 ringcl 
 |-  ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` 0 ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
38 19 21 36 37 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) )
39 15 6 grpsubcl 
 |-  ( ( Y e. Grp /\ .0. e. ( Base ` Y ) /\ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. ( Base ` Y ) ) -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. ( Base ` Y ) )
40 14 18 38 39 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. ( Base ` Y ) )
41 40 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n = 0 ) -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. ( Base ` Y ) )
42 25 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
43 22 42 anim12i 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ s e. NN0 ) )
44 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) <-> ( ( N e. Fin /\ R e. Ring ) /\ s e. NN0 ) )
45 43 44 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( N e. Fin /\ R e. Ring /\ s e. NN0 ) )
46 eluzfz2 
 |-  ( s e. ( ZZ>= ` 0 ) -> s e. ( 0 ... s ) )
47 27 46 syl 
 |-  ( s e. NN -> s e. ( 0 ... s ) )
48 47 anim1ci 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( b e. ( B ^m ( 0 ... s ) ) /\ s e. ( 0 ... s ) ) )
49 48 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b e. ( B ^m ( 0 ... s ) ) /\ s e. ( 0 ... s ) ) )
50 1 2 3 4 8 m2pmfzmap 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ ( b e. ( B ^m ( 0 ... s ) ) /\ s e. ( 0 ... s ) ) ) -> ( T ` ( b ` s ) ) e. ( Base ` Y ) )
51 45 49 50 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` s ) ) e. ( Base ` Y ) )
52 51 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( T ` ( b ` s ) ) e. ( Base ` Y ) )
53 52 ad2antrr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n = ( s + 1 ) ) -> ( T ` ( b ` s ) ) e. ( Base ` Y ) )
54 18 ad4antr 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ ( s + 1 ) < n ) -> .0. e. ( Base ` Y ) )
55 nn0re 
 |-  ( n e. NN0 -> n e. RR )
56 55 adantl 
 |-  ( ( s e. NN /\ n e. NN0 ) -> n e. RR )
57 peano2nn 
 |-  ( s e. NN -> ( s + 1 ) e. NN )
58 57 nnred 
 |-  ( s e. NN -> ( s + 1 ) e. RR )
59 58 adantr 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( s + 1 ) e. RR )
60 56 59 lenltd 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( n <_ ( s + 1 ) <-> -. ( s + 1 ) < n ) )
61 nesym 
 |-  ( ( s + 1 ) =/= n <-> -. n = ( s + 1 ) )
62 ltlen 
 |-  ( ( n e. RR /\ ( s + 1 ) e. RR ) -> ( n < ( s + 1 ) <-> ( n <_ ( s + 1 ) /\ ( s + 1 ) =/= n ) ) )
63 55 58 62 syl2anr 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( n < ( s + 1 ) <-> ( n <_ ( s + 1 ) /\ ( s + 1 ) =/= n ) ) )
64 63 biimprd 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( ( n <_ ( s + 1 ) /\ ( s + 1 ) =/= n ) -> n < ( s + 1 ) ) )
65 64 expcomd 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( ( s + 1 ) =/= n -> ( n <_ ( s + 1 ) -> n < ( s + 1 ) ) ) )
66 61 65 biimtrrid 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( -. n = ( s + 1 ) -> ( n <_ ( s + 1 ) -> n < ( s + 1 ) ) ) )
67 66 com23 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( n <_ ( s + 1 ) -> ( -. n = ( s + 1 ) -> n < ( s + 1 ) ) ) )
68 60 67 sylbird 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( -. ( s + 1 ) < n -> ( -. n = ( s + 1 ) -> n < ( s + 1 ) ) ) )
69 68 impcomd 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( ( -. n = ( s + 1 ) /\ -. ( s + 1 ) < n ) -> n < ( s + 1 ) ) )
70 69 ex 
 |-  ( s e. NN -> ( n e. NN0 -> ( ( -. n = ( s + 1 ) /\ -. ( s + 1 ) < n ) -> n < ( s + 1 ) ) ) )
71 70 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( n e. NN0 -> ( ( -. n = ( s + 1 ) /\ -. ( s + 1 ) < n ) -> n < ( s + 1 ) ) ) )
72 71 imp 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( ( -. n = ( s + 1 ) /\ -. ( s + 1 ) < n ) -> n < ( s + 1 ) ) )
73 72 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( -. n = ( s + 1 ) /\ -. ( s + 1 ) < n ) -> n < ( s + 1 ) ) )
74 10 12 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Grp )
75 74 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> Y e. Grp )
76 75 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> Y e. Grp )
77 22 ad4antr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( N e. Fin /\ R e. Ring ) )
78 24 ad4antlr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> b : ( 0 ... s ) --> B )
79 neqne 
 |-  ( -. n = 0 -> n =/= 0 )
80 79 anim2i 
 |-  ( ( n e. NN0 /\ -. n = 0 ) -> ( n e. NN0 /\ n =/= 0 ) )
81 elnnne0 
 |-  ( n e. NN <-> ( n e. NN0 /\ n =/= 0 ) )
82 80 81 sylibr 
 |-  ( ( n e. NN0 /\ -. n = 0 ) -> n e. NN )
83 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
84 82 83 syl 
 |-  ( ( n e. NN0 /\ -. n = 0 ) -> ( n - 1 ) e. NN0 )
85 84 ad4ant23 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( n - 1 ) e. NN0 )
86 42 ad4antlr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> s e. NN0 )
87 63 simprbda 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n <_ ( s + 1 ) )
88 56 adantr 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n e. RR )
89 1red 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> 1 e. RR )
90 nnre 
 |-  ( s e. NN -> s e. RR )
91 90 ad2antrr 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> s e. RR )
92 88 89 91 lesubaddd 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> ( ( n - 1 ) <_ s <-> n <_ ( s + 1 ) ) )
93 87 92 mpbird 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> ( n - 1 ) <_ s )
94 93 exp31 
 |-  ( s e. NN -> ( n e. NN0 -> ( n < ( s + 1 ) -> ( n - 1 ) <_ s ) ) )
95 94 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( n e. NN0 -> ( n < ( s + 1 ) -> ( n - 1 ) <_ s ) ) )
96 95 imp 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> ( n < ( s + 1 ) -> ( n - 1 ) <_ s ) )
97 96 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( n < ( s + 1 ) -> ( n - 1 ) <_ s ) )
98 97 imp 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( n - 1 ) <_ s )
99 elfz2nn0 
 |-  ( ( n - 1 ) e. ( 0 ... s ) <-> ( ( n - 1 ) e. NN0 /\ s e. NN0 /\ ( n - 1 ) <_ s ) )
100 85 86 98 99 syl3anbrc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( n - 1 ) e. ( 0 ... s ) )
101 78 100 ffvelcdmd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( b ` ( n - 1 ) ) e. B )
102 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( n - 1 ) ) e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ ( b ` ( n - 1 ) ) e. B ) )
103 77 101 102 sylanbrc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( N e. Fin /\ R e. Ring /\ ( b ` ( n - 1 ) ) e. B ) )
104 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( n - 1 ) ) e. B ) -> ( T ` ( b ` ( n - 1 ) ) ) e. ( Base ` Y ) )
105 103 104 syl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( T ` ( b ` ( n - 1 ) ) ) e. ( Base ` Y ) )
106 19 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> Y e. Ring )
107 21 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> ( T ` M ) e. ( Base ` Y ) )
108 45 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> ( N e. Fin /\ R e. Ring /\ s e. NN0 ) )
109 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b e. ( B ^m ( 0 ... s ) ) )
110 109 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> b e. ( B ^m ( 0 ... s ) ) )
111 simplr 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n e. NN0 )
112 25 ad2antrr 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> s e. NN0 )
113 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
114 nnz 
 |-  ( s e. NN -> s e. ZZ )
115 zleltp1 
 |-  ( ( n e. ZZ /\ s e. ZZ ) -> ( n <_ s <-> n < ( s + 1 ) ) )
116 113 114 115 syl2anr 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( n <_ s <-> n < ( s + 1 ) ) )
117 116 biimpar 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n <_ s )
118 elfz2nn0 
 |-  ( n e. ( 0 ... s ) <-> ( n e. NN0 /\ s e. NN0 /\ n <_ s ) )
119 111 112 117 118 syl3anbrc 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n e. ( 0 ... s ) )
120 119 exp31 
 |-  ( s e. NN -> ( n e. NN0 -> ( n < ( s + 1 ) -> n e. ( 0 ... s ) ) ) )
121 120 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( n e. NN0 -> ( n < ( s + 1 ) -> n e. ( 0 ... s ) ) ) )
122 121 imp31 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n e. ( 0 ... s ) )
123 1 2 3 4 8 m2pmfzmap 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) /\ ( b e. ( B ^m ( 0 ... s ) ) /\ n e. ( 0 ... s ) ) ) -> ( T ` ( b ` n ) ) e. ( Base ` Y ) )
124 108 110 122 123 syl12anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> ( T ` ( b ` n ) ) e. ( Base ` Y ) )
125 15 5 ringcl 
 |-  ( ( Y e. Ring /\ ( T ` M ) e. ( Base ` Y ) /\ ( T ` ( b ` n ) ) e. ( Base ` Y ) ) -> ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) e. ( Base ` Y ) )
126 106 107 124 125 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) e. ( Base ` Y ) )
127 126 adantlr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) e. ( Base ` Y ) )
128 15 6 grpsubcl 
 |-  ( ( Y e. Grp /\ ( T ` ( b ` ( n - 1 ) ) ) e. ( Base ` Y ) /\ ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) e. ( Base ` Y ) ) -> ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) e. ( Base ` Y ) )
129 76 105 127 128 syl3anc 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ n < ( s + 1 ) ) -> ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) e. ( Base ` Y ) )
130 129 ex 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( n < ( s + 1 ) -> ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) e. ( Base ` Y ) ) )
131 73 130 syld 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) -> ( ( -. n = ( s + 1 ) /\ -. ( s + 1 ) < n ) -> ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) e. ( Base ` Y ) ) )
132 131 impl 
 |-  ( ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) /\ -. ( s + 1 ) < n ) -> ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) e. ( Base ` Y ) )
133 54 132 ifclda 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) /\ -. n = ( s + 1 ) ) -> if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) e. ( Base ` Y ) )
134 53 133 ifclda 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ -. n = 0 ) -> if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) e. ( Base ` Y ) )
135 41 134 ifclda 
 |-  ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) -> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) e. ( Base ` Y ) )
136 135 9 fmptd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> ( Base ` Y ) )