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