rhmpsr

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

	Ref	Expression
Hypotheses	rhmpsr.p	$⊢ P = I mPwSer R$
	rhmpsr.q	$⊢ Q = I mPwSer S$
	rhmpsr.b	$⊢ B = {Base}_{P}$
	rhmpsr.f	$⊢ F = (p \in B ⟼ H \circ p)$
	rhmpsr.i	$⊢ φ \to I \in V$
	rhmpsr.h	$⊢ φ \to H \in (R RingHom S)$
Assertion	rhmpsr	$⊢ φ \to F \in (P RingHom Q)$

Proof

Step	Hyp	Ref	Expression
1		rhmpsr.p	$⊢ P = I mPwSer R$
2		rhmpsr.q	$⊢ Q = I mPwSer S$
3		rhmpsr.b	$⊢ B = {Base}_{P}$
4		rhmpsr.f	$⊢ F = (p \in B ⟼ H \circ p)$
5		rhmpsr.i	$⊢ φ \to I \in V$
6		rhmpsr.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	psrring	$⊢ φ \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	psrring	$⊢ φ \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 5 12 17 18 19 7	psr1	$⊢ φ \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 5 15 17 38 34 8	psr1	$⊢ φ \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	rhmcomulpsr	$⊢ (φ \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	53 59	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x \cdot_{P} y) \in V$
61	4 57 59 60	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \cdot_{P} y) = H \circ (x \cdot_{P} y)$
62		coeq2	$⊢ p = x \to H \circ p = H \circ x$
63	53 54	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ x \in V$
64	4 62 54 63	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) = H \circ x$
65		coeq2	$⊢ p = y \to H \circ p = H \circ y$
66	53 55	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ y \in V$
67	4 65 55 66	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (y) = H \circ y$
68	64 67	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) \cdot_{Q} F (y) = (H \circ x) \cdot_{Q} (H \circ y)$
69	56 61 68	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x \cdot_{P} y) = F (x) \cdot_{Q} F (y)$
70		eqid	$⊢ +_{P} = +_{P}$
71		eqid	$⊢ +_{Q} = +_{Q}$
72		ghmmhm	$⊢ H \in (R GrpHom S) \to H \in (R MndHom S)$
73	6 37 72	3syl	$⊢ φ \to H \in (R MndHom S)$
74	73	adantr	$⊢ (φ \land p \in B) \to H \in (R MndHom S)$
75		simpr	$⊢ (φ \land p \in B) \to p \in B$
76	1 2 3 52 74 75	mhmcopsr	$⊢ (φ \land p \in B) \to H \circ p \in {Base}_{Q}$
77	76 4	fmptd	$⊢ φ \to F : B ⟶ {Base}_{Q}$
78	53 37 72	3syl	$⊢ (φ \land (x \in B \land y \in B)) \to H \in (R MndHom S)$
79	1 2 3 52 70 71 78 54 55	mhmcoaddpsr	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x +_{P} y) = (H \circ x) +_{Q} (H \circ y)$
80		coeq2	$⊢ p = x +_{P} y \to H \circ p = H \circ (x +_{P} y)$
81	58	ringgrpd	$⊢ (φ \land (x \in B \land y \in B)) \to P \in Grp$
82	3 70 81 54 55	grpcld	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{P} y \in B$
83	53 82	coexd	$⊢ (φ \land (x \in B \land y \in B)) \to H \circ (x +_{P} y) \in V$
84	4 80 82 83	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to F (x +_{P} y) = H \circ (x +_{P} y)$
85	64 67	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x) +_{Q} F (y) = (H \circ x) +_{Q} (H \circ y)$
86	79 84 85	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to F (x +_{P} y) = F (x) +_{Q} F (y)$
87	3 7 8 9 10 13 16 51 69 52 70 71 77 86	isrhmd	$⊢ φ \to F \in (P RingHom Q)$

Metamath Proof Explorer

Theorem rhmpsr

Proof