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 = ( Poly1 ` R )
	rhmply1.q	\|- Q = ( Poly1 ` S )
	rhmply1.b	\|- B = ( Base ` P )
	rhmply1.f	\|- F = ( p e. B \|-> ( H o. p ) )
	rhmply1.h	\|- ( ph -> H e. ( R RingHom S ) )
Assertion	rhmply1	\|- ( ph -> F e. ( P RingHom Q ) )

Proof

Step	Hyp	Ref	Expression
1		rhmply1.p	\|- P = ( Poly1 ` R )
2		rhmply1.q	\|- Q = ( Poly1 ` S )
3		rhmply1.b	\|- B = ( Base ` P )
4		rhmply1.f	\|- F = ( p e. B \|-> ( H o. p ) )
5		rhmply1.h	\|- ( ph -> H e. ( R RingHom S ) )
6		eqid	\|- ( 1o mPoly R ) = ( 1o mPoly R )
7		eqid	\|- ( 1o mPoly S ) = ( 1o mPoly S )
8	1 3	ply1bas	\|- B = ( Base ` ( 1o mPoly R ) )
9		1oex	\|- 1o e. _V
10	9	a1i	\|- ( ph -> 1o e. _V )
11	6 7 8 4 10 5	rhmmpl	\|- ( ph -> F e. ( ( 1o mPoly R ) RingHom ( 1o mPoly S ) ) )
12	3	a1i	\|- ( ph -> B = ( Base ` P ) )
13		eqid	\|- ( Base ` Q ) = ( Base ` Q )
14	13	a1i	\|- ( ph -> ( Base ` Q ) = ( Base ` Q ) )
15	8	a1i	\|- ( ph -> B = ( Base ` ( 1o mPoly R ) ) )
16	2 13	ply1bas	\|- ( Base ` Q ) = ( Base ` ( 1o mPoly S ) )
17	16	a1i	\|- ( ph -> ( Base ` Q ) = ( Base ` ( 1o mPoly S ) ) )
18		eqid	\|- ( +g ` P ) = ( +g ` P )
19	1 6 18	ply1plusg	\|- ( +g ` P ) = ( +g ` ( 1o mPoly R ) )
20	19	oveqi	\|- ( x ( +g ` P ) y ) = ( x ( +g ` ( 1o mPoly R ) ) y )
21	20	a1i	\|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` P ) y ) = ( x ( +g ` ( 1o mPoly R ) ) y ) )
22		eqid	\|- ( +g ` Q ) = ( +g ` Q )
23	2 7 22	ply1plusg	\|- ( +g ` Q ) = ( +g ` ( 1o mPoly S ) )
24	23	oveqi	\|- ( x ( +g ` Q ) y ) = ( x ( +g ` ( 1o mPoly S ) ) y )
25	24	a1i	\|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( x ( +g ` Q ) y ) = ( x ( +g ` ( 1o mPoly S ) ) y ) )
26		eqid	\|- ( .r ` P ) = ( .r ` P )
27	1 6 26	ply1mulr	\|- ( .r ` P ) = ( .r ` ( 1o mPoly R ) )
28	27	oveqi	\|- ( x ( .r ` P ) y ) = ( x ( .r ` ( 1o mPoly R ) ) y )
29	28	a1i	\|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` P ) y ) = ( x ( .r ` ( 1o mPoly R ) ) y ) )
30		eqid	\|- ( .r ` Q ) = ( .r ` Q )
31	2 7 30	ply1mulr	\|- ( .r ` Q ) = ( .r ` ( 1o mPoly S ) )
32	31	oveqi	\|- ( x ( .r ` Q ) y ) = ( x ( .r ` ( 1o mPoly S ) ) y )
33	32	a1i	\|- ( ( ph /\ ( x e. ( Base ` Q ) /\ y e. ( Base ` Q ) ) ) -> ( x ( .r ` Q ) y ) = ( x ( .r ` ( 1o mPoly S ) ) y ) )
34	12 14 15 17 21 25 29 33	rhmpropd	\|- ( ph -> ( P RingHom Q ) = ( ( 1o mPoly R ) RingHom ( 1o mPoly S ) ) )
35	11 34	eleqtrrd	\|- ( ph -> F e. ( P RingHom Q ) )

Metamath Proof Explorer

Theorem rhmply1

Proof