Theorem mhmcompl

Description: The composition of a monoid homomorphism and a polynomial is a polynomial. (Contributed by SN, 7-Feb-2025)

	Ref	Expression
Hypotheses	mhmcompl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mhmcompl.q	⊢ 𝑄 = ( 𝐼 mPoly 𝑆 )
	mhmcompl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mhmcompl.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
	mhmcompl.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
	mhmcompl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	mhmcompl	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mhmcompl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mhmcompl.q	⊢ 𝑄 = ( 𝐼 mPoly 𝑆 )
3		mhmcompl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		mhmcompl.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
5		mhmcompl.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
6		mhmcompl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) ∈ V )
8		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
9		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 𝐼 ) ∈ V )
10	8 9	rabexd	⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13	11 12	mhmf	⊢ ( 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
14	5 13	syl	⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
15	1 11 3 8 6	mplelf	⊢ ( 𝜑 → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
16	14 15	fcod	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑆 ) )
17	7 10 16	elmapdd	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( ( Base ‘ 𝑆 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
18		eqid	⊢ ( 𝐼 mPwSer 𝑆 ) = ( 𝐼 mPwSer 𝑆 )
19		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) )
20	1 3	mplrcl	⊢ ( 𝐹 ∈ 𝐵 → 𝐼 ∈ V )
21	6 20	syl	⊢ ( 𝜑 → 𝐼 ∈ V )
22	18 12 8 19 21	psrbas	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( ( Base ‘ 𝑆 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
23	17 22	eleqtrrd	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
24		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ V )
25		mhmrcl1	⊢ ( 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) → 𝑅 ∈ Mnd )
26	5 25	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
27		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
28	11 27	mndidcl	⊢ ( 𝑅 ∈ Mnd → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
29	26 28	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
30		ssidd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
31		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
32	1 3 27 6 26	mplelsfi	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
33		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
34	27 33	mhm0	⊢ ( 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) → ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
35	5 34	syl	⊢ ( 𝜑 → ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
36	24 29 15 14 30 10 31 32 35	fsuppcor	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) finSupp ( 0g ‘ 𝑆 ) )
37	2 18 19 33 4	mplelbas	⊢ ( ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 ↔ ( ( 𝐻 ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ∧ ( 𝐻 ∘ 𝐹 ) finSupp ( 0g ‘ 𝑆 ) ) )
38	23 36 37	sylanbrc	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )