This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 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 ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )