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

Metamath Proof Explorer

Theorem evls1maprnss

Description: The function F mapping polynomials p to their subring evaluation at a given point A takes all values in the subring S . (Contributed by Thierry Arnoux, 25-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 evls1maprnss ( 𝜑 → 𝑆 ⊆ ran 𝐹 )

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 ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
10 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) = ( algSc ‘ ( Poly1 ‘ 𝑅 ) )
11 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
12 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
13 9 10 11 2 6 12 subrg1ascl ⊢ ( 𝜑 → ( algSc ‘ 𝑃 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( algSc ‘ 𝑃 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) )
15 14 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) = ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) ‘ 𝑦 ) )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
17 16 fvresd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ↾ 𝑆 ) ‘ 𝑦 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑦 ) )
18 15 17 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) = ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑦 ) )
19 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
20 10 11 9 2 4 19 16 asclply1subcl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( algSc ‘ ( Poly1 ‘ 𝑅 ) ) ‘ 𝑦 ) ∈ 𝑈 )
21 18 20 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ∈ 𝑈 )
22 fveq2 ⊢ ( 𝑝 = ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) )
23 22 fveq1d ⊢ ( 𝑝 = ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) )
24 23 eqeq2d ⊢ ( 𝑝 = ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) → ( 𝑦 = ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ↔ 𝑦 = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) ) )
25 24 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑝 = ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) → ( 𝑦 = ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) ↔ 𝑦 = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) ) )
26 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑅 ∈ CRing )
27 1 2 11 3 12 26 19 16 evls1sca ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) = ( 𝐵 × { 𝑦 } ) )
28 27 fveq1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) = ( ( 𝐵 × { 𝑦 } ) ‘ 𝑋 ) )
29 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
30 vex ⊢ 𝑦 ∈ V
31 30 fvconst2 ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐵 × { 𝑦 } ) ‘ 𝑋 ) = 𝑦 )
32 29 31 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐵 × { 𝑦 } ) ‘ 𝑋 ) = 𝑦 )
33 28 32 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ 𝑋 ) )
34 21 25 33 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ∃ 𝑝 ∈ 𝑈 𝑦 = ( ( 𝑂 ‘ 𝑝 ) ‘ 𝑋 ) )
35 8 34 16 elrnmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ran 𝐹 )
36 35 ex ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ran 𝐹 ) )
37 36 ssrdv ⊢ ( 𝜑 → 𝑆 ⊆ ran 𝐹 )