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 ffvelrnd
 |-  ( ( 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 syl5bir
 |-  ( ( 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 ffvelrnd
 |-  ( ( ( ( ( ( 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 ) )