ply1sclf1

Description: The polynomial scalar function is injective. (Contributed by Stefan O'Rear, 28-Mar-2015)

Step	Hyp	Ref	Expression
1		ply1scl.p	$⊢ P = {Poly}_{1} (R)$
2		ply1scl.a	$⊢ A = algSc (P)$
3		ply1sclid.k	$⊢ K = {Base}_{R}$
4		ply1sclf1.b	$⊢ B = {Base}_{P}$
5	1 2 3 4	ply1sclf	$⊢ R \in Ring \to A : K ⟶ B$
6		fveq2	$⊢ A (x) = A (y) \to {coe}_{1} (A (x)) = {coe}_{1} (A (y))$
7	6	fveq1d	$⊢ A (x) = A (y) \to {coe}_{1} (A (x)) (0) = {coe}_{1} (A (y)) (0)$
8	1 2 3	ply1sclid	$⊢ (R \in Ring \land x \in K) \to x = {coe}_{1} (A (x)) (0)$
9	8	adantrr	$⊢ (R \in Ring \land (x \in K \land y \in K)) \to x = {coe}_{1} (A (x)) (0)$
10	1 2 3	ply1sclid	$⊢ (R \in Ring \land y \in K) \to y = {coe}_{1} (A (y)) (0)$
11	10	adantrl	$⊢ (R \in Ring \land (x \in K \land y \in K)) \to y = {coe}_{1} (A (y)) (0)$
12	9 11	eqeq12d	$⊢ (R \in Ring \land (x \in K \land y \in K)) \to (x = y \leftrightarrow {coe}_{1} (A (x)) (0) = {coe}_{1} (A (y)) (0))$
13	7 12	imbitrrid	$⊢ (R \in Ring \land (x \in K \land y \in K)) \to (A (x) = A (y) \to x = y)$
14	13	ralrimivva	$⊢ R \in Ring \to \forall x \in K \forall y \in K (A (x) = A (y) \to x = y)$
15		dff13	$⊢ A : K \underset{1-1}{⟶} B \leftrightarrow (A : K ⟶ B \land \forall x \in K \forall y \in K (A (x) = A (y) \to x = y))$
16	5 14 15	sylanbrc	$⊢ R \in Ring \to A : K \underset{1-1}{⟶} B$

Metamath Proof Explorer