Metamath Proof Explorer

Theorem evlsmaprhm

Description: The function F mapping polynomials p to their subring evaluation at a given point X is a ring homomorphism. Compare evls1maprhm . (Contributed by SN, 12-Mar-2025)

Ref Expression
Hypotheses evlsmaprhm.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝑆 )
evlsmaprhm.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
evlsmaprhm.u ⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
evlsmaprhm.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
evlsmaprhm.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
evlsmaprhm.f ⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝐴 ) )
evlsmaprhm.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlsmaprhm.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evlsmaprhm.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
evlsmaprhm.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
Assertion evlsmaprhm ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )

Proof

Step Hyp Ref Expression
1 evlsmaprhm.q ⊢ 𝑄 = ( ( 𝐼 evalSub 𝑅 ) ‘ 𝑆 )
2 evlsmaprhm.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑈 )
3 evlsmaprhm.u ⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
4 evlsmaprhm.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
5 evlsmaprhm.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
6 evlsmaprhm.f ⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( ( 𝑄 ‘ 𝑝 ) ‘ 𝐴 ) )
7 evlsmaprhm.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8 evlsmaprhm.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
9 evlsmaprhm.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
10 evlsmaprhm.a ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
11 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
12 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
13 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
14 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
15 3 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → 𝑈 ∈ Ring )
16 9 15 syl ⊢ ( 𝜑 → 𝑈 ∈ Ring )
17 2 7 16 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
18 8 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
19 fveq2 ⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( 𝑄 ‘ 𝑝 ) = ( 𝑄 ‘ ( 1r ‘ 𝑃 ) ) )
20 19 fveq1d ⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝐴 ) )
21 4 11 ringidcl ⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
22 17 21 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
23 fvexd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝐴 ) ∈ V )
24 6 20 22 23 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( ( 𝑄 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝐴 ) )
25 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
26 eqid ⊢ ( 1r ‘ 𝑈 ) = ( 1r ‘ 𝑈 )
27 2 25 26 11 7 16 mplascl1 ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑈 ) ) = ( 1r ‘ 𝑃 ) )
28 27 eqcomd ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑈 ) ) )
29 28 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ ( 1r ‘ 𝑃 ) ) = ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑈 ) ) ) )
30 29 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝐴 ) = ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑈 ) ) ) ‘ 𝐴 ) )
31 3 12 subrg1 ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑈 ) )
32 9 31 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑈 ) )
33 12 subrg1cl ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
34 9 33 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
35 32 34 eqeltrrd ⊢ ( 𝜑 → ( 1r ‘ 𝑈 ) ∈ 𝑆 )
36 1 2 3 5 4 25 7 8 9 35 10 evlsscaval ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑈 ) ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑈 ) ) ) ‘ 𝐴 ) = ( 1r ‘ 𝑈 ) ) )
37 36 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑈 ) ) ) ‘ 𝐴 ) = ( 1r ‘ 𝑈 ) )
38 37 32 eqtr4d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑈 ) ) ) ‘ 𝐴 ) = ( 1r ‘ 𝑅 ) )
39 24 30 38 3eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑅 ) )
40 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝐼 ∈ 𝑉 )
41 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑅 ∈ CRing )
42 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
43 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
44 simprl ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑞 ∈ 𝐵 )
45 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) )
46 44 45 jca ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) ) )
47 simprr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑟 ∈ 𝐵 )
48 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) )
49 47 48 jca ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑟 ∈ 𝐵 ∧ ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) ) )
50 1 2 3 5 4 40 41 42 43 46 49 13 14 evlsmulval ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) ( .r ‘ 𝑅 ) ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) ) ) )
51 50 simprd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑄 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) ( .r ‘ 𝑅 ) ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) ) )
52 fveq2 ⊢ ( 𝑝 = ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) → ( 𝑄 ‘ 𝑝 ) = ( 𝑄 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) )
53 52 fveq1d ⊢ ( 𝑝 = ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) )
54 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
55 4 13 54 44 47 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ∈ 𝐵 )
56 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑄 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) ∈ V )
57 6 53 55 56 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝑄 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) )
58 fveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝑄 ‘ 𝑝 ) = ( 𝑄 ‘ 𝑞 ) )
59 58 fveq1d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) )
60 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) ∈ V )
61 6 59 44 60 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑞 ) = ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) )
62 fveq2 ⊢ ( 𝑝 = 𝑟 → ( 𝑄 ‘ 𝑝 ) = ( 𝑄 ‘ 𝑟 ) )
63 62 fveq1d ⊢ ( 𝑝 = 𝑟 → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) )
64 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) ∈ V )
65 6 63 47 64 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑟 ) = ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) )
66 61 65 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) = ( ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) ( .r ‘ 𝑅 ) ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) ) )
67 51 57 66 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝐹 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) )
68 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
69 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
70 7 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐼 ∈ 𝑉 )
71 8 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑅 ∈ CRing )
72 9 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
73 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
74 10 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐴 ∈ ( 𝐾 ↑m 𝐼 ) )
75 1 2 3 4 5 70 71 72 73 74 evlscl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝐴 ) ∈ 𝐾 )
76 75 6 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐾 )
77 1 2 3 5 4 40 41 42 43 46 49 68 69 evlsaddval ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ∈ 𝐵 ∧ ( ( 𝑄 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) ( +g ‘ 𝑅 ) ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) ) ) )
78 77 simprd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑄 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) = ( ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) ( +g ‘ 𝑅 ) ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) ) )
79 fveq2 ⊢ ( 𝑝 = ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) → ( 𝑄 ‘ 𝑝 ) = ( 𝑄 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) )
80 79 fveq1d ⊢ ( 𝑝 = ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) → ( ( 𝑄 ‘ 𝑝 ) ‘ 𝐴 ) = ( ( 𝑄 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) )
81 17 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
82 81 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → 𝑃 ∈ Grp )
83 4 68 82 44 47 grpcld ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ∈ 𝐵 )
84 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝑄 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) ∈ V )
85 6 80 83 84 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝑄 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝐴 ) )
86 61 65 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑞 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) = ( ( ( 𝑄 ‘ 𝑞 ) ‘ 𝐴 ) ( +g ‘ 𝑅 ) ( ( 𝑄 ‘ 𝑟 ) ‘ 𝐴 ) ) )
87 78 85 86 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝐹 ‘ 𝑞 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) )
88 4 11 12 13 14 17 18 39 67 5 68 69 76 87 isrhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )