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

Metamath Proof Explorer

Theorem evls1fvf

Description: The subring evaluation function for a univariate polynomial as a function, with domain and codomain. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses evls1fn.o ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
evls1fn.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
evls1fn.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
evls1fn.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evls1fn.2 ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
evls1fvf.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evls1fvf.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
Assertion evls1fvf ( 𝜑 → ( 𝑂 ‘ 𝑄 ) : 𝐵 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 evls1fn.o ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2 evls1fn.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3 evls1fn.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
4 evls1fn.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
5 evls1fn.2 ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
6 evls1fvf.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
7 evls1fvf.q ⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
8 eqid ⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
9 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
10 6 fvexi ⊢ 𝐵 ∈ V
11 10 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
12 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
13 1 6 8 12 2 evls1rhm ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
14 4 5 13 syl2anc ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) )
15 3 9 rhmf ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s 𝐵 ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
16 14 15 syl ⊢ ( 𝜑 → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
17 16 7 ffvelcdmd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑄 ) ∈ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
18 8 6 9 4 11 17 pwselbas ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑄 ) : 𝐵 ⟶ 𝐵 )