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 𝑃 = ( 𝐼 mPoly 𝑅 )
rhmmpl.q 𝑄 = ( 𝐼 mPoly 𝑆 )
rhmmpl.b 𝐵 = ( Base ‘ 𝑃 )
rhmmpl.f 𝐹 = ( 𝑝𝐵 ↦ ( 𝐻𝑝 ) )
rhmmpl.i ( 𝜑𝐼𝑉 )
rhmmpl.h ( 𝜑𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion rhmmpl ( 𝜑𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )

Proof

Step Hyp Ref Expression
1 rhmmpl.p 𝑃 = ( 𝐼 mPoly 𝑅 )
2 rhmmpl.q 𝑄 = ( 𝐼 mPoly 𝑆 )
3 rhmmpl.b 𝐵 = ( Base ‘ 𝑃 )
4 rhmmpl.f 𝐹 = ( 𝑝𝐵 ↦ ( 𝐻𝑝 ) )
5 rhmmpl.i ( 𝜑𝐼𝑉 )
6 rhmmpl.h ( 𝜑𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
7 eqid ( 1r𝑃 ) = ( 1r𝑃 )
8 eqid ( 1r𝑄 ) = ( 1r𝑄 )
9 eqid ( .r𝑃 ) = ( .r𝑃 )
10 eqid ( .r𝑄 ) = ( .r𝑄 )
11 rhmrcl1 ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
12 6 11 syl ( 𝜑𝑅 ∈ Ring )
13 1 5 12 mplringd ( 𝜑𝑃 ∈ Ring )
14 rhmrcl2 ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
15 6 14 syl ( 𝜑𝑆 ∈ Ring )
16 2 5 15 mplringd ( 𝜑𝑄 ∈ Ring )
17 eqid { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
18 eqid ( 0g𝑅 ) = ( 0g𝑅 )
19 eqid ( 1r𝑅 ) = ( 1r𝑅 )
20 1 17 18 19 7 5 12 mpl1 ( 𝜑 → ( 1r𝑃 ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) )
21 20 coeq2d ( 𝜑 → ( 𝐻 ∘ ( 1r𝑃 ) ) = ( 𝐻 ∘ ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) )
22 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
24 22 23 rhmf ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
25 6 24 syl ( 𝜑𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
26 22 19 ringidcl ( 𝑅 ∈ Ring → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27 12 26 syl ( 𝜑 → ( 1r𝑅 ) ∈ ( Base ‘ 𝑅 ) )
28 22 18 ring0cl ( 𝑅 ∈ Ring → ( 0g𝑅 ) ∈ ( Base ‘ 𝑅 ) )
29 12 28 syl ( 𝜑 → ( 0g𝑅 ) ∈ ( Base ‘ 𝑅 ) )
30 27 29 ifcld ( 𝜑 → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
31 30 adantr ( ( 𝜑𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ) → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
32 25 31 cofmpt ( 𝜑 → ( 𝐻 ∘ ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) )
33 fvif ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 𝐻 ‘ ( 1r𝑅 ) ) , ( 𝐻 ‘ ( 0g𝑅 ) ) )
34 eqid ( 1r𝑆 ) = ( 1r𝑆 )
35 19 34 rhm1 ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐻 ‘ ( 1r𝑅 ) ) = ( 1r𝑆 ) )
36 6 35 syl ( 𝜑 → ( 𝐻 ‘ ( 1r𝑅 ) ) = ( 1r𝑆 ) )
37 rhmghm ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
38 eqid ( 0g𝑆 ) = ( 0g𝑆 )
39 18 38 ghmid ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐻 ‘ ( 0g𝑅 ) ) = ( 0g𝑆 ) )
40 6 37 39 3syl ( 𝜑 → ( 𝐻 ‘ ( 0g𝑅 ) ) = ( 0g𝑆 ) )
41 36 40 ifeq12d ( 𝜑 → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 𝐻 ‘ ( 1r𝑅 ) ) , ( 𝐻 ‘ ( 0g𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑆 ) , ( 0g𝑆 ) ) )
42 33 41 eqtrid ( 𝜑 → ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑆 ) , ( 0g𝑆 ) ) )
43 42 mpteq2dv ( 𝜑 → ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑅 ) , ( 0g𝑅 ) ) ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑆 ) , ( 0g𝑆 ) ) ) )
44 21 32 43 3eqtrd ( 𝜑 → ( 𝐻 ∘ ( 1r𝑃 ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑆 ) , ( 0g𝑆 ) ) ) )
45 coeq2 ( 𝑝 = ( 1r𝑃 ) → ( 𝐻𝑝 ) = ( 𝐻 ∘ ( 1r𝑃 ) ) )
46 3 7 ringidcl ( 𝑃 ∈ Ring → ( 1r𝑃 ) ∈ 𝐵 )
47 13 46 syl ( 𝜑 → ( 1r𝑃 ) ∈ 𝐵 )
48 6 47 coexd ( 𝜑 → ( 𝐻 ∘ ( 1r𝑃 ) ) ∈ V )
49 4 45 47 48 fvmptd3 ( 𝜑 → ( 𝐹 ‘ ( 1r𝑃 ) ) = ( 𝐻 ∘ ( 1r𝑃 ) ) )
50 2 17 38 34 8 5 15 mpl1 ( 𝜑 → ( 1r𝑄 ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r𝑆 ) , ( 0g𝑆 ) ) ) )
51 44 49 50 3eqtr4d ( 𝜑 → ( 𝐹 ‘ ( 1r𝑃 ) ) = ( 1r𝑄 ) )
52 eqid ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
53 6 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
54 simprl ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑥𝐵 )
55 simprr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑦𝐵 )
56 1 2 3 52 9 10 53 54 55 rhmcomulmpl ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r𝑃 ) 𝑦 ) ) = ( ( 𝐻𝑥 ) ( .r𝑄 ) ( 𝐻𝑦 ) ) )
57 coeq2 ( 𝑝 = ( 𝑥 ( .r𝑃 ) 𝑦 ) → ( 𝐻𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( .r𝑃 ) 𝑦 ) ) )
58 13 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑃 ∈ Ring )
59 3 9 58 54 55 ringcld ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝑃 ) 𝑦 ) ∈ 𝐵 )
60 ovexd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( .r𝑃 ) 𝑦 ) ∈ V )
61 53 60 coexd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r𝑃 ) 𝑦 ) ) ∈ V )
62 4 57 59 61 fvmptd3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( .r𝑃 ) 𝑦 ) ) )
63 coeq2 ( 𝑝 = 𝑥 → ( 𝐻𝑝 ) = ( 𝐻𝑥 ) )
64 53 54 coexd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐻𝑥 ) ∈ V )
65 4 63 54 64 fvmptd3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐹𝑥 ) = ( 𝐻𝑥 ) )
66 coeq2 ( 𝑝 = 𝑦 → ( 𝐻𝑝 ) = ( 𝐻𝑦 ) )
67 53 55 coexd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐻𝑦 ) ∈ V )
68 4 66 55 67 fvmptd3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐹𝑦 ) = ( 𝐻𝑦 ) )
69 65 68 oveq12d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝐹𝑥 ) ( .r𝑄 ) ( 𝐹𝑦 ) ) = ( ( 𝐻𝑥 ) ( .r𝑄 ) ( 𝐻𝑦 ) ) )
70 56 62 69 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r𝑃 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( .r𝑄 ) ( 𝐹𝑦 ) ) )
71 eqid ( +g𝑃 ) = ( +g𝑃 )
72 eqid ( +g𝑄 ) = ( +g𝑄 )
73 ghmmhm ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
74 6 37 73 3syl ( 𝜑𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
75 74 adantr ( ( 𝜑𝑝𝐵 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
76 simpr ( ( 𝜑𝑝𝐵 ) → 𝑝𝐵 )
77 1 2 3 52 75 76 mhmcompl ( ( 𝜑𝑝𝐵 ) → ( 𝐻𝑝 ) ∈ ( Base ‘ 𝑄 ) )
78 77 4 fmptd ( 𝜑𝐹 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )
79 53 37 73 3syl ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
80 1 2 3 52 71 72 79 54 55 mhmcoaddmpl ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) = ( ( 𝐻𝑥 ) ( +g𝑄 ) ( 𝐻𝑦 ) ) )
81 coeq2 ( 𝑝 = ( 𝑥 ( +g𝑃 ) 𝑦 ) → ( 𝐻𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) )
82 13 ringgrpd ( 𝜑𝑃 ∈ Grp )
83 82 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑃 ∈ Grp )
84 3 71 83 54 55 grpcld ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑃 ) 𝑦 ) ∈ 𝐵 )
85 ovexd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑃 ) 𝑦 ) ∈ V )
86 53 85 coexd ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) ∈ V )
87 4 81 84 86 fvmptd3 ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) )
88 65 68 oveq12d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝐹𝑥 ) ( +g𝑄 ) ( 𝐹𝑦 ) ) = ( ( 𝐻𝑥 ) ( +g𝑄 ) ( 𝐻𝑦 ) ) )
89 80 87 88 3eqtr4d ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g𝑃 ) 𝑦 ) ) = ( ( 𝐹𝑥 ) ( +g𝑄 ) ( 𝐹𝑦 ) ) )
90 3 7 8 9 10 13 16 51 70 52 71 72 78 89 isrhmd ( 𝜑𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )