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	$⊢ O = R {evalSub}_{1} S$
		evls1fn.p	$⊢ P = {Poly}_{1} (R ↾_{𝑠} S)$
		evls1fn.u	$⊢ U = {Base}_{P}$
		evls1fn.1	$⊢ φ \to R \in CRing$
		evls1fn.2	$⊢ φ \to S \in SubRing (R)$
		evls1fvf.b	$⊢ B = {Base}_{R}$
		evls1fvf.q	$⊢ φ \to Q \in U$
	Assertion	evls1fvf	$⊢ φ \to O (Q) : B ⟶ B$

Proof

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		evls1fvf.b	$⊢ B = {Base}_{R}$
7		evls1fvf.q	$⊢ φ \to Q \in U$
8		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
9		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
10	6	fvexi	$⊢ B \in V$
11	10	a1i	$⊢ φ \to B \in V$
12		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
13	1 6 8 12 2	evls1rhm	$⊢ (R \in CRing \land S \in SubRing (R)) \to O \in (P RingHom (R ↑_{𝑠} B))$
14	4 5 13	syl2anc	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} B))$
15	3 9	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} B)) \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
16	14 15	syl	$⊢ φ \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
17	16 7	ffvelcdmd	$⊢ φ \to O (Q) \in {Base}_{(R ↑_{𝑠} B)}$
18	8 6 9 4 11 17	pwselbas	$⊢ φ \to O (Q) : B ⟶ B$