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

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 ⊢ ( 𝐶 ∈ 𝐾 → ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
12 9 11 syl ⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
13 psr1baslem ⊢ ( ℕ0 ↑m 1o ) = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
14 13 feq2i ⊢ ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : ( ℕ0 ↑m 1o ) ⟶ 𝐾 ↔ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } ⟶ 𝐾 )
15 12 14 sylibr ⊢ ( 𝜑 → ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )
16 1 3 4 ply1basf ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )
17 10 16 syl ⊢ ( 𝜑 → 𝑋 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 )
18 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
19 4 18 rhmf ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : 𝐾 ⟶ ( Base ‘ 𝑆 ) )
20 8 19 syl ⊢ ( 𝜑 → 𝐻 : 𝐾 ⟶ ( Base ‘ 𝑆 ) )
21 20 ffnd ⊢ ( 𝜑 → 𝐻 Fn 𝐾 )
22 ovexd ⊢ ( 𝜑 → ( ℕ0 ↑m 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 ⊢ ( 𝜑 → ( 𝐻 ∘ ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r ‘ 𝑅 ) 𝑋 ) ) = ( ( 𝐻 ∘ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ) ∘f ( .r ‘ 𝑆 ) ( 𝐻 ∘ 𝑋 ) ) )
34 fcoconst ⊢ ( ( 𝐻 Fn 𝐾 ∧ 𝐶 ∈ 𝐾 ) → ( 𝐻 ∘ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ) = ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 𝐻 ‘ 𝐶 ) } ) )
35 21 9 34 syl2anc ⊢ ( 𝜑 → ( 𝐻 ∘ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ) = ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 𝐻 ‘ 𝐶 ) } ) )
36 35 oveq1d ⊢ ( 𝜑 → ( ( 𝐻 ∘ ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ) ∘f ( .r ‘ 𝑆 ) ( 𝐻 ∘ 𝑋 ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { ( 𝐻 ‘ 𝐶 ) } ) ∘f ( .r ‘ 𝑆 ) ( 𝐻 ∘ 𝑋 ) ) )
37 33 36 eqtrd ⊢ ( 𝜑 → ( 𝐻 ∘ ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r ‘ 𝑅 ) 𝑋 ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 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 ⊢ { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
42 38 39 4 40 25 41 9 10 mplvsca ⊢ ( 𝜑 → ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) = ( ( { ℎ ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } × { 𝐶 } ) ∘f ( .r ‘ 𝑅 ) 𝑋 ) )
43 42 coeq2d ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐶 ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) ) 𝑋 ) ) = ( 𝐻 ∘ ( ( { ℎ ∈ ( ℕ0 ↑m 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 𝑆 ) ) ( 𝐻 ∘ 𝑋 ) ) = ( ( { ℎ ∈ ( ℕ0 ↑m 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 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐶 · 𝑋 ) ) = ( ( 𝐻 ‘ 𝐶 ) ∙ ( 𝐹 ‘ 𝑋 ) ) )