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	$⊢ 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	5	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to I \in V$
54	6	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to H \in (R RingHom S)$
55		simprl	$⊢ (φ \land (x \in B \land y \in B)) \to x \in B$
56		simprr	$⊢ (φ \land (x \in B \land y \in B)) \to y \in B$
57	1 2 3 52 9 10 53 54 55 56	rhmcomulmpl	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x \cdot_{P} y) = (H \circ x) \cdot_{Q} (H \circ y)$
58		coeq2	$⊢ p = x \cdot_{P} y \to H \circ p = H \circ (x \cdot_{P} y)$
59	13	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to P \in Ring$
60	3 9 59 55 56	ringcld	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{P} y \in B$
61		ovexd	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{P} y \in V$
62	54 61	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x \cdot_{P} y) \in V$
63	4 58 60 62	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \cdot_{P} y) = H \circ (x \cdot_{P} y)$
64		coeq2	$⊢ p = x \to H \circ p = H \circ x$
65	54 55	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ x \in V$
66	4 64 55 65	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) = H \circ x$
67		coeq2	$⊢ p = y \to H \circ p = H \circ y$
68	54 56	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ y \in V$
69	4 67 56 68	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (y) = H \circ y$
70	66 69	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) \cdot_{Q} F (y) = (H \circ x) \cdot_{Q} (H \circ y)$
71	57 63 70	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \cdot_{P} y) = F (x) \cdot_{Q} F (y)$
72		eqid	$⊢ +_{P} = +_{P}$
73		eqid	$⊢ +_{Q} = +_{Q}$
74	5	adantr	$⊢ (φ \land p \in B) \to I \in V$
75		ghmmhm	$⊢ H \in (R GrpHom S) \to H \in (R MndHom S)$
76	6 37 75	3syl	$⊢ φ \to H \in (R MndHom S)$
77	76	adantr	$⊢ (φ \land p \in B) \to H \in (R MndHom S)$
78		simpr	$⊢ (φ \land p \in B) \to p \in B$
79	1 2 3 52 74 77 78	mhmcompl	$⊢ (φ \land p \in B) \to H \circ p \in {Base}_{Q}$
80	79 4	fmptd	$⊢ φ \to F : B ⟶ {Base}_{Q}$
81	76	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to H \in (R MndHom S)$
82	1 2 3 52 72 73 53 81 55 56	mhmcoaddmpl	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x +_{P} y) = (H \circ x) +_{Q} (H \circ y)$
83		coeq2	$⊢ p = x +_{P} y \to H \circ p = H \circ (x +_{P} y)$
84	13	ringgrpd	$⊢ φ \to P \in Grp$
85	84	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to P \in Grp$
86	3 72 85 55 56	grpcld	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{P} y \in B$
87		ovexd	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{P} y \in V$
88	54 87	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x +_{P} y) \in V$
89	4 83 86 88	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x +_{P} y) = H \circ (x +_{P} y)$
90	66 69	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) +_{Q} F (y) = (H \circ x) +_{Q} (H \circ y)$
91	82 89 90	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x +_{P} y) = F (x) +_{Q} F (y)$
92	3 7 8 9 10 13 16 51 71 52 72 73 80 91	isrhmd	$⊢ φ \to F \in (P RingHom Q)$

Metamath Proof Explorer

Theorem rhmmpl

Proof