evl1scad

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

Step	Hyp	Ref	Expression
1		evl1sca.o	$⊢ O = {eval}_{1} (R)$
2		evl1sca.p	$⊢ P = {Poly}_{1} (R)$
3		evl1sca.b	$⊢ B = {Base}_{R}$
4		evl1sca.a	$⊢ A = algSc (P)$
5		evl1scad.u	$⊢ U = {Base}_{P}$
6		evl1scad.1	$⊢ φ \to R \in CRing$
7		evl1scad.2	$⊢ φ \to X \in B$
8		evl1scad.3	$⊢ φ \to Y \in B$
9		crngring	$⊢ R \in CRing \to R \in Ring$
10	2 4 3 5	ply1sclf	$⊢ R \in Ring \to A : B ⟶ U$
11	6 9 10	3syl	$⊢ φ \to A : B ⟶ U$
12	11 7	ffvelcdmd	$⊢ φ \to A (X) \in U$
13	1 2 3 4	evl1sca	$⊢ (R \in CRing \land X \in B) \to O (A (X)) = B \times \{X\}$
14	6 7 13	syl2anc	$⊢ φ \to O (A (X)) = B \times \{X\}$
15	14	fveq1d	$⊢ φ \to O (A (X)) (Y) = (B \times \{X\}) (Y)$
16		fvconst2g	$⊢ (X \in B \land Y \in B) \to (B \times \{X\}) (Y) = X$
17	7 8 16	syl2anc	$⊢ φ \to (B \times \{X\}) (Y) = X$
18	15 17	eqtrd	$⊢ φ \to O (A (X)) (Y) = X$
19	12 18	jca	$⊢ φ \to (A (X) \in U \land O (A (X)) (Y) = X)$

Metamath Proof Explorer