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

Metamath Proof Explorer

Theorem evls1fn

Description: Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025)

Ref Expression
Hypotheses evls1fn.o ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
evls1fn.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
evls1fn.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
evls1fn.1 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
evls1fn.2 ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
Assertion evls1fn ( 𝜑 → 𝑂 Fn 𝑈 )

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 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) = ( 𝑅 ↑s ( Base ‘ 𝑅 ) )
8 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
9 1 6 7 8 2 evls1rhm ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
10 4 5 9 syl2anc ⊢ ( 𝜑 → 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
11 eqid ⊢ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) = ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) )
12 3 11 rhmf ⊢ ( 𝑂 ∈ ( 𝑃 RingHom ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
13 10 12 syl ⊢ ( 𝜑 → 𝑂 : 𝑈 ⟶ ( Base ‘ ( 𝑅 ↑s ( Base ‘ 𝑅 ) ) ) )
14 13 ffnd ⊢ ( 𝜑 → 𝑂 Fn 𝑈 )