This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝐹 + 𝐺 ) ) = ( ( 𝐻 ∘ 𝐹 ) ✚ ( 𝐻 ∘ 𝐺 ) ) )