Metamath Proof Explorer

Theorem chfacfisfcpmat

Description: The "characteristic factor function" is a function from the nonnegative integers to constant polynomial matrices. (Contributed by AV, 19-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 ) ) ) ) ) ) ) )
chfacfisfcpmat.s 
|- S = ( N ConstPolyMat R )
Assertion chfacfisfcpmat 
|- ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> S )

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 chfacfisfcpmat.s 
 |-  S = ( N ConstPolyMat R )
11 10 3 4 cpmatsubgpmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` Y ) )
12 11 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> S e. ( SubGrp ` Y ) )
13 12 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> S e. ( SubGrp ` Y ) )
14 subgsubm 
 |-  ( S e. ( SubGrp ` Y ) -> S e. ( SubMnd ` Y ) )
15 7 subm0cl 
 |-  ( S e. ( SubMnd ` Y ) -> .0. e. S )
16 12 14 15 3syl 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> .0. e. S )
17 16 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> .0. e. S )
18 10 3 4 cpmatsrgpmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubRing ` Y ) )
19 18 3adant3 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> S e. ( SubRing ` Y ) )
20 19 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> S e. ( SubRing ` Y ) )
21 10 8 1 2 m2cpm 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. S )
22 21 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` M ) e. S )
23 3simpa 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
24 elmapi 
 |-  ( b e. ( B ^m ( 0 ... s ) ) -> b : ( 0 ... s ) --> B )
25 24 adantl 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> b : ( 0 ... s ) --> B )
26 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
27 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
28 26 27 eleqtrdi 
 |-  ( s e. NN -> s e. ( ZZ>= ` 0 ) )
29 eluzfz1 
 |-  ( s e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... s ) )
30 28 29 syl 
 |-  ( s e. NN -> 0 e. ( 0 ... s ) )
31 30 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> 0 e. ( 0 ... s ) )
32 25 31 ffvelcdmd 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( b ` 0 ) e. B )
33 23 32 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 ) )
34 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ ( b ` 0 ) e. B ) )
35 33 34 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 ) )
36 10 8 1 2 m2cpm 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` 0 ) e. B ) -> ( T ` ( b ` 0 ) ) e. S )
37 35 36 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` 0 ) ) e. S )
38 5 subrgmcl 
 |-  ( ( S e. ( SubRing ` Y ) /\ ( T ` M ) e. S /\ ( T ` ( b ` 0 ) ) e. S ) -> ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. S )
39 20 22 37 38 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. S )
40 6 subgsubcl 
 |-  ( ( S e. ( SubGrp ` Y ) /\ .0. e. S /\ ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) e. S ) -> ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) e. S )
41 13 17 39 40 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. S )
42 41 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. S )
43 simpl1 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> N e. Fin )
44 simpl2 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> R e. Ring )
45 25 adantl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> b : ( 0 ... s ) --> B )
46 eluzfz2 
 |-  ( s e. ( ZZ>= ` 0 ) -> s e. ( 0 ... s ) )
47 28 46 syl 
 |-  ( s e. NN -> s e. ( 0 ... s ) )
48 47 ad2antrl 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> s e. ( 0 ... s ) )
49 45 48 ffvelcdmd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( b ` s ) e. B )
50 10 8 1 2 m2cpm 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` s ) e. B ) -> ( T ` ( b ` s ) ) e. S )
51 43 44 49 50 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( T ` ( b ` s ) ) e. S )
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. S )
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. S )
54 17 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. S )
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 12 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 e. ( SubGrp ` Y ) )
75 23 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 ) )
76 25 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 )
77 neqne 
 |-  ( -. n = 0 -> n =/= 0 )
78 77 anim2i 
 |-  ( ( n e. NN0 /\ -. n = 0 ) -> ( n e. NN0 /\ n =/= 0 ) )
79 elnnne0 
 |-  ( n e. NN <-> ( n e. NN0 /\ n =/= 0 ) )
80 78 79 sylibr 
 |-  ( ( n e. NN0 /\ -. n = 0 ) -> n e. NN )
81 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
82 80 81 syl 
 |-  ( ( n e. NN0 /\ -. n = 0 ) -> ( n - 1 ) e. NN0 )
83 82 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 )
84 26 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
85 84 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 )
86 63 simprbda 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n <_ ( s + 1 ) )
87 56 adantr 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n e. RR )
88 1red 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> 1 e. RR )
89 nnre 
 |-  ( s e. NN -> s e. RR )
90 89 ad2antrr 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> s e. RR )
91 87 88 90 lesubaddd 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> ( ( n - 1 ) <_ s <-> n <_ ( s + 1 ) ) )
92 86 91 mpbird 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> ( n - 1 ) <_ s )
93 92 exp31 
 |-  ( s e. NN -> ( n e. NN0 -> ( n < ( s + 1 ) -> ( n - 1 ) <_ s ) ) )
94 93 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 ) ) )
95 94 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 ) )
96 95 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 ) )
97 96 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 )
98 elfz2nn0 
 |-  ( ( n - 1 ) e. ( 0 ... s ) <-> ( ( n - 1 ) e. NN0 /\ s e. NN0 /\ ( n - 1 ) <_ s ) )
99 83 85 97 98 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 ) )
100 76 99 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 )
101 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( n - 1 ) ) e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ ( b ` ( n - 1 ) ) e. B ) )
102 75 100 101 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 ) )
103 10 8 1 2 m2cpm 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` ( n - 1 ) ) e. B ) -> ( T ` ( b ` ( n - 1 ) ) ) e. S )
104 102 103 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. S )
105 20 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 ) ) -> S e. ( SubRing ` Y ) )
106 22 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. S )
107 23 84 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 ) )
108 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ s e. NN0 ) <-> ( ( N e. Fin /\ R e. Ring ) /\ s e. NN0 ) )
109 107 108 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 ) )
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 ) ) -> ( N e. Fin /\ R e. Ring /\ s e. NN0 ) )
111 110 simp1d 
 |-  ( ( ( ( ( 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 )
112 110 simp2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> R e. Ring )
113 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 ) ) -> b : ( 0 ... s ) --> B )
114 simplr 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n e. NN0 )
115 26 ad2antrr 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> s e. NN0 )
116 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
117 nnz 
 |-  ( s e. NN -> s e. ZZ )
118 zleltp1 
 |-  ( ( n e. ZZ /\ s e. ZZ ) -> ( n <_ s <-> n < ( s + 1 ) ) )
119 116 117 118 syl2anr 
 |-  ( ( s e. NN /\ n e. NN0 ) -> ( n <_ s <-> n < ( s + 1 ) ) )
120 119 biimpar 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n <_ s )
121 elfz2nn0 
 |-  ( n e. ( 0 ... s ) <-> ( n e. NN0 /\ s e. NN0 /\ n <_ s ) )
122 114 115 120 121 syl3anbrc 
 |-  ( ( ( s e. NN /\ n e. NN0 ) /\ n < ( s + 1 ) ) -> n e. ( 0 ... s ) )
123 122 exp31 
 |-  ( s e. NN -> ( n e. NN0 -> ( n < ( s + 1 ) -> n e. ( 0 ... s ) ) ) )
124 123 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 ) ) ) )
125 124 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 ) )
126 113 125 ffvelcdmd 
 |-  ( ( ( ( ( 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 ` n ) e. B )
127 10 8 1 2 m2cpm 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( b ` n ) e. B ) -> ( T ` ( b ` n ) ) e. S )
128 111 112 126 127 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 ` ( b ` n ) ) e. S )
129 5 subrgmcl 
 |-  ( ( S e. ( SubRing ` Y ) /\ ( T ` M ) e. S /\ ( T ` ( b ` n ) ) e. S ) -> ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) e. S )
130 105 106 128 129 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. S )
131 130 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. S )
132 6 subgsubcl 
 |-  ( ( S e. ( SubGrp ` Y ) /\ ( T ` ( b ` ( n - 1 ) ) ) e. S /\ ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) e. S ) -> ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) e. S )
133 74 104 131 132 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. S )
134 133 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. S ) )
135 73 134 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. S ) )
136 135 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. S )
137 54 136 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. S )
138 53 137 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. S )
139 42 138 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. S )
140 139 9 fmptd 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> S )