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 ‘ 𝑌 ) )