Theorem rhmpsr1

Description: Provide a ring homomorphism between two univariate 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	rhmpsr1.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
	rhmpsr1.q	⊢ 𝑄 = ( PwSer1 ‘ 𝑆 )
	rhmpsr1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	rhmpsr1.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
	rhmpsr1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion	rhmpsr1	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmpsr1.p	⊢ 𝑃 = ( PwSer1 ‘ 𝑅 )
2		rhmpsr1.q	⊢ 𝑄 = ( PwSer1 ‘ 𝑆 )
3		rhmpsr1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		rhmpsr1.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
5		rhmpsr1.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
6		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
7		eqid	⊢ ( 1o mPwSer 𝑆 ) = ( 1o mPwSer 𝑆 )
8	1 3 6	psr1bas2	⊢ 𝐵 = ( Base ‘ ( 1o mPwSer 𝑅 ) )
9		1oex	⊢ 1o ∈ V
10	9	a1i	⊢ ( 𝜑 → 1o ∈ V )
11	6 7 8 4 10 5	rhmpsr	⊢ ( 𝜑 → 𝐹 ∈ ( ( 1o mPwSer 𝑅 ) RingHom ( 1o mPwSer 𝑆 ) ) )
12		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
13	1 12 6	psr1bas2	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPwSer 𝑅 ) )
14	13	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
15		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
16	2 15 7	psr1bas2	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPwSer 𝑆 ) )
17	16	a1i	⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ ( 1o mPwSer 𝑆 ) ) )
18		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) )
19		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 ) )
20		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
21	1 6 20	psr1plusg	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ ( 1o mPwSer 𝑅 ) )
22	21	eqcomi	⊢ ( +g ‘ ( 1o mPwSer 𝑅 ) ) = ( +g ‘ 𝑃 )
23	22	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( +g ‘ ( 1o mPwSer 𝑅 ) ) = ( +g ‘ 𝑃 ) )
24	23	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( +g ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) )
25		eqid	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
26	2 7 25	psr1plusg	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ ( 1o mPwSer 𝑆 ) )
27	26	eqcomi	⊢ ( +g ‘ ( 1o mPwSer 𝑆 ) ) = ( +g ‘ 𝑄 )
28	27	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( +g ‘ ( 1o mPwSer 𝑆 ) ) = ( +g ‘ 𝑄 ) )
29	28	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝑥 ( +g ‘ ( 1o mPwSer 𝑆 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑄 ) 𝑦 ) )
30		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
31	1 6 30	psr1mulr	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ ( 1o mPwSer 𝑅 ) )
32	31	eqcomi	⊢ ( .r ‘ ( 1o mPwSer 𝑅 ) ) = ( .r ‘ 𝑃 )
33	32	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( .r ‘ ( 1o mPwSer 𝑅 ) ) = ( .r ‘ 𝑃 ) )
34	33	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑃 ) ∧ 𝑦 ∈ ( Base ‘ 𝑃 ) ) ) → ( 𝑥 ( .r ‘ ( 1o mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) )
35		eqid	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
36	2 7 35	psr1mulr	⊢ ( .r ‘ 𝑄 ) = ( .r ‘ ( 1o mPwSer 𝑆 ) )
37	36	eqcomi	⊢ ( .r ‘ ( 1o mPwSer 𝑆 ) ) = ( .r ‘ 𝑄 )
38	37	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( .r ‘ ( 1o mPwSer 𝑆 ) ) = ( .r ‘ 𝑄 ) )
39	38	oveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝑄 ) ∧ 𝑦 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝑥 ( .r ‘ ( 1o mPwSer 𝑆 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑄 ) 𝑦 ) )
40	14 17 18 19 24 29 34 39	rhmpropd	⊢ ( 𝜑 → ( ( 1o mPwSer 𝑅 ) RingHom ( 1o mPwSer 𝑆 ) ) = ( 𝑃 RingHom 𝑄 ) )
41	11 40	eleqtrd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )