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 3 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
19 13 18 syl ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
20 19 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 ∈ Ring )
21 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
22 21 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
23 20 22 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
24 23 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
25 simp3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
26 13 3ad2ant2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
27 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
28 10 3 27 vr1cl ⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
29 26 28 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
30 29 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝑋 ∈ ( Base ‘ 𝑃 ) )
31 21 27 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
32 31 12 mulgnn0cl ⊢ ( ( ( mulGrp ‘ 𝑃 ) ∈ Mnd ∧ 𝐾 ∈ ℕ0 ∧ 𝑋 ∈ ( Base ‘ 𝑃 ) ) → ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
33 24 25 30 32 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
34 3 ply1crng ⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )
35 34 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
36 35 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) )
37 4 matsca2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ CRing ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
38 36 37 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑃 = ( Scalar ‘ 𝑌 ) )
39 38 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝑌 ) = 𝑃 )
40 39 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
41 40 3ad2ant1 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ 𝑃 ) )
42 33 41 eleqtrrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) )
43 1 2 3 4 5 6 7 8 9 chfacfisf ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
44 13 43 syl3anl2 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
45 44 3adant3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → 𝐺 : ℕ0 ⟶ ( Base ‘ 𝑌 ) )
46 45 25 ffvelrnd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑌 ) )
47 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
48 eqid ⊢ ( Scalar ‘ 𝑌 ) = ( Scalar ‘ 𝑌 )
49 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑌 ) ) = ( Base ‘ ( Scalar ‘ 𝑌 ) )
50 47 48 11 49 lmodvscl ⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐾 ↑ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ 𝑌 ) ) ∧ ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑌 ) ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) ∈ ( Base ‘ 𝑌 ) )
51 17 42 46 50 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ∧ 𝐾 ∈ ℕ0 ) → ( ( 𝐾 ↑ 𝑋 ) · ( 𝐺 ‘ 𝐾 ) ) ∈ ( Base ‘ 𝑌 ) )