This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evls1maprhm

Description: The function F mapping polynomials p to their subring evaluation at a given point X is a ring homomorphism. (Contributed by Thierry Arnoux, 8-Feb-2025)

Ref Expression
Hypotheses evls1maprhm.q ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
evls1maprhm.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
evls1maprhm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evls1maprhm.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
evls1maprhm.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evls1maprhm.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
evls1maprhm.y ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
evls1maprhm.f ⊢ 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
Assertion evls1maprhm ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )

Proof

Step Hyp Ref Expression
1 evls1maprhm.q ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2 evls1maprhm.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3 evls1maprhm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 evls1maprhm.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
5 evls1maprhm.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
6 evls1maprhm.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
7 evls1maprhm.y ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 evls1maprhm.f ⊢ 𝐹 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
9 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
10 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
11 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
14 13 subrgcrng ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝑅 ↾s 𝑆 ) ∈ CRing )
15 5 6 14 syl2anc ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ CRing )
16 2 ply1crng ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ CRing → 𝑃 ∈ CRing )
17 15 16 syl ⊢ ( 𝜑 → 𝑃 ∈ CRing )
18 17 crngringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
19 5 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
20 fveq2 ⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) )
21 20 fveq1d ⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝑋 ) )
22 4 9 ringidcl ⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝑈 )
23 18 22 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ 𝑈 )
24 fvexd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝑋 ) ∈ V )
25 8 21 23 24 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝑋 ) )
26 13 10 subrg1 ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
27 6 26 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) )
28 27 fveq2d ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
29 15 crngringd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
30 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
31 eqid ⊢ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) = ( 1r ‘ ( 𝑅 ↾s 𝑆 ) )
32 2 30 31 9 ply1scl1 ⊢ ( ( 𝑅 ↾s 𝑆 ) ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 1r ‘ 𝑃 ) )
33 29 32 syl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 1r ‘ 𝑃 ) )
34 28 33 eqtr2d ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) )
35 34 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) )
36 35 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 1r ‘ 𝑃 ) ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) )
37 10 subrg1cl ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
38 6 37 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
39 1 2 13 3 30 5 6 38 7 evls1scafv ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) ) ‘ 𝑋 ) = ( 1r ‘ 𝑅 ) )
40 25 36 39 3eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑅 ) )
41 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑅 ∈ CRing )
42 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
43 simprl ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑞 ∈ 𝑈 )
44 simprr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑟 ∈ 𝑈 )
45 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
46 1 3 2 13 4 11 12 41 42 43 44 45 evls1muld ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) = ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ) )
47 fveq2 ⊢ ( 𝑝 = ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) )
48 47 fveq1d ⊢ ( 𝑝 = ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) )
49 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑃 ∈ Ring )
50 4 11 49 43 44 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ∈ 𝑈 )
51 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) ∈ V )
52 8 48 50 51 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝑂 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) )
53 fveq2 ⊢ ( 𝑝 = 𝑞 → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ 𝑞 ) )
54 53 fveq1d ⊢ ( 𝑝 = 𝑞 → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) )
55 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ∈ V )
56 8 54 43 55 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ 𝑞 ) = ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) )
57 fveq2 ⊢ ( 𝑝 = 𝑟 → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ 𝑟 ) )
58 57 fveq1d ⊢ ( 𝑝 = 𝑟 → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) )
59 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ∈ V )
60 8 58 44 59 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ 𝑟 ) = ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) )
61 56 60 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝐹 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) = ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ( .r ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ) )
62 46 52 61 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑞 ( .r ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝐹 ‘ 𝑞 ) ( .r ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) )
63 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
64 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
65 eqid ⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
66 1 3 2 13 4 65 5 6 ressply1evl ⊢ ( 𝜑 → 𝑂 = ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) )
67 66 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑂 = ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) )
68 67 fveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑂 ‘ 𝑝 ) = ( ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) ‘ 𝑝 ) )
69 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ 𝑈 )
70 69 fvresd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( ( eval1 ‘ 𝑅 ) ↾ 𝑈 ) ‘ 𝑝 ) = ( ( eval1 ‘ 𝑅 ) ‘ 𝑝 ) )
71 68 70 eqtrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( 𝑂 ‘ 𝑝 ) = ( ( eval1 ‘ 𝑅 ) ‘ 𝑝 ) )
72 71 fveq1d ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( ( eval1 ‘ 𝑅 ) ‘ 𝑝 ) ‘ 𝑋 ) )
73 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
74 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
75 5 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑅 ∈ CRing )
76 7 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑋 ∈ 𝐵 )
77 eqid ⊢ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) )
78 eqid ⊢ ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
79 73 13 2 4 6 77 78 74 ressply1bas2 ⊢ ( 𝜑 → 𝑈 = ( ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) )
80 inss2 ⊢ ( ( Base ‘ ( PwSer1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ∩ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) ⊆ ( Base ‘ ( Poly1 ‘ 𝑅 ) )
81 79 80 eqsstrdi ⊢ ( 𝜑 → 𝑈 ⊆ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
82 81 sselda ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
83 65 73 3 74 75 76 82 fveval1fvcl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( ( eval1 ‘ 𝑅 ) ‘ 𝑝 ) ‘ 𝑋 ) ∈ 𝐵 )
84 72 83 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ∈ 𝐵 )
85 84 8 fmptd ⊢ ( 𝜑 → 𝐹 : 𝑈 ⟶ 𝐵 )
86 1 3 2 13 4 63 64 41 42 43 44 45 evls1addd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) = ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ) )
87 fveq2 ⊢ ( 𝑝 = ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) )
88 87 fveq1d ⊢ ( 𝑝 = ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) )
89 49 ringgrpd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → 𝑃 ∈ Grp )
90 4 63 89 43 44 grpcld ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ∈ 𝑈 )
91 fvexd ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) ∈ V )
92 8 88 90 91 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝑂 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) ‘ 𝑋 ) )
93 56 60 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( ( 𝐹 ‘ 𝑞 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) = ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝑋 ) ( +g ‘ 𝑅 ) ( ( 𝑂 ‘ 𝑟 ) ‘ 𝑋 ) ) )
94 86 92 93 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑞 ∈ 𝑈 ∧ 𝑟 ∈ 𝑈 ) ) → ( 𝐹 ‘ ( 𝑞 ( +g ‘ 𝑃 ) 𝑟 ) ) = ( ( 𝐹 ‘ 𝑞 ) ( +g ‘ 𝑅 ) ( 𝐹 ‘ 𝑟 ) ) )
95 4 9 10 11 12 18 19 40 62 3 63 64 85 94 isrhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑅 ) )