Metamath Proof Explorer

Theorem chfacfscmulcl

Description: Closure of a scaled value of the "characteristic factor function". (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 chfacfscmulcl 
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. NN0 ) -> ( ( K .^ X ) .x. ( G ` K ) ) e. ( Base ` Y ) )

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 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 3 4 pmatlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> Y e. LMod )
15 13 14 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> Y e. LMod )
16 15 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> Y e. LMod )
17 16 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. NN0 ) -> Y e. LMod )
18 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
19 13 18 syl 
 |-  ( R e. CRing -> P e. Ring )
20 19 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P e. Ring )
21 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
22 21 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
23 20 22 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` P ) e. Mnd )
24 23 3ad2ant1 
 |-  ( ( ( 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 )
25 simp3 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. NN0 ) -> K e. NN0 )
26 13 3ad2ant2 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R e. Ring )
27 eqid 
 |-  ( Base ` P ) = ( Base ` P )
28 10 3 27 vr1cl 
 |-  ( R e. Ring -> X e. ( Base ` P ) )
29 26 28 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> X e. ( Base ` P ) )
30 29 3ad2ant1 
 |-  ( ( ( 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 ) )
31 21 27 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
32 31 12 mulgnn0cl 
 |-  ( ( ( mulGrp ` P ) e. Mnd /\ K e. NN0 /\ X e. ( Base ` P ) ) -> ( K .^ X ) e. ( Base ` P ) )
33 24 25 30 32 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 ) )
34 3 ply1crng 
 |-  ( R e. CRing -> P e. CRing )
35 34 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ P e. CRing ) )
36 35 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ P e. CRing ) )
37 4 matsca2 
 |-  ( ( N e. Fin /\ P e. CRing ) -> P = ( Scalar ` Y ) )
38 36 37 syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> P = ( Scalar ` Y ) )
39 38 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Scalar ` Y ) = P )
40 39 fveq2d 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
41 40 3ad2ant1 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. NN0 ) -> ( Base ` ( Scalar ` Y ) ) = ( Base ` P ) )
42 33 41 eleqtrrd 
 |-  ( ( ( 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 ) ) )
43 1 2 3 4 5 6 7 8 9 chfacfisf 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> ( Base ` Y ) )
44 13 43 syl3anl2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> G : NN0 --> ( Base ` Y ) )
45 44 3adant3 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. NN0 ) -> G : NN0 --> ( Base ` Y ) )
46 45 25 ffvelrnd 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. NN0 ) -> ( G ` K ) e. ( Base ` Y ) )
47 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
48 eqid 
 |-  ( Scalar ` Y ) = ( Scalar ` Y )
49 eqid 
 |-  ( Base ` ( Scalar ` Y ) ) = ( Base ` ( Scalar ` Y ) )
50 47 48 11 49 lmodvscl 
 |-  ( ( Y e. LMod /\ ( K .^ X ) e. ( Base ` ( Scalar ` Y ) ) /\ ( G ` K ) e. ( Base ` Y ) ) -> ( ( K .^ X ) .x. ( G ` K ) ) e. ( Base ` Y ) )
51 17 42 46 50 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( s e. NN /\ b e. ( B ^m ( 0 ... s ) ) ) /\ K e. NN0 ) -> ( ( K .^ X ) .x. ( G ` K ) ) e. ( Base ` Y ) )