Metamath Proof Explorer


Theorem rhmmpl

Description: Provide a ring homomorphism between two polynomial algebras over their respective base rings given a ring homomorphism between the two base rings. Compare pwsco2rhm . (Contributed by SN, 8-Feb-2025)

Ref Expression
Hypotheses rhmmpl.p P = I mPoly R
rhmmpl.q Q = I mPoly S
rhmmpl.b B = Base P
rhmmpl.f F = p B H p
rhmmpl.i φ I V
rhmmpl.h φ H R RingHom S
Assertion rhmmpl φ F P RingHom Q

Proof

Step Hyp Ref Expression
1 rhmmpl.p P = I mPoly R
2 rhmmpl.q Q = I mPoly S
3 rhmmpl.b B = Base P
4 rhmmpl.f F = p B H p
5 rhmmpl.i φ I V
6 rhmmpl.h φ H R RingHom S
7 eqid 1 P = 1 P
8 eqid 1 Q = 1 Q
9 eqid P = P
10 eqid Q = Q
11 rhmrcl1 H R RingHom S R Ring
12 6 11 syl φ R Ring
13 1 5 12 mplringd φ P Ring
14 rhmrcl2 H R RingHom S S Ring
15 6 14 syl φ S Ring
16 2 5 15 mplringd φ Q Ring
17 eqid f 0 I | f -1 Fin = f 0 I | f -1 Fin
18 eqid 0 R = 0 R
19 eqid 1 R = 1 R
20 1 17 18 19 7 5 12 mpl1 φ 1 P = d f 0 I | f -1 Fin if d = I × 0 1 R 0 R
21 20 coeq2d φ H 1 P = H d f 0 I | f -1 Fin if d = I × 0 1 R 0 R
22 eqid Base R = Base R
23 eqid Base S = Base S
24 22 23 rhmf H R RingHom S H : Base R Base S
25 6 24 syl φ H : Base R Base S
26 22 19 ringidcl R Ring 1 R Base R
27 12 26 syl φ 1 R Base R
28 22 18 ring0cl R Ring 0 R Base R
29 12 28 syl φ 0 R Base R
30 27 29 ifcld φ if d = I × 0 1 R 0 R Base R
31 30 adantr φ d f 0 I | f -1 Fin if d = I × 0 1 R 0 R Base R
32 25 31 cofmpt φ H d f 0 I | f -1 Fin if d = I × 0 1 R 0 R = d f 0 I | f -1 Fin H if d = I × 0 1 R 0 R
33 fvif H if d = I × 0 1 R 0 R = if d = I × 0 H 1 R H 0 R
34 eqid 1 S = 1 S
35 19 34 rhm1 H R RingHom S H 1 R = 1 S
36 6 35 syl φ H 1 R = 1 S
37 rhmghm H R RingHom S H R GrpHom S
38 eqid 0 S = 0 S
39 18 38 ghmid H R GrpHom S H 0 R = 0 S
40 6 37 39 3syl φ H 0 R = 0 S
41 36 40 ifeq12d φ if d = I × 0 H 1 R H 0 R = if d = I × 0 1 S 0 S
42 33 41 eqtrid φ H if d = I × 0 1 R 0 R = if d = I × 0 1 S 0 S
43 42 mpteq2dv φ d f 0 I | f -1 Fin H if d = I × 0 1 R 0 R = d f 0 I | f -1 Fin if d = I × 0 1 S 0 S
44 21 32 43 3eqtrd φ H 1 P = d f 0 I | f -1 Fin if d = I × 0 1 S 0 S
45 coeq2 p = 1 P H p = H 1 P
46 3 7 ringidcl P Ring 1 P B
47 13 46 syl φ 1 P B
48 6 47 coexd φ H 1 P V
49 4 45 47 48 fvmptd3 φ F 1 P = H 1 P
50 2 17 38 34 8 5 15 mpl1 φ 1 Q = d f 0 I | f -1 Fin if d = I × 0 1 S 0 S
51 44 49 50 3eqtr4d φ F 1 P = 1 Q
52 eqid Base Q = Base Q
53 6 adantr φ x B y B H R RingHom S
54 simprl φ x B y B x B
55 simprr φ x B y B y B
56 1 2 3 52 9 10 53 54 55 rhmcomulmpl φ x B y B H x P y = H x Q H y
57 coeq2 p = x P y H p = H x P y
58 13 adantr φ x B y B P Ring
59 3 9 58 54 55 ringcld φ x B y B x P y B
60 ovexd φ x B y B x P y V
61 53 60 coexd φ x B y B H x P y V
62 4 57 59 61 fvmptd3 φ x B y B F x P y = H x P y
63 coeq2 p = x H p = H x
64 53 54 coexd φ x B y B H x V
65 4 63 54 64 fvmptd3 φ x B y B F x = H x
66 coeq2 p = y H p = H y
67 53 55 coexd φ x B y B H y V
68 4 66 55 67 fvmptd3 φ x B y B F y = H y
69 65 68 oveq12d φ x B y B F x Q F y = H x Q H y
70 56 62 69 3eqtr4d φ x B y B F x P y = F x Q F y
71 eqid + P = + P
72 eqid + Q = + Q
73 ghmmhm H R GrpHom S H R MndHom S
74 6 37 73 3syl φ H R MndHom S
75 74 adantr φ p B H R MndHom S
76 simpr φ p B p B
77 1 2 3 52 75 76 mhmcompl φ p B H p Base Q
78 77 4 fmptd φ F : B Base Q
79 53 37 73 3syl φ x B y B H R MndHom S
80 1 2 3 52 71 72 79 54 55 mhmcoaddmpl φ x B y B H x + P y = H x + Q H y
81 coeq2 p = x + P y H p = H x + P y
82 13 ringgrpd φ P Grp
83 82 adantr φ x B y B P Grp
84 3 71 83 54 55 grpcld φ x B y B x + P y B
85 ovexd φ x B y B x + P y V
86 53 85 coexd φ x B y B H x + P y V
87 4 81 84 86 fvmptd3 φ x B y B F x + P y = H x + P y
88 65 68 oveq12d φ x B y B F x + Q F y = H x + Q H y
89 80 87 88 3eqtr4d φ x B y B F x + P y = F x + Q F y
90 3 7 8 9 10 13 16 51 70 52 71 72 78 89 isrhmd φ F P RingHom Q