Theorem 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	⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
	rhmpsr.q	⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
	rhmpsr.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	rhmpsr.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
	rhmpsr.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	rhmpsr.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion	rhmpsr	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		rhmpsr.p	⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
2		rhmpsr.q	⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
3		rhmpsr.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		rhmpsr.f	⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
5		rhmpsr.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6		rhmpsr.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	psrring	⊢ ( 𝜑 → 𝑃 ∈ Ring )
14		rhmrcl2	⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
15	6 14	syl	⊢ ( 𝜑 → 𝑆 ∈ Ring )
16	2 5 15	psrring	⊢ ( 𝜑 → 𝑄 ∈ Ring )
17		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
18		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20	1 5 12 17 18 19 7	psr1	⊢ ( 𝜑 → ( 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 5 15 17 38 34 8	psr1	⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) ) )
51	44 49 50	3eqtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑄 ) )
52		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
53	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
54		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
55		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
56	1 2 3 52 9 10 53 54 55	rhmcomulpsr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
57		coeq2	⊢ ( 𝑝 = ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
58	13	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
59	3 9 58 54 55	ringcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
60	53 59	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) ∈ V )
61	4 57 59 60	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
62		coeq2	⊢ ( 𝑝 = 𝑥 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑥 ) )
63	53 54	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ 𝑥 ) ∈ V )
64	4 62 54 63	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ∘ 𝑥 ) )
65		coeq2	⊢ ( 𝑝 = 𝑦 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑦 ) )
66	53 55	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ 𝑦 ) ∈ V )
67	4 65 55 66	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ∘ 𝑦 ) )
68	64 67	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
69	56 61 68	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) )
70		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
71		eqid	⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
72		ghmmhm	⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
73	6 37 72	3syl	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
74	73	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
75		simpr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
76	1 2 3 52 74 75	mhmcopsr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝐻 ∘ 𝑝 ) ∈ ( Base ‘ 𝑄 ) )
77	76 4	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )
78	53 37 72	3syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
79	1 2 3 52 70 71 78 54 55	mhmcoaddpsr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
80		coeq2	⊢ ( 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) )
81	58	ringgrpd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Grp )
82	3 70 81 54 55	grpcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
83	53 82	coexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) ∈ V )
84	4 80 82 83	fvmptd3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) )
85	64 67	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
86	79 84 85	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) )
87	3 7 8 9 10 13 16 51 69 52 70 71 77 86	isrhmd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )