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 ⊢ P = I mPwSer R
mhmcoaddpsr.q ⊢ Q = I mPwSer S
mhmcoaddpsr.b ⊢ B = Base P
mhmcoaddpsr.c ⊢ C = Base Q
mhmcoaddpsr.1 ⊢ + ˙ = + P
mhmcoaddpsr.2 ⊢ ✚ ˙ = + Q
mhmcoaddpsr.h ⊢ φ → H ∈ R MndHom S
mhmcoaddpsr.f ⊢ φ → F ∈ B
mhmcoaddpsr.g ⊢ φ → G ∈ B
Assertion mhmcoaddpsr ⊢ φ → H ∘ F + ˙ G = H ∘ F ✚ ˙ H ∘ G

Proof

Step Hyp Ref Expression
1 mhmcoaddpsr.p ⊢ P = I mPwSer R
2 mhmcoaddpsr.q ⊢ Q = I mPwSer S
3 mhmcoaddpsr.b ⊢ B = Base P
4 mhmcoaddpsr.c ⊢ C = Base Q
5 mhmcoaddpsr.1 ⊢ + ˙ = + P
6 mhmcoaddpsr.2 ⊢ ✚ ˙ = + Q
7 mhmcoaddpsr.h ⊢ φ → H ∈ R MndHom S
8 mhmcoaddpsr.f ⊢ φ → F ∈ B
9 mhmcoaddpsr.g ⊢ φ → G ∈ B
10 fvexd ⊢ φ → Base R ∈ V
11 ovex ⊢ ℕ 0 I ∈ V
12 11 rabex ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∈ V
13 12 a1i ⊢ φ → f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∈ V
14 eqid ⊢ Base R = Base R
15 eqid ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
16 1 14 15 3 8 psrelbas ⊢ φ → F : f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟶ Base R
17 10 13 16 elmapdd ⊢ φ → F ∈ Base R f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
18 1 14 15 3 9 psrelbas ⊢ φ → G : f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟶ Base R
19 10 13 18 elmapdd ⊢ φ → G ∈ Base R f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
20 eqid ⊢ + R = + R
21 eqid ⊢ + S = + S
22 14 20 21 mhmvlin ⊢ H ∈ R MndHom S ∧ F ∈ Base R f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∧ G ∈ Base R f ∈ ℕ 0 I | f -1 ℕ ∈ Fin → H ∘ F + R f G = H ∘ F + S f H ∘ G
23 7 17 19 22 syl3anc ⊢ φ → H ∘ F + R f G = H ∘ F + S f H ∘ G
24 1 3 20 5 8 9 psradd ⊢ φ → F + ˙ G = F + R f G
25 24 coeq2d ⊢ φ → H ∘ F + ˙ G = H ∘ F + R f G
26 1 2 3 4 7 8 mhmcopsr ⊢ φ → H ∘ F ∈ C
27 1 2 3 4 7 9 mhmcopsr ⊢ φ → H ∘ G ∈ C
28 2 4 21 6 26 27 psradd ⊢ φ → H ∘ F ✚ ˙ H ∘ G = H ∘ F + S f H ∘ G
29 23 25 28 3eqtr4d ⊢ φ → H ∘ F + ˙ G = H ∘ F ✚ ˙ H ∘ G