Theorem mhmcoaddmpl

Description: Show that the ring homomorphism in rhmmpl preserves addition. (Contributed by SN, 8-Feb-2025)

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

Proof

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