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	$⊢ P = I mPoly R$
	rhmmpl.q	$⊢ Q = I mPoly S$
	rhmmpl.b	$⊢ B = {Base}_{P}$
	rhmmpl.f	$⊢ F = (p \in B ⟼ H \circ p)$
	rhmmpl.i	$⊢ φ \to I \in V$
	rhmmpl.h	$⊢ φ \to H \in (R RingHom S)$
Assertion	rhmmpl	$⊢ φ \to F \in (P RingHom Q)$

Proof

Step	Hyp	Ref	Expression
1		rhmmpl.p	$⊢ P = I mPoly R$
2		rhmmpl.q	$⊢ Q = I mPoly S$
3		rhmmpl.b	$⊢ B = {Base}_{P}$
4		rhmmpl.f	$⊢ F = (p \in B ⟼ H \circ p)$
5		rhmmpl.i	$⊢ φ \to I \in V$
6		rhmmpl.h	$⊢ φ \to H \in (R RingHom S)$
7		eqid	$⊢ 1_{P} = 1_{P}$
8		eqid	$⊢ 1_{Q} = 1_{Q}$
9		eqid	$⊢ \cdot_{P} = \cdot_{P}$
10		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
11		rhmrcl1	$⊢ H \in (R RingHom S) \to R \in Ring$
12	6 11	syl	$⊢ φ \to R \in Ring$
13	1 5 12	mplringd	$⊢ φ \to P \in Ring$
14		rhmrcl2	$⊢ H \in (R RingHom S) \to S \in Ring$
15	6 14	syl	$⊢ φ \to S \in Ring$
16	2 5 15	mplringd	$⊢ φ \to Q \in Ring$
17		eqid	$⊢ \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
18		eqid	$⊢ 0_{R} = 0_{R}$
19		eqid	$⊢ 1_{R} = 1_{R}$
20	1 17 18 19 7 5 12	mpl1	$⊢ φ \to 1_{P} = (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (d = I \times \{0\}, 1_{R}, 0_{R}))$
21	20	coeq2d	$⊢ φ \to H \circ 1_{P} = H \circ (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (d = I \times \{0\}, 1_{R}, 0_{R}))$
22		eqid	$⊢ {Base}_{R} = {Base}_{R}$
23		eqid	$⊢ {Base}_{S} = {Base}_{S}$
24	22 23	rhmf	$⊢ H \in (R RingHom S) \to H : {Base}_{R} ⟶ {Base}_{S}$
25	6 24	syl	$⊢ φ \to H : {Base}_{R} ⟶ {Base}_{S}$
26	22 19	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
27	12 26	syl	$⊢ φ \to 1_{R} \in {Base}_{R}$
28	22 18	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
29	12 28	syl	$⊢ φ \to 0_{R} \in {Base}_{R}$
30	27 29	ifcld	$⊢ φ \to if (d = I \times \{0\}, 1_{R}, 0_{R}) \in {Base}_{R}$
31	30	adantr	$⊢ (φ \land d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}) \to if (d = I \times \{0\}, 1_{R}, 0_{R}) \in {Base}_{R}$
32	25 31	cofmpt	$⊢ φ \to H \circ (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (d = I \times \{0\}, 1_{R}, 0_{R})) = (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ H (if (d = I \times \{0\}, 1_{R}, 0_{R})))$
33		fvif	$⊢ H (if (d = I \times \{0\}, 1_{R}, 0_{R})) = if (d = I \times \{0\}, H (1_{R}), H (0_{R}))$
34		eqid	$⊢ 1_{S} = 1_{S}$
35	19 34	rhm1	$⊢ H \in (R RingHom S) \to H (1_{R}) = 1_{S}$
36	6 35	syl	$⊢ φ \to H (1_{R}) = 1_{S}$
37		rhmghm	$⊢ H \in (R RingHom S) \to H \in (R GrpHom S)$
38		eqid	$⊢ 0_{S} = 0_{S}$
39	18 38	ghmid	$⊢ H \in (R GrpHom S) \to H (0_{R}) = 0_{S}$
40	6 37 39	3syl	$⊢ φ \to H (0_{R}) = 0_{S}$
41	36 40	ifeq12d	$⊢ φ \to if (d = I \times \{0\}, H (1_{R}), H (0_{R})) = if (d = I \times \{0\}, 1_{S}, 0_{S})$
42	33 41	eqtrid	$⊢ φ \to H (if (d = I \times \{0\}, 1_{R}, 0_{R})) = if (d = I \times \{0\}, 1_{S}, 0_{S})$
43	42	mpteq2dv	$⊢ φ \to (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ H (if (d = I \times \{0\}, 1_{R}, 0_{R}))) = (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (d = I \times \{0\}, 1_{S}, 0_{S}))$
44	21 32 43	3eqtrd	$⊢ φ \to H \circ 1_{P} = (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (d = I \times \{0\}, 1_{S}, 0_{S}))$
45		coeq2	$⊢ p = 1_{P} \to H \circ p = H \circ 1_{P}$
46	3 7	ringidcl	$⊢ P \in Ring \to 1_{P} \in B$
47	13 46	syl	$⊢ φ \to 1_{P} \in B$
48	6 47	coexd	$⊢ φ \to H \circ 1_{P} \in V$
49	4 45 47 48	fvmptd3	$⊢ φ \to F (1_{P}) = H \circ 1_{P}$
50	2 17 38 34 8 5 15	mpl1	$⊢ φ \to 1_{Q} = (d \in \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\} ⟼ if (d = I \times \{0\}, 1_{S}, 0_{S}))$
51	44 49 50	3eqtr4d	$⊢ φ \to F (1_{P}) = 1_{Q}$
52		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
53	6	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to H \in (R RingHom S)$
54		simprl	$⊢ (φ \land (x \in B \land y \in B)) \to x \in B$
55		simprr	$⊢ (φ \land (x \in B \land y \in B)) \to y \in B$
56	1 2 3 52 9 10 53 54 55	rhmcomulmpl	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x \cdot_{P} y) = (H \circ x) \cdot_{Q} (H \circ y)$
57		coeq2	$⊢ p = x \cdot_{P} y \to H \circ p = H \circ (x \cdot_{P} y)$
58	13	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to P \in Ring$
59	3 9 58 54 55	ringcld	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{P} y \in B$
60		ovexd	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{P} y \in V$
61	53 60	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x \cdot_{P} y) \in V$
62	4 57 59 61	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \cdot_{P} y) = H \circ (x \cdot_{P} y)$
63		coeq2	$⊢ p = x \to H \circ p = H \circ x$
64	53 54	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ x \in V$
65	4 63 54 64	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) = H \circ x$
66		coeq2	$⊢ p = y \to H \circ p = H \circ y$
67	53 55	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ y \in V$
68	4 66 55 67	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (y) = H \circ y$
69	65 68	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) \cdot_{Q} F (y) = (H \circ x) \cdot_{Q} (H \circ y)$
70	56 62 69	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \cdot_{P} y) = F (x) \cdot_{Q} F (y)$
71		eqid	$⊢ +_{P} = +_{P}$
72		eqid	$⊢ +_{Q} = +_{Q}$
73		ghmmhm	$⊢ H \in (R GrpHom S) \to H \in (R MndHom S)$
74	6 37 73	3syl	$⊢ φ \to H \in (R MndHom S)$
75	74	adantr	$⊢ (φ \land p \in B) \to H \in (R MndHom S)$
76		simpr	$⊢ (φ \land p \in B) \to p \in B$
77	1 2 3 52 75 76	mhmcompl	$⊢ (φ \land p \in B) \to H \circ p \in {Base}_{Q}$
78	77 4	fmptd	$⊢ φ \to F : B ⟶ {Base}_{Q}$
79	53 37 73	3syl	$⊢ (φ \land (x \in B \land y \in B)) \to H \in (R MndHom S)$
80	1 2 3 52 71 72 79 54 55	mhmcoaddmpl	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x +_{P} y) = (H \circ x) +_{Q} (H \circ y)$
81		coeq2	$⊢ p = x +_{P} y \to H \circ p = H \circ (x +_{P} y)$
82	13	ringgrpd	$⊢ φ \to P \in Grp$
83	82	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to P \in Grp$
84	3 71 83 54 55	grpcld	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{P} y \in B$
85		ovexd	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{P} y \in V$
86	53 85	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x +_{P} y) \in V$
87	4 81 84 86	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x +_{P} y) = H \circ (x +_{P} y)$
88	65 68	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) +_{Q} F (y) = (H \circ x) +_{Q} (H \circ y)$
89	80 87 88	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x +_{P} y) = F (x) +_{Q} F (y)$
90	3 7 8 9 10 13 16 51 70 52 71 72 78 89	isrhmd	$⊢ φ \to F \in (P RingHom Q)$

Metamath Proof Explorer

Theorem rhmmpl

Proof