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 𝐴 = ( 𝑁 Mat 𝑅 )
chfacfisf.b 𝐵 = ( Base ‘ 𝐴 )
chfacfisf.p 𝑃 = ( Poly1𝑅 )
chfacfisf.y 𝑌 = ( 𝑁 Mat 𝑃 )
chfacfisf.r × = ( .r𝑌 )
chfacfisf.s = ( -g𝑌 )
chfacfisf.0 0 = ( 0g𝑌 )
chfacfisf.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
chfacfisf.g 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ) ) ) )
chfacfscmulcl.x 𝑋 = ( var1𝑅 )
chfacfscmulcl.m · = ( ·𝑠𝑌 )
chfacfscmulcl.e = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
Assertion chfacfscmulcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 𝑋 ) · ( 𝐺𝐾 ) ) ∈ ( Base ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 chfacfisf.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 chfacfisf.b 𝐵 = ( Base ‘ 𝐴 )
3 chfacfisf.p 𝑃 = ( Poly1𝑅 )
4 chfacfisf.y 𝑌 = ( 𝑁 Mat 𝑃 )
5 chfacfisf.r × = ( .r𝑌 )
6 chfacfisf.s = ( -g𝑌 )
7 chfacfisf.0 0 = ( 0g𝑌 )
8 chfacfisf.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9 chfacfisf.g 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ) ) ) )
10 chfacfscmulcl.x 𝑋 = ( var1𝑅 )
11 chfacfscmulcl.m · = ( ·𝑠𝑌 )
12 chfacfscmulcl.e = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
13 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14 3 4 pmatlmod ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ LMod )
15 13 14 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑌 ∈ LMod )
16 15 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑌 ∈ LMod )
17 16 3ad2ant1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑌 ∈ LMod )
18 eqid ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
19 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
20 18 19 mgpbas ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
21 3 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
22 13 21 syl ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
23 22 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑃 ∈ Ring )
24 18 ringmgp ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
25 23 24 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
26 25 3ad2ant1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
27 simp3 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
28 13 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑅 ∈ Ring )
29 10 3 19 vr1cl ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
30 28 29 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
31 30 3ad2ant1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
32 20 12 26 27 31 mulgnn0cld ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
33 3 ply1crng ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
34 33 anim2i ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
35 34 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
36 4 matsca2 ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
37 35 36 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
38 37 eqcomd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
39 38 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
40 39 3ad2ant1 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
41 32 40 eleqtrrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
42 1 2 3 4 5 6 7 8 9 chfacfisf ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
43 13 42 syl3anl2 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
44 43 3adant3 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
45 44 27 ffvelcdmd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐺𝐾 ) ∈ ( Base ‘ 𝑌 ) )
46 eqid ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
47 eqid ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
48 eqid ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
49 46 47 11 48 lmodvscl ( ( 𝑌 ∈ LMod ∧ ( 𝐾 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝐺𝐾 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝐾 𝑋 ) · ( 𝐺𝐾 ) ) ∈ ( Base ‘ 𝑌 ) )
50 17 41 45 49 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 𝑋 ) · ( 𝐺𝐾 ) ) ∈ ( Base ‘ 𝑌 ) )