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