evls1fn

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

Step	Hyp	Ref	Expression
1		evls1fn.o	$⊢ O = R {evalSub}_{1} S$
2		evls1fn.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
3		evls1fn.u	$⊢ U = {Base}_{P}$
4		evls1fn.1	$⊢ φ \to R \in CRing$
5		evls1fn.2	$⊢ φ \to S \in SubRing (R)$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7		eqid	$⊢ R ↑_{𝑠} {Base}_{R} = R ↑_{𝑠} {Base}_{R}$
8		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
9	1 6 7 8 2	evls1rhm	$⊢ (R \in CRing \land S \in SubRing (R)) \to O \in (P RingHom (R ↑_{𝑠} {Base}_{R}))$
10	4 5 9	syl2anc	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} {Base}_{R}))$
11		eqid	$⊢ {Base}_{(R ↑_{𝑠} {Base}_{R})} = {Base}_{(R ↑_{𝑠} {Base}_{R})}$
12	3 11	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} {Base}_{R})) \to O : U ⟶ {Base}_{(R ↑_{𝑠} {Base}_{R})}$
13	10 12	syl	$⊢ φ \to O : U ⟶ {Base}_{(R ↑_{𝑠} {Base}_{R})}$
14	13	ffnd	$⊢ φ \to O Fn U$

Metamath Proof Explorer