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

Metamath Proof Explorer

Theorem rhmply1

Description: Provide a ring homomorphism between two univariate polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 20-May-2025)

Ref Expression
Hypotheses rhmply1.p ⊢ P = Poly 1 ⁡ R
rhmply1.q ⊢ Q = Poly 1 ⁡ S
rhmply1.b ⊢ B = Base P
rhmply1.f ⊢ F = p ∈ B ⟼ H ∘ p
rhmply1.h ⊢ φ → H ∈ R RingHom S
Assertion rhmply1 ⊢ φ → F ∈ P RingHom Q

Proof

Step Hyp Ref Expression
1 rhmply1.p ⊢ P = Poly 1 ⁡ R
2 rhmply1.q ⊢ Q = Poly 1 ⁡ S
3 rhmply1.b ⊢ B = Base P
4 rhmply1.f ⊢ F = p ∈ B ⟼ H ∘ p
5 rhmply1.h ⊢ φ → H ∈ R RingHom S
6 eqid ⊢ 1 𝑜 mPoly R = 1 𝑜 mPoly R
7 eqid ⊢ 1 𝑜 mPoly S = 1 𝑜 mPoly S
8 1 3 ply1bas ⊢ B = Base 1 𝑜 mPoly R
9 1oex ⊢ 1 𝑜 ∈ V
10 9 a1i ⊢ φ → 1 𝑜 ∈ V
11 6 7 8 4 10 5 rhmmpl ⊢ φ → F ∈ 1 𝑜 mPoly R RingHom 1 𝑜 mPoly S
12 3 a1i ⊢ φ → B = Base P
13 eqid ⊢ Base Q = Base Q
14 13 a1i ⊢ φ → Base Q = Base Q
15 8 a1i ⊢ φ → B = Base 1 𝑜 mPoly R
16 2 13 ply1bas ⊢ Base Q = Base 1 𝑜 mPoly S
17 16 a1i ⊢ φ → Base Q = Base 1 𝑜 mPoly S
18 eqid ⊢ + P = + P
19 1 6 18 ply1plusg ⊢ + P = + 1 𝑜 mPoly R
20 19 oveqi ⊢ x + P y = x + 1 𝑜 mPoly R y
21 20 a1i ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + P y = x + 1 𝑜 mPoly R y
22 eqid ⊢ + Q = + Q
23 2 7 22 ply1plusg ⊢ + Q = + 1 𝑜 mPoly S
24 23 oveqi ⊢ x + Q y = x + 1 𝑜 mPoly S y
25 24 a1i ⊢ φ ∧ x ∈ Base Q ∧ y ∈ Base Q → x + Q y = x + 1 𝑜 mPoly S y
26 eqid ⊢ ⋅ P = ⋅ P
27 1 6 26 ply1mulr ⊢ ⋅ P = ⋅ 1 𝑜 mPoly R
28 27 oveqi ⊢ x ⋅ P y = x ⋅ 1 𝑜 mPoly R y
29 28 a1i ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ⋅ P y = x ⋅ 1 𝑜 mPoly R y
30 eqid ⊢ ⋅ Q = ⋅ Q
31 2 7 30 ply1mulr ⊢ ⋅ Q = ⋅ 1 𝑜 mPoly S
32 31 oveqi ⊢ x ⋅ Q y = x ⋅ 1 𝑜 mPoly S y
33 32 a1i ⊢ φ ∧ x ∈ Base Q ∧ y ∈ Base Q → x ⋅ Q y = x ⋅ 1 𝑜 mPoly S y
34 12 14 15 17 21 25 29 33 rhmpropd ⊢ φ → P RingHom Q = 1 𝑜 mPoly R RingHom 1 𝑜 mPoly S
35 11 34 eleqtrrd ⊢ φ → F ∈ P RingHom Q