Metamath Proof Explorer


Theorem rhmply1vsca

Description: Apply a ring homomorphism between two univariate polynomial algebras to a scaled polynomial. (Contributed by SN, 20-May-2025)

Ref Expression
Hypotheses rhmply1vsca.p 𝑃 = ( Poly1𝑅 )
rhmply1vsca.q 𝑄 = ( Poly1𝑆 )
rhmply1vsca.b 𝐵 = ( Base ‘ 𝑃 )
rhmply1vsca.k 𝐾 = ( Base ‘ 𝑅 )
rhmply1vsca.f 𝐹 = ( 𝑝𝐵 ↦ ( 𝐻𝑝 ) )
rhmply1vsca.t · = ( ·𝑠𝑃 )
rhmply1vsca.u = ( ·𝑠𝑄 )
rhmply1vsca.h ( 𝜑𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
rhmply1vsca.c ( 𝜑𝐶𝐾 )
rhmply1vsca.x ( 𝜑𝑋𝐵 )
Assertion rhmply1vsca ( 𝜑 → ( 𝐹 ‘ ( 𝐶 · 𝑋 ) ) = ( ( 𝐻𝐶 ) ( 𝐹𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 rhmply1vsca.p 𝑃 = ( Poly1𝑅 )
2 rhmply1vsca.q 𝑄 = ( Poly1𝑆 )
3 rhmply1vsca.b 𝐵 = ( Base ‘ 𝑃 )
4 rhmply1vsca.k 𝐾 = ( Base ‘ 𝑅 )
5 rhmply1vsca.f 𝐹 = ( 𝑝𝐵 ↦ ( 𝐻𝑝 ) )
6 rhmply1vsca.t · = ( ·𝑠𝑃 )
7 rhmply1vsca.u = ( ·𝑠𝑄 )
8 rhmply1vsca.h ( 𝜑𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
9 rhmply1vsca.c ( 𝜑𝐶𝐾 )
10 rhmply1vsca.x ( 𝜑𝑋𝐵 )
11 fconst6g ( 𝐶𝐾 → ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } ⟶ 𝐾 )
12 9 11 syl ( 𝜑 → ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } ⟶ 𝐾 )
13 psr1baslem ( ℕ0m 1o ) = { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin }
14 13 feq2i ( ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) : ( ℕ0m 1o ) ⟶ 𝐾 ↔ ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } ⟶ 𝐾 )
15 12 14 sylibr ( 𝜑 → ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) : ( ℕ0m 1o ) ⟶ 𝐾 )
16 1 3 4 ply1basf ( 𝑋𝐵𝑋 : ( ℕ0m 1o ) ⟶ 𝐾 )
17 10 16 syl ( 𝜑𝑋 : ( ℕ0m 1o ) ⟶ 𝐾 )
18 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
19 4 18 rhmf ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : 𝐾 ⟶ ( Base ‘ 𝑆 ) )
20 8 19 syl ( 𝜑𝐻 : 𝐾 ⟶ ( Base ‘ 𝑆 ) )
21 20 ffnd ( 𝜑𝐻 Fn 𝐾 )
22 ovexd ( 𝜑 → ( ℕ0m 1o ) ∈ V )
23 rhmrcl1 ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
24 8 23 syl ( 𝜑𝑅 ∈ Ring )
25 eqid ( .r𝑅 ) = ( .r𝑅 )
26 4 25 ringcl ( ( 𝑅 ∈ Ring ∧ 𝑎𝐾𝑏𝐾 ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) ∈ 𝐾 )
27 24 26 syl3an1 ( ( 𝜑𝑎𝐾𝑏𝐾 ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) ∈ 𝐾 )
28 27 3expb ( ( 𝜑 ∧ ( 𝑎𝐾𝑏𝐾 ) ) → ( 𝑎 ( .r𝑅 ) 𝑏 ) ∈ 𝐾 )
29 eqid ( .r𝑆 ) = ( .r𝑆 )
30 4 25 29 rhmmul ( ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝑎𝐾𝑏𝐾 ) → ( 𝐻 ‘ ( 𝑎 ( .r𝑅 ) 𝑏 ) ) = ( ( 𝐻𝑎 ) ( .r𝑆 ) ( 𝐻𝑏 ) ) )
31 8 30 syl3an1 ( ( 𝜑𝑎𝐾𝑏𝐾 ) → ( 𝐻 ‘ ( 𝑎 ( .r𝑅 ) 𝑏 ) ) = ( ( 𝐻𝑎 ) ( .r𝑆 ) ( 𝐻𝑏 ) ) )
32 31 3expb ( ( 𝜑 ∧ ( 𝑎𝐾𝑏𝐾 ) ) → ( 𝐻 ‘ ( 𝑎 ( .r𝑅 ) 𝑏 ) ) = ( ( 𝐻𝑎 ) ( .r𝑆 ) ( 𝐻𝑏 ) ) )
33 15 17 21 22 28 32 coof ( 𝜑 → ( 𝐻 ∘ ( ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r𝑅 ) 𝑋 ) ) = ( ( 𝐻 ∘ ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) ) ∘f ( .r𝑆 ) ( 𝐻𝑋 ) ) )
34 fcoconst ( ( 𝐻 Fn 𝐾𝐶𝐾 ) → ( 𝐻 ∘ ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) ) = ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { ( 𝐻𝐶 ) } ) )
35 21 9 34 syl2anc ( 𝜑 → ( 𝐻 ∘ ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) ) = ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { ( 𝐻𝐶 ) } ) )
36 35 oveq1d ( 𝜑 → ( ( 𝐻 ∘ ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) ) ∘f ( .r𝑆 ) ( 𝐻𝑋 ) ) = ( ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { ( 𝐻𝐶 ) } ) ∘f ( .r𝑆 ) ( 𝐻𝑋 ) ) )
37 33 36 eqtrd ( 𝜑 → ( 𝐻 ∘ ( ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r𝑅 ) 𝑋 ) ) = ( ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { ( 𝐻𝐶 ) } ) ∘f ( .r𝑆 ) ( 𝐻𝑋 ) ) )
38 eqid ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
39 eqid ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
40 1 3 ply1bas 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
41 eqid { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } = { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin }
42 38 39 4 40 25 41 9 10 mplvsca ( 𝜑 → ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) = ( ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r𝑅 ) 𝑋 ) )
43 42 coeq2d ( 𝜑 → ( 𝐻 ∘ ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) ) = ( 𝐻 ∘ ( ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r𝑅 ) 𝑋 ) ) )
44 eqid ( 1o mPoly 𝑆 ) = ( 1o mPoly 𝑆 )
45 eqid ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) ) = ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) )
46 eqid ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
47 2 46 ply1bas ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPoly 𝑆 ) )
48 20 9 ffvelcdmd ( 𝜑 → ( 𝐻𝐶 ) ∈ ( Base ‘ 𝑆 ) )
49 rhmghm ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
50 ghmmhm ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
51 8 49 50 3syl ( 𝜑𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
52 1 2 3 46 51 10 mhmcoply1 ( 𝜑 → ( 𝐻𝑋 ) ∈ ( Base ‘ 𝑄 ) )
53 44 45 18 47 29 41 48 52 mplvsca ( 𝜑 → ( ( 𝐻𝐶 ) ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) ) ( 𝐻𝑋 ) ) = ( ( { ∈ ( ℕ0m 1o ) ∣ ( “ ℕ ) ∈ Fin } × { ( 𝐻𝐶 ) } ) ∘f ( .r𝑆 ) ( 𝐻𝑋 ) ) )
54 37 43 53 3eqtr4d ( 𝜑 → ( 𝐻 ∘ ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) ) = ( ( 𝐻𝐶 ) ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) ) ( 𝐻𝑋 ) ) )
55 1 38 6 ply1vsca · = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
56 55 oveqi ( 𝐶 · 𝑋 ) = ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 )
57 56 coeq2i ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) = ( 𝐻 ∘ ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) )
58 2 44 7 ply1vsca = ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) )
59 58 oveqi ( ( 𝐻𝐶 ) ( 𝐻𝑋 ) ) = ( ( 𝐻𝐶 ) ( ·𝑠 ‘ ( 1o mPoly 𝑆 ) ) ( 𝐻𝑋 ) )
60 54 57 59 3eqtr4g ( 𝜑 → ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) = ( ( 𝐻𝐶 ) ( 𝐻𝑋 ) ) )
61 coeq2 ( 𝑝 = ( 𝐶 · 𝑋 ) → ( 𝐻𝑝 ) = ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) )
62 1 3 4 6 24 9 10 ply1vscl ( 𝜑 → ( 𝐶 · 𝑋 ) ∈ 𝐵 )
63 8 62 coexd ( 𝜑 → ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) ∈ V )
64 5 61 62 63 fvmptd3 ( 𝜑 → ( 𝐹 ‘ ( 𝐶 · 𝑋 ) ) = ( 𝐻 ∘ ( 𝐶 · 𝑋 ) ) )
65 coeq2 ( 𝑝 = 𝑋 → ( 𝐻𝑝 ) = ( 𝐻𝑋 ) )
66 8 10 coexd ( 𝜑 → ( 𝐻𝑋 ) ∈ V )
67 5 65 10 66 fvmptd3 ( 𝜑 → ( 𝐹𝑋 ) = ( 𝐻𝑋 ) )
68 67 oveq2d ( 𝜑 → ( ( 𝐻𝐶 ) ( 𝐹𝑋 ) ) = ( ( 𝐻𝐶 ) ( 𝐻𝑋 ) ) )
69 60 64 68 3eqtr4d ( 𝜑 → ( 𝐹 ‘ ( 𝐶 · 𝑋 ) ) = ( ( 𝐻𝐶 ) ( 𝐹𝑋 ) ) )