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 . TODO: Currently mhmvlin would have to be moved up. Investigate the usefulness of surrounding theorems like mndvcl and the difference between mhmvlin , ofco , and ofco2 . (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	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑉 )
54	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
55		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
56		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
57	1 2 3 52 9 10 53 54 55 56	rhmcomulmpl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
58		coeq2	⊢ ( 𝑝 = ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
59	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
60	3 9 59 55 56	ringcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
61		ovexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ V )
62	54 61	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) ∈ V )
63	4 58 60 62	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
64		coeq2	⊢ ( 𝑝 = 𝑥 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑥 ) )
65	54 55	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ 𝑥 ) ∈ V )
66	4 64 55 65	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ∘ 𝑥 ) )
67		coeq2	⊢ ( 𝑝 = 𝑦 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑦 ) )
68	54 56	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ 𝑦 ) ∈ V )
69	4 67 56 68	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ∘ 𝑦 ) )
70	66 69	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
71	57 63 70	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) )
72		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
73		eqid	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
74	5	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐼 ∈ 𝑉 )
75		ghmmhm	⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
76	6 37 75	3syl	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
77	76	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
78		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
79	1 2 3 52 74 77 78	mhmcompl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝐻 ∘ 𝑝 ) ∈ ( Base ‘ 𝑄 ) )
80	79 4	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )
81	76	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
82	1 2 3 52 72 73 53 81 55 56	mhmcoaddmpl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
83		coeq2	⊢ ( 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) )
84	13	ringgrpd	⊢ ( 𝜑 → 𝑃 ∈ Grp )
85	84	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Grp )
86	3 72 85 55 56	grpcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
87		ovexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ V )
88	54 87	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) ∈ V )
89	4 83 86 88	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) )
90	66 69	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
91	82 89 90	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) )
92	3 7 8 9 10 13 16 51 71 52 72 73 80 91	isrhmd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )