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 ) ) |