Theorem mhmcoaddpsr

Description: Show that the ring homomorphism in rhmpsr preserves addition. (Contributed by SN, 18-May-2025)

	Ref	Expression
Hypotheses	mhmcoaddpsr.p	⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
	mhmcoaddpsr.q	⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
	mhmcoaddpsr.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mhmcoaddpsr.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
	mhmcoaddpsr.1	⊢ + = ( +g ‘ 𝑃 )
	mhmcoaddpsr.2	⊢ + = ( +g ‘ 𝑄 )
	mhmcoaddpsr.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
	mhmcoaddpsr.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	mhmcoaddpsr.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion	mhmcoaddpsr	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 + 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) + ( 𝐻 ∘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mhmcoaddpsr.p	⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
2		mhmcoaddpsr.q	⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
3		mhmcoaddpsr.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		mhmcoaddpsr.c	⊢ 𝐶 = ( Base ‘ 𝑄 )
5		mhmcoaddpsr.1	⊢ + = ( +g ‘ 𝑃 )
6		mhmcoaddpsr.2	⊢ + = ( +g ‘ 𝑄 )
7		mhmcoaddpsr.h	⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
8		mhmcoaddpsr.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		mhmcoaddpsr.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
10		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
11		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
12	11	rabex	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
13	12	a1i	⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
14		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
16	1 14 15 3 8	psrelbas	⊢ ( 𝜑 → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
17	10 13 16	elmapdd	⊢ ( 𝜑 → 𝐹 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
18	1 14 15 3 9	psrelbas	⊢ ( 𝜑 → 𝐺 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
19	10 13 18	elmapdd	⊢ ( 𝜑 → 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
20		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
21		eqid	⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
22	14 20 21	mhmvlin	⊢ ( ( 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐹 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝐺 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) → ( 𝐻 ∘ ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∘f ( +g ‘ 𝑆 ) ( 𝐻 ∘ 𝐺 ) ) )
23	7 17 19 22	syl3anc	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∘f ( +g ‘ 𝑆 ) ( 𝐻 ∘ 𝐺 ) ) )
24	1 3 20 5 8 9	psradd	⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) = ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) )
25	24	coeq2d	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 + 𝐺 ) ) = ( 𝐻 ∘ ( 𝐹 ∘f ( +g ‘ 𝑅 ) 𝐺 ) ) )
26	1 2 3 4 7 8	mhmcopsr	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ 𝐶 )
27	1 2 3 4 7 9	mhmcopsr	⊢ ( 𝜑 → ( 𝐻 ∘ 𝐺 ) ∈ 𝐶 )
28	2 4 21 6 26 27	psradd	⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) + ( 𝐻 ∘ 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ∘f ( +g ‘ 𝑆 ) ( 𝐻 ∘ 𝐺 ) ) )
29	23 25 28	3eqtr4d	⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 + 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) + ( 𝐻 ∘ 𝐺 ) ) )