Metamath Proof Explorer

Theorem chfacfscmul0

Description: A scaled value of the "characteristic factor function" is zero almost always. (Contributed by AV, 9-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 ) ) ) ) ) ) ) )
chfacfscmulcl.x 
|- X = ( var1 ` R )
chfacfscmulcl.m 
|- .x. = ( .s ` Y )
chfacfscmulcl.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
Assertion chfacfscmul0 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. ( ZZ>= ` ( s + 2 ) ) ) -> ( ( K .^ X ) .x. ( G ` K ) ) = .0. )

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 chfacfscmulcl.x 
 |-  X = ( var1 ` R )
11 chfacfscmulcl.m 
 |-  .x. = ( .s ` Y )
12 chfacfscmulcl.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
13 eluz2 
 |-  ( K e. ( ZZ>= ` ( s + 2 ) ) <-> ( ( s + 2 ) e. ZZ /\ K e. ZZ /\ ( s + 2 ) <_ K ) )
14 simpll 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> K e. ZZ )
15 nngt0 
 |-  ( s e. NN -> 0 < s )
16 nnre 
 |-  ( s e. NN -> s e. RR )
17 16 adantl 
 |-  ( ( K e. ZZ /\ s e. NN ) -> s e. RR )
18 2rp 
 |-  2 e. RR+
19 18 a1i 
 |-  ( ( K e. ZZ /\ s e. NN ) -> 2 e. RR+ )
20 17 19 ltaddrpd 
 |-  ( ( K e. ZZ /\ s e. NN ) -> s < ( s + 2 ) )
21 0red 
 |-  ( ( K e. ZZ /\ s e. NN ) -> 0 e. RR )
22 2re 
 |-  2 e. RR
23 22 a1i 
 |-  ( ( K e. ZZ /\ s e. NN ) -> 2 e. RR )
24 17 23 readdcld 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( s + 2 ) e. RR )
25 lttr 
 |-  ( ( 0 e. RR /\ s e. RR /\ ( s + 2 ) e. RR ) -> ( ( 0 < s /\ s < ( s + 2 ) ) -> 0 < ( s + 2 ) ) )
26 21 17 24 25 syl3anc 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( 0 < s /\ s < ( s + 2 ) ) -> 0 < ( s + 2 ) ) )
27 20 26 mpan2d 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( 0 < s -> 0 < ( s + 2 ) ) )
28 27 ex 
 |-  ( K e. ZZ -> ( s e. NN -> ( 0 < s -> 0 < ( s + 2 ) ) ) )
29 28 com13 
 |-  ( 0 < s -> ( s e. NN -> ( K e. ZZ -> 0 < ( s + 2 ) ) ) )
30 15 29 mpcom 
 |-  ( s e. NN -> ( K e. ZZ -> 0 < ( s + 2 ) ) )
31 30 impcom 
 |-  ( ( K e. ZZ /\ s e. NN ) -> 0 < ( s + 2 ) )
32 zre 
 |-  ( K e. ZZ -> K e. RR )
33 32 adantr 
 |-  ( ( K e. ZZ /\ s e. NN ) -> K e. RR )
34 ltleletr 
 |-  ( ( 0 e. RR /\ ( s + 2 ) e. RR /\ K e. RR ) -> ( ( 0 < ( s + 2 ) /\ ( s + 2 ) <_ K ) -> 0 <_ K ) )
35 21 24 33 34 syl3anc 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( 0 < ( s + 2 ) /\ ( s + 2 ) <_ K ) -> 0 <_ K ) )
36 31 35 mpand 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 2 ) <_ K -> 0 <_ K ) )
37 36 imp 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> 0 <_ K )
38 elnn0z 
 |-  ( K e. NN0 <-> ( K e. ZZ /\ 0 <_ K ) )
39 14 37 38 sylanbrc 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> K e. NN0 )
40 nncn 
 |-  ( s e. NN -> s e. CC )
41 add1p1 
 |-  ( s e. CC -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
42 40 41 syl 
 |-  ( s e. NN -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
43 42 adantl 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 1 ) + 1 ) = ( s + 2 ) )
44 43 eqcomd 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( s + 2 ) = ( ( s + 1 ) + 1 ) )
45 44 breq1d 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 2 ) <_ K <-> ( ( s + 1 ) + 1 ) <_ K ) )
46 nnz 
 |-  ( s e. NN -> s e. ZZ )
47 46 peano2zd 
 |-  ( s e. NN -> ( s + 1 ) e. ZZ )
48 47 anim2i 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( K e. ZZ /\ ( s + 1 ) e. ZZ ) )
49 48 ancomd 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 1 ) e. ZZ /\ K e. ZZ ) )
50 zltp1le 
 |-  ( ( ( s + 1 ) e. ZZ /\ K e. ZZ ) -> ( ( s + 1 ) < K <-> ( ( s + 1 ) + 1 ) <_ K ) )
51 50 bicomd 
 |-  ( ( ( s + 1 ) e. ZZ /\ K e. ZZ ) -> ( ( ( s + 1 ) + 1 ) <_ K <-> ( s + 1 ) < K ) )
52 49 51 syl 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( ( s + 1 ) + 1 ) <_ K <-> ( s + 1 ) < K ) )
53 45 52 bitrd 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 2 ) <_ K <-> ( s + 1 ) < K ) )
54 53 biimpa 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> ( s + 1 ) < K )
55 39 54 jca 
 |-  ( ( ( K e. ZZ /\ s e. NN ) /\ ( s + 2 ) <_ K ) -> ( K e. NN0 /\ ( s + 1 ) < K ) )
56 55 ex 
 |-  ( ( K e. ZZ /\ s e. NN ) -> ( ( s + 2 ) <_ K -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
57 56 impancom 
 |-  ( ( K e. ZZ /\ ( s + 2 ) <_ K ) -> ( s e. NN -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
58 57 3adant1 
 |-  ( ( ( s + 2 ) e. ZZ /\ K e. ZZ /\ ( s + 2 ) <_ K ) -> ( s e. NN -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
59 58 com12 
 |-  ( s e. NN -> ( ( ( s + 2 ) e. ZZ /\ K e. ZZ /\ ( s + 2 ) <_ K ) -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
60 13 59 syl5bi 
 |-  ( s e. NN -> ( K e. ( ZZ>= ` ( s + 2 ) ) -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
61 60 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( K e. ( ZZ>= ` ( s + 2 ) ) -> ( K e. NN0 /\ ( s + 1 ) < K ) ) )
62 61 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 ) ) )
63 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 )
64 peano2re 
 |-  ( s e. RR -> ( s + 1 ) e. RR )
65 16 64 syl 
 |-  ( s e. NN -> ( s + 1 ) e. RR )
66 65 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( s + 1 ) e. RR )
67 66 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( s + 1 ) e. RR )
68 67 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 )
69 nn0re 
 |-  ( K e. NN0 -> K e. RR )
70 69 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 )
71 nnnn0 
 |-  ( s e. NN -> s e. NN0 )
72 71 adantr 
 |-  ( ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) -> s e. NN0 )
73 72 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 )
74 nn0p1gt0 
 |-  ( s e. NN0 -> 0 < ( s + 1 ) )
75 73 74 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 ) )
76 75 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 ) )
77 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 )
78 63 68 70 76 77 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 )
79 78 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 )
80 79 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 )
81 80 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 )
82 eqeq1 
 |-  ( n = K -> ( n = 0 <-> K = 0 ) )
83 82 notbid 
 |-  ( n = K -> ( -. n = 0 <-> -. K = 0 ) )
84 83 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 ) )
85 81 84 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 )
86 85 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 ) ) ) ) ) ) )
87 66 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 )
88 ltne 
 |-  ( ( ( s + 1 ) e. RR /\ ( s + 1 ) < K ) -> K =/= ( s + 1 ) )
89 87 88 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 ) )
90 89 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 ) )
91 90 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 ) )
92 eqeq1 
 |-  ( n = K -> ( n = ( s + 1 ) <-> K = ( s + 1 ) ) )
93 92 notbid 
 |-  ( n = K -> ( -. n = ( s + 1 ) <-> -. K = ( s + 1 ) ) )
94 93 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 ) ) )
95 91 94 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 ) )
96 95 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 ) ) ) ) ) )
97 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 )
98 breq2 
 |-  ( n = K -> ( ( s + 1 ) < n <-> ( s + 1 ) < K ) )
99 98 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 ) )
100 97 99 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 )
101 100 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. )
102 86 96 101 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. )
103 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 )
104 7 fvexi 
 |-  .0. e. _V
105 104 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 )
106 9 102 103 105 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. )
107 106 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 .^ X ) .x. ( G ` K ) ) = ( ( K .^ X ) .x. .0. ) )
108 crngring 
 |-  ( R e. CRing -> R e. Ring )
109 3 4 pmatlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. LMod )
110 108 109 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. LMod )
111 110 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. LMod )
112 111 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> Y e. LMod )
113 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
114 108 113 syl 
 |-  ( R e. CRing -> P e. Ring )
115 114 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
116 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
117 116 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
118 115 117 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
119 118 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( mulGrp ` P ) e. Mnd )
120 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 )
121 108 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
122 eqid 
 |-  ( Base ` P ) = ( Base ` P )
123 10 3 122 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
124 121 123 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` P ) )
125 124 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> X e. ( Base ` P ) )
126 116 122 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
127 126 12 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ K e. NN0 /\ X e. ( Base ` P ) ) -> ( K .^ X ) e. ( Base ` P ) )
128 119 120 125 127 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( K .^ X ) e. ( Base ` P ) )
129 3 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
130 129 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
131 130 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
132 4 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
133 131 132 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = ( Scalar ` Y ) )
134 133 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` Y ) = P )
135 134 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
136 135 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( K .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( K .^ X ) e. ( Base ` P ) ) )
137 136 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( ( K .^ X ) e. ( Base ` ( Scalar ` Y ) ) <-> ( K .^ X ) e. ( Base ` P ) ) )
138 128 137 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( K .^ X ) e. ( Base ` ( Scalar ` Y ) ) )
139 112 138 jca 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) /\ K e. NN0 ) -> ( Y e. LMod /\ ( K .^ X ) e. ( Base ` ( Scalar ` Y ) ) ) )
140 139 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 ) -> ( Y e. LMod /\ ( K .^ X ) e. ( Base ` ( Scalar ` Y ) ) ) )
141 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
142 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
143 141 11 142 7 lmodvs0 
 |-  ( ( Y e. LMod /\ ( K .^ X ) e. ( Base ` ( Scalar ` Y ) ) ) -> ( ( K .^ X ) .x. .0. ) = .0. )
144 140 143 syl 
 |-  ( ( ( ( ( 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 .^ X ) .x. .0. ) = .0. )
145 107 144 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 .^ X ) .x. ( G ` K ) ) = .0. )
146 145 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 .^ X ) .x. ( G ` K ) ) = .0. ) )
147 62 146 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 .^ X ) .x. ( G ` K ) ) = .0. ) )
148 147 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 .^ X ) .x. ( G ` K ) ) = .0. )