Theorem rhmmpl

Description: Provide a ring homomorphism between two polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. Compare pwsco2rhm . (Contributed by SN, 8-Feb-2025)

	Ref	Expression
Hypotheses	rhmmpl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	rhmmpl.q	⊢ 𝑄 = ( 𝐼 mPoly 𝑆 )
	rhmmpl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	rhmmpl.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
	rhmmpl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	rhmmpl.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion	rhmmpl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmmpl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		rhmmpl.q	⊢ 𝑄 = ( 𝐼 mPoly 𝑆 )
3		rhmmpl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		rhmmpl.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
5		rhmmpl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		rhmmpl.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
7		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
8		eqid	⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
9		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
10		eqid	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
11		rhmrcl1	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
12	6 11	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
13	1 5 12	mplringd	⊢ ( 𝜑 → 𝑃 ∈ Ring )
14		rhmrcl2	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
15	6 14	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
16	2 5 15	mplringd	⊢ ( 𝜑 → 𝑄 ∈ Ring )
17		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
18		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20	1 17 18 19 7 5 12	mpl1	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
21	20	coeq2d	⊢ ( 𝜑 → ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) = ( 𝐻 ∘ ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
22		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
24	22 23	rhmf	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
25	6 24	syl	⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
26	22 19	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27	12 26	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
28	22 18	ring0cl	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
29	12 28	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
30	27 29	ifcld	⊢ ( 𝜑 → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
32	25 31	cofmpt	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
33		fvif	⊢ ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 𝐻 ‘ ( 1r ‘ 𝑅 ) ) , ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) )
34		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
35	19 34	rhm1	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐻 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
36	6 35	syl	⊢ ( 𝜑 → ( 𝐻 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
37		rhmghm	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
38		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
39	18 38	ghmid	⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
40	6 37 39	3syl	⊢ ( 𝜑 → ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
41	36 40	ifeq12d	⊢ ( 𝜑 → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 𝐻 ‘ ( 1r ‘ 𝑅 ) ) , ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) )
42	33 41	eqtrid	⊢ ( 𝜑 → ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) )
43	42	mpteq2dv	⊢ ( 𝜑 → ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) ) )
44	21 32 43	3eqtrd	⊢ ( 𝜑 → ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) ) )
45		coeq2	⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) )
46	3 7	ringidcl	⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
47	13 46	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
48	6 47	coexd	⊢ ( 𝜑 → ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) ∈ V )
49	4 45 47 48	fvmptd3	⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) )
50	2 17 38 34 8 5 15	mpl1	⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) ) )
51	44 49 50	3eqtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑄 ) )
52		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
53	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
54		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
55		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
56	1 2 3 52 9 10 53 54 55	rhmcomulmpl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
57		coeq2	⊢ ( 𝑝 = ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
58	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
59	3 9 58 54 55	ringcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
60		ovexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ V )
61	53 60	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) ∈ V )
62	4 57 59 61	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
63		coeq2	⊢ ( 𝑝 = 𝑥 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑥 ) )
64	53 54	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ 𝑥 ) ∈ V )
65	4 63 54 64	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ∘ 𝑥 ) )
66		coeq2	⊢ ( 𝑝 = 𝑦 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑦 ) )
67	53 55	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ 𝑦 ) ∈ V )
68	4 66 55 67	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ∘ 𝑦 ) )
69	65 68	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
70	56 62 69	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) )
71		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
72		eqid	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
73		ghmmhm	⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
74	6 37 73	3syl	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
75	74	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
76		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
77	1 2 3 52 75 76	mhmcompl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝐻 ∘ 𝑝 ) ∈ ( Base ‘ 𝑄 ) )
78	77 4	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )
79	53 37 73	3syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
80	1 2 3 52 71 72 79 54 55	mhmcoaddmpl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
81		coeq2	⊢ ( 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) )
82	13	ringgrpd	⊢ ( 𝜑 → 𝑃 ∈ Grp )
83	82	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Grp )
84	3 71 83 54 55	grpcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
85		ovexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ V )
86	53 85	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) ∈ V )
87	4 81 84 86	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) )
88	65 68	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
89	80 87 88	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) )
90	3 7 8 9 10 13 16 51 70 52 71 72 78 89	isrhmd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )