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

Metamath Proof Explorer

Theorem mhmcoaddmpl

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

Ref Expression
Hypotheses mhmcoaddmpl.p ⊢ P = I mPoly R
mhmcoaddmpl.q ⊢ Q = I mPoly S
mhmcoaddmpl.b ⊢ B = Base P
mhmcoaddmpl.c ⊢ C = Base Q
mhmcoaddmpl.1 ⊢ + ˙ = + P
mhmcoaddmpl.2 ⊢ ✚ ˙ = + Q
mhmcoaddmpl.h ⊢ φ → H ∈ R MndHom S
mhmcoaddmpl.f ⊢ φ → F ∈ B
mhmcoaddmpl.g ⊢ φ → G ∈ B
Assertion mhmcoaddmpl ⊢ φ → H ∘ F + ˙ G = H ∘ F ✚ ˙ H ∘ G

Proof

Step Hyp Ref Expression
1 mhmcoaddmpl.p ⊢ P = I mPoly R
2 mhmcoaddmpl.q ⊢ Q = I mPoly S
3 mhmcoaddmpl.b ⊢ B = Base P
4 mhmcoaddmpl.c ⊢ C = Base Q
5 mhmcoaddmpl.1 ⊢ + ˙ = + P
6 mhmcoaddmpl.2 ⊢ ✚ ˙ = + Q
7 mhmcoaddmpl.h ⊢ φ → H ∈ R MndHom S
8 mhmcoaddmpl.f ⊢ φ → F ∈ B
9 mhmcoaddmpl.g ⊢ φ → G ∈ B
10 fvexd ⊢ φ → Base R ∈ V
11 eqid ⊢ f ∈ ℕ 0 I | f -1 ℕ ∈ Fin = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
12 ovexd ⊢ φ → ℕ 0 I ∈ V
13 11 12 rabexd ⊢ φ → f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ∈ V
14 eqid ⊢ Base R = Base R
15 1 14 3 11 8 mplelf ⊢ φ → F : f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟶ Base R
16 10 13 15 elmapdd ⊢ φ → F ∈ Base R f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
17 1 14 3 11 9 mplelf ⊢ φ → G : f ∈ ℕ 0 I | f -1 ℕ ∈ Fin ⟶ Base R
18 10 13 17 elmapdd ⊢ φ → G ∈ Base R f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
19 eqid ⊢ + R = + R
20 eqid ⊢ + S = + S
21 14 19 20 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
22 7 16 18 21 syl3anc ⊢ φ → H ∘ F + R f G = H ∘ F + S f H ∘ G
23 1 3 19 5 8 9 mpladd ⊢ φ → F + ˙ G = F + R f G
24 23 coeq2d ⊢ φ → H ∘ F + ˙ G = H ∘ F + R f G
25 1 2 3 4 7 8 mhmcompl ⊢ φ → H ∘ F ∈ C
26 1 2 3 4 7 9 mhmcompl ⊢ φ → H ∘ G ∈ C
27 2 4 20 6 25 26 mpladd ⊢ φ → H ∘ F ✚ ˙ H ∘ G = H ∘ F + S f H ∘ G
28 22 24 27 3eqtr4d ⊢ φ → H ∘ F + ˙ G = H ∘ F ✚ ˙ H ∘ G