Metamath Proof Explorer

Theorem cpmidpmatlem3

Description: Lemma 3 for cpmidpmat . (Contributed by AV, 14-Nov-2019) (Proof shortened by AV, 7-Dec-2019)

Ref Expression
Hypotheses cpmidgsum.a 
|- A = ( N Mat R )
cpmidgsum.b 
|- B = ( Base ` A )
cpmidgsum.p 
|- P = ( Poly1 ` R )
cpmidgsum.y 
|- Y = ( N Mat P )
cpmidgsum.x 
|- X = ( var1 ` R )
cpmidgsum.e 
|- .^ = ( .g ` ( mulGrp ` P ) )
cpmidgsum.m 
|- .x. = ( .s ` Y )
cpmidgsum.1 
|- .1. = ( 1r ` Y )
cpmidgsum.u 
|- U = ( algSc ` P )
cpmidgsum.c 
|- C = ( N CharPlyMat R )
cpmidgsum.k 
|- K = ( C ` M )
cpmidgsum.h 
|- H = ( K .x. .1. )
cpmidgsumm2pm.o 
|- O = ( 1r ` A )
cpmidgsumm2pm.m 
|- .* = ( .s ` A )
cpmidgsumm2pm.t 
|- T = ( N matToPolyMat R )
cpmidpmat.g 
|- G = ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) )
Assertion cpmidpmatlem3 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> G finSupp ( 0g ` A ) )

Proof

Step Hyp Ref Expression
1 cpmidgsum.a 
 |-  A = ( N Mat R )
2 cpmidgsum.b 
 |-  B = ( Base ` A )
3 cpmidgsum.p 
 |-  P = ( Poly1 ` R )
4 cpmidgsum.y 
 |-  Y = ( N Mat P )
5 cpmidgsum.x 
 |-  X = ( var1 ` R )
6 cpmidgsum.e 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
7 cpmidgsum.m 
 |-  .x. = ( .s ` Y )
8 cpmidgsum.1 
 |-  .1. = ( 1r ` Y )
9 cpmidgsum.u 
 |-  U = ( algSc ` P )
10 cpmidgsum.c 
 |-  C = ( N CharPlyMat R )
11 cpmidgsum.k 
 |-  K = ( C ` M )
12 cpmidgsum.h 
 |-  H = ( K .x. .1. )
13 cpmidgsumm2pm.o 
 |-  O = ( 1r ` A )
14 cpmidgsumm2pm.m 
 |-  .* = ( .s ` A )
15 cpmidgsumm2pm.t 
 |-  T = ( N matToPolyMat R )
16 cpmidpmat.g 
 |-  G = ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) )
17 fvexd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0g ` A ) e. _V )
18 ovexd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ k e. NN0 ) -> ( ( ( coe1 ` K ) ` k ) .* O ) e. _V )
19 fveq2 
 |-  ( k = l -> ( ( coe1 ` K ) ` k ) = ( ( coe1 ` K ) ` l ) )
20 19 oveq1d 
 |-  ( k = l -> ( ( ( coe1 ` K ) ` k ) .* O ) = ( ( ( coe1 ` K ) ` l ) .* O ) )
21 fvexd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( 0g ` R ) e. _V )
22 eqid 
 |-  ( Base ` P ) = ( Base ` P )
23 10 1 2 3 22 chpmatply1 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) e. ( Base ` P ) )
24 11 23 eqeltrid 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> K e. ( Base ` P ) )
25 eqid 
 |-  ( coe1 ` K ) = ( coe1 ` K )
26 eqid 
 |-  ( Base ` R ) = ( Base ` R )
27 25 22 3 26 coe1fvalcl 
 |-  ( ( K e. ( Base ` P ) /\ n e. NN0 ) -> ( ( coe1 ` K ) ` n ) e. ( Base ` R ) )
28 24 27 sylan 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ n e. NN0 ) -> ( ( coe1 ` K ) ` n ) e. ( Base ` R ) )
29 crngring 
 |-  ( R e. CRing -> R e. Ring )
30 29 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
31 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
32 3 22 31 mptcoe1fsupp 
 |-  ( ( R e. Ring /\ K e. ( Base ` P ) ) -> ( n e. NN0 |-> ( ( coe1 ` K ) ` n ) ) finSupp ( 0g ` R ) )
33 30 24 32 syl2anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( n e. NN0 |-> ( ( coe1 ` K ) ` n ) ) finSupp ( 0g ` R ) )
34 21 28 33 mptnn0fsuppr 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 A. l e. NN0 ( s < l -> [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) )
35 csbfv 
 |-  [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( ( coe1 ` K ) ` l )
36 35 a1i 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) -> [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( ( coe1 ` K ) ` l ) )
37 36 eqeq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) -> ( [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) <-> ( ( coe1 ` K ) ` l ) = ( 0g ` R ) ) )
38 37 biimpa 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) /\ [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> ( ( coe1 ` K ) ` l ) = ( 0g ` R ) )
39 1 matsca2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` A ) )
40 39 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R = ( Scalar ` A ) )
41 40 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) /\ [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> R = ( Scalar ` A ) )
42 41 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) /\ [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` A ) ) )
43 38 42 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) /\ [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> ( ( coe1 ` K ) ` l ) = ( 0g ` ( Scalar ` A ) ) )
44 43 oveq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) /\ [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> ( ( ( coe1 ` K ) ` l ) .* O ) = ( ( 0g ` ( Scalar ` A ) ) .* O ) )
45 1 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
46 29 45 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. LMod )
47 46 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> A e. LMod )
48 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
49 29 48 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
50 2 13 ringidcl 
 |-  ( A e. Ring -> O e. B )
51 49 50 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> O e. B )
52 51 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> O e. B )
53 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
54 eqid 
 |-  ( 0g ` ( Scalar ` A ) ) = ( 0g ` ( Scalar ` A ) )
55 eqid 
 |-  ( 0g ` A ) = ( 0g ` A )
56 2 53 14 54 55 lmod0vs 
 |-  ( ( A e. LMod /\ O e. B ) -> ( ( 0g ` ( Scalar ` A ) ) .* O ) = ( 0g ` A ) )
57 47 52 56 syl2anc 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( 0g ` ( Scalar ` A ) ) .* O ) = ( 0g ` A ) )
58 57 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) /\ [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> ( ( 0g ` ( Scalar ` A ) ) .* O ) = ( 0g ` A ) )
59 44 58 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) /\ [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> ( ( ( coe1 ` K ) ` l ) .* O ) = ( 0g ` A ) )
60 59 ex 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) -> ( [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) -> ( ( ( coe1 ` K ) ` l ) .* O ) = ( 0g ` A ) ) )
61 60 imim2d 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ l e. NN0 ) -> ( ( s < l -> [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> ( s < l -> ( ( ( coe1 ` K ) ` l ) .* O ) = ( 0g ` A ) ) ) )
62 61 ralimdva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( A. l e. NN0 ( s < l -> [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> A. l e. NN0 ( s < l -> ( ( ( coe1 ` K ) ` l ) .* O ) = ( 0g ` A ) ) ) )
63 62 reximdv 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN0 A. l e. NN0 ( s < l -> [_ l / n ]_ ( ( coe1 ` K ) ` n ) = ( 0g ` R ) ) -> E. s e. NN0 A. l e. NN0 ( s < l -> ( ( ( coe1 ` K ) ` l ) .* O ) = ( 0g ` A ) ) ) )
64 34 63 mpd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN0 A. l e. NN0 ( s < l -> ( ( ( coe1 ` K ) ` l ) .* O ) = ( 0g ` A ) ) )
65 17 18 20 64 mptnn0fsuppd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( k e. NN0 |-> ( ( ( coe1 ` K ) ` k ) .* O ) ) finSupp ( 0g ` A ) )
66 16 65 eqbrtrid 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> G finSupp ( 0g ` A ) )