evl1vard

Description: Polynomial evaluation builder for the variable. (Contributed by Mario Carneiro, 4-Jul-2015)

Step	Hyp	Ref	Expression
1		evl1var.q	$⊢ O = {eval}_{1} (R)$
2		evl1var.v	$⊢ X = {var}_{1} (R)$
3		evl1var.b	$⊢ B = {Base}_{R}$
4		evl1vard.p	$⊢ P = {Poly}_{1} (R)$
5		evl1vard.u	$⊢ U = {Base}_{P}$
6		evl1vard.1	$⊢ φ \to R \in CRing$
7		evl1vard.2	$⊢ φ \to Y \in B$
8		crngring	$⊢ R \in CRing \to R \in Ring$
9	2 4 5	vr1cl	$⊢ R \in Ring \to X \in U$
10	6 8 9	3syl	$⊢ φ \to X \in U$
11	1 2 3	evl1var	$⊢ R \in CRing \to O (X) = {I ↾}_{B}$
12	6 11	syl	$⊢ φ \to O (X) = {I ↾}_{B}$
13	12	fveq1d	$⊢ φ \to O (X) (Y) = ({I ↾}_{B}) (Y)$
14		fvresi	$⊢ Y \in B \to ({I ↾}_{B}) (Y) = Y$
15	7 14	syl	$⊢ φ \to ({I ↾}_{B}) (Y) = Y$
16	13 15	eqtrd	$⊢ φ \to O (X) (Y) = Y$
17	10 16	jca	$⊢ φ \to (X \in U \land O (X) (Y) = Y)$

Metamath Proof Explorer