Metamath Proof Explorer

Theorem chfacfpmmul0

Description: The value of the "characteristic factor function" multiplied with a constant polynomial matrix is zero almost always. (Contributed by AV, 23-Nov-2019)

Ref Expression
Hypotheses cayhamlem1.a 
|- A = ( N Mat R )
cayhamlem1.b 
|- B = ( Base ` A )
cayhamlem1.p 
|- P = ( Poly1 ` R )
cayhamlem1.y 
|- Y = ( N Mat P )
cayhamlem1.r 
|- .X. = ( .r ` Y )
cayhamlem1.s 
|- .- = ( -g ` Y )
cayhamlem1.0 
|- .0. = ( 0g ` Y )
cayhamlem1.t 
|- T = ( N matToPolyMat R )
cayhamlem1.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 ) ) ) ) ) ) ) )
cayhamlem1.e 
|- .^ = ( .g ` ( mulGrp ` Y ) )
Assertion chfacfpmmul0 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. ( ZZ>= ` ( s + 2 ) ) ) -> ( ( K .^ ( T ` M ) ) .X. ( G ` K ) ) = .0. )

Proof

Step Hyp Ref Expression
1 cayhamlem1.a 
 |-  A = ( N Mat R )
2 cayhamlem1.b 
 |-  B = ( Base ` A )
3 cayhamlem1.p 
 |-  P = ( Poly1 ` R )
4 cayhamlem1.y 
 |-  Y = ( N Mat P )
5 cayhamlem1.r 
 |-  .X. = ( .r ` Y )
6 cayhamlem1.s 
 |-  .- = ( -g ` Y )
7 cayhamlem1.0 
 |-  .0. = ( 0g ` Y )
8 cayhamlem1.t 
 |-  T = ( N matToPolyMat R )
9 cayhamlem1.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 cayhamlem1.e 
 |-  .^ = ( .g ` ( mulGrp ` Y ) )
11 eluz2 
 |-  ( K e. ( ZZ>= ` ( s + 2 ) ) <-> ( ( s + 2 ) e. ZZ /\ K e. ZZ /\ ( s + 2 ) <_ K ) )
12 simpll 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> K e. ZZ )
13 nngt0 
 |-  ( s e. NN -> 0 < s )
14 nnre 
 |-  ( s e. NN -> s e. RR )
15 14 adantl 
 |-  ( ( K e. ZZ /\ s e. NN ) -> s e. RR )
16 2rp 
 |-  2 e. RR+
17 16 a1i 
 |-  ( ( K e. ZZ /\ s e. NN ) -> 2 e. RR+ )
18 15 17 ltaddrpd 
 |-  ( ( K e. ZZ /\ s e. NN ) -> s < ( s + 2 ) )
19 0red 
 |-  ( ( K e. ZZ /\ s e. NN ) -> 0 e. RR )
20 2re 
 |-  2 e. RR
21 20 a1i 
 |-  ( ( K e. ZZ /\ s e. NN ) -> 2 e. RR )
22 15 21 readdcld 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( s + 2 ) e. RR )
23 lttr 
 |-  ( ( 0 e. RR /\ s e. RR /\ ( s + 2 ) e. RR ) -> ( ( 0 < s /\ s < ( s + 2 ) ) -> 0 < ( s + 2 ) ) )
24 19 15 22 23 syl3anc 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( 0 < s /\ s < ( s + 2 ) ) -> 0 < ( s + 2 ) ) )
25 18 24 mpan2d 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( 0 < s -> 0 < ( s + 2 ) ) )
26 25 ex 
 |-  ( K e. ZZ -> ( s e. NN -> ( 0 < s -> 0 < ( s + 2 ) ) ) )
27 26 com13 
 |-  ( 0 < s -> ( s e. NN -> ( K e. ZZ -> 0 < ( s + 2 ) ) ) )
28 13 27 mpcom 
 |-  ( s e. NN -> ( K e. ZZ -> 0 < ( s + 2 ) ) )
29 28 impcom 
 |-  ( ( K e. ZZ /\ s e. NN ) -> 0 < ( s + 2 ) )
30 zre 
 |-  ( K e. ZZ -> K e. RR )
31 30 adantr 
 |-  ( ( K e. ZZ /\ s e. NN ) -> K e. RR )
32 ltleletr 
 |-  ( ( 0 e. RR /\ ( s + 2 ) e. RR /\ K e. RR ) -> ( ( 0 < ( s + 2 ) /\ ( s + 2 ) <_ K ) -> 0 <_ K ) )
33 19 22 31 32 syl3anc 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( 0 < ( s + 2 ) /\ ( s + 2 ) <_ K ) -> 0 <_ K ) )
34 29 33 mpand 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 2 ) <_ K -> 0 <_ K ) )
35 34 imp 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> 0 <_ K )
36 elnn0z 
 |-  ( K e. NN0 <-> ( K e. ZZ /\ 0 <_ K ) )
37 12 35 36 sylanbrc 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> K e. NN0 )
38 nncn 
 |-  ( s e. NN -> s e. CC )
39 add1p1 
 |-  ( s e. CC -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
40 38 39 syl 
 |-  ( s e. NN -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
41 40 adantl 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
42 41 eqcomd 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( s + 2 ) = ( ( s + 1 ) + 1 ) )
43 42 breq1d 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 2 ) <_ K <-> ( ( s + 1 ) + 1 ) <_ K ) )
44 nnz 
 |-  ( s e. NN -> s e. ZZ )
45 44 peano2zd 
 |-  ( s e. NN -> ( s + 1 ) e. ZZ )
46 45 anim2i 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( K e. ZZ /\ ( s + 1 ) e. ZZ ) )
47 46 ancomd 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 1 ) e. ZZ /\ K e. ZZ ) )
48 zltp1le 
 |-  ( ( ( s + 1 ) e. ZZ /\ K e. ZZ ) -> ( ( s + 1 ) < K <-> ( ( s + 1 ) + 1 ) <_ K ) )
49 48 bicomd 
 |-  ( ( ( s + 1 ) e. ZZ /\ K e. ZZ ) -> ( ( ( s + 1 ) + 1 ) <_ K <-> ( s + 1 ) < K ) )
50 47 49 syl 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( ( s + 1 ) + 1 ) <_ K <-> ( s + 1 ) < K ) )
51 43 50 bitrd 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 2 ) <_ K <-> ( s + 1 ) < K ) )
52 51 biimpa 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> ( s + 1 ) < K )
53 37 52 jca 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> ( K e. NN0 /\ ( s + 1 ) < K ) )
54 53 ex 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 2 ) <_ K -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
55 54 impancom 
 |-  ( ( K e. ZZ /\ ( s + 2 ) <_ K ) -> ( s e. NN -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
56 55 3adant1 
 |-  ( ( ( s + 2 ) e. ZZ /\ K e. ZZ /\ ( s + 2 ) <_ K ) -> ( s e. NN -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
57 56 com12 
 |-  ( s e. NN -> ( ( ( s + 2 ) e. ZZ /\ K e. ZZ /\ ( s + 2 ) <_ K ) -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
58 11 57 syl5bi 
 |-  ( s e. NN -> ( K e. ( ZZ>= ` ( s + 2 ) ) -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
59 58 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( K e. ( ZZ>= ` ( s + 2 ) ) -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
60 59 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( K e. ( ZZ>= ` ( s + 2 ) ) -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
61 0red 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> 0 e. RR )
62 peano2re 
 |-  ( s e. RR -> ( s + 1 ) e. RR )
63 14 62 syl 
 |-  ( s e. NN -> ( s + 1 ) e. RR )
64 63 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( s + 1 ) e. RR )
65 64 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. RR )
66 65 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> ( s + 1 ) e. RR )
67 nn0re 
 |-  ( K e. NN0 -> K e. RR )
68 67 ad2antlr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> K e. RR )
69 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
70 69 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
71 70 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> s e. NN0 )
72 nn0p1gt0 
 |-  ( s e. NN0 -> 0 < ( s + 1 ) )
73 71 72 syl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> 0 < ( s + 1 ) )
74 73 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> 0 < ( s + 1 ) )
75 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> ( s + 1 ) < K )
76 61 66 68 74 75 lttrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> 0 < K )
77 76 gt0ne0d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> K =/= 0 )
78 77 neneqd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> -. K = 0 )
79 78 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> -. K = 0 )
80 eqeq1 
 |-  ( n = K -> ( n = 0 <-> K = 0 ) )
81 80 notbid 
 |-  ( n = K -> ( -. n = 0 <-> -. K = 0 ) )
82 81 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> ( -. n = 0 <-> -. K = 0 ) )
83 79 82 mpbird 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> -. n = 0 )
84 83 iffalsed 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> 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 ) ) ) ) ) ) ) = if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) )
85 64 ad2antlr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( s + 1 ) e. RR )
86 ltne 
 |-  ( ( ( s + 1 ) e. RR /\ ( s + 1 ) < K ) -> K =/= ( s + 1 ) )
87 85 86 sylan 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> K =/= ( s + 1 ) )
88 87 neneqd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> -. K = ( s + 1 ) )
89 88 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> -. K = ( s + 1 ) )
90 eqeq1 
 |-  ( n = K -> ( n = ( s + 1 ) <-> K = ( s + 1 ) ) )
91 90 notbid 
 |-  ( n = K -> ( -. n = ( s + 1 ) <-> -. K = ( s + 1 ) ) )
92 91 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> ( -. n = ( s + 1 ) <-> -. K = ( s + 1 ) ) )
93 89 92 mpbird 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> -. n = ( s + 1 ) )
94 93 iffalsed 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) = if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) )
95 simplr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> ( s + 1 ) < K )
96 breq2 
 |-  ( n = K -> ( ( s + 1 ) < n <-> ( s + 1 ) < K ) )
97 96 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> ( ( s + 1 ) < n <-> ( s + 1 ) < K ) )
98 95 97 mpbird 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> ( s + 1 ) < n )
99 98 iftrued 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) = .0. )
100 84 94 99 3eqtrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) /\ n = K ) -> 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 ) ) ) ) ) ) ) = .0. )
101 simplr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> K e. NN0 )
102 7 fvexi 
 |-  .0. e. _V
103 102 a1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> .0. e. _V )
104 9 100 101 103 fvmptd2 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> ( G ` K ) = .0. )
105 104 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> ( ( K .^ ( T ` M ) ) .X. ( G ` K ) ) = ( ( K .^ ( T ` M ) ) .X. .0. ) )
106 crngring 
 |-  ( R e. CRing -> R e. Ring )
107 3 4 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. Ring )
108 106 107 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. Ring )
109 108 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. Ring )
110 109 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> Y e. Ring )
111 110 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> Y e. Ring )
112 eqid 
 |-  ( mulGrp ` Y ) = ( mulGrp ` Y )
113 112 ringmgp 
 |-  ( Y e. Ring -> ( mulGrp ` Y ) e. Mnd )
114 109 113 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` Y ) e. Mnd )
115 114 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( mulGrp ` Y ) e. Mnd )
116 simpr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> K e. NN0 )
117 8 1 2 3 4 mat2pmatbas 
 |-  ( ( N e. Fin /\ R e. Ring /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
118 106 117 syl3an2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( T ` M ) e. ( Base ` Y ) )
119 118 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( T ` M ) e. ( Base ` Y ) )
120 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
121 112 120 mgpbas 
 |-  ( Base ` Y ) = ( Base ` ( mulGrp ` Y ) )
122 121 10 mulgnn0cl 
 |-  ( ( ( mulGrp ` Y ) e. Mnd /\ K e. NN0 /\ ( T ` M ) e. ( Base ` Y ) ) -> ( K .^ ( T ` M ) ) e. ( Base ` Y ) )
123 115 116 119 122 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( K .^ ( T ` M ) ) e. ( Base ` Y ) )
124 123 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> ( K .^ ( T ` M ) ) e. ( Base ` Y ) )
125 120 5 7 ringrz 
 |-  ( ( Y e. Ring /\ ( K .^ ( T ` M ) ) e. ( Base ` Y ) ) -> ( ( K .^ ( T ` M ) ) .X. .0. ) = .0. )
126 111 124 125 syl2anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> ( ( K .^ ( T ` M ) ) .X. .0. ) = .0. )
127 105 126 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) /\ ( s + 1 ) < K ) -> ( ( K .^ ( T ` M ) ) .X. ( G ` K ) ) = .0. )
128 127 expl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( K e. NN0 /\ ( s + 1 ) < K ) -> ( ( K .^ ( T ` M ) ) .X. ( G ` K ) ) = .0. ) )
129 60 128 syld 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( K e. ( ZZ>= ` ( s + 2 ) ) -> ( ( K .^ ( T ` M ) ) .X. ( G ` K ) ) = .0. ) )
130 129 3impia 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. ( ZZ>= ` ( s + 2 ) ) ) -> ( ( K .^ ( T ` M ) ) .X. ( G ` K ) ) = .0. )