ply1sclid

Description: Recover the base scalar from a scalar polynomial. (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		eqid	$⊢ 0_{R} = 0_{R}$
5	1 2 3 4	coe1scl	$⊢ (R \in Ring \land X \in K) \to {coe}_{1} (A (X)) = (x \in ℕ_{0} ⟼ if (x = 0, X, 0_{R}))$
6	5	fveq1d	$⊢ (R \in Ring \land X \in K) \to {coe}_{1} (A (X)) (0) = (x \in ℕ_{0} ⟼ if (x = 0, X, 0_{R})) (0)$
7		0nn0	$⊢ 0 \in ℕ_{0}$
8		iftrue	$⊢ x = 0 \to if (x = 0, X, 0_{R}) = X$
9		eqid	$⊢ (x \in ℕ_{0} ⟼ if (x = 0, X, 0_{R})) = (x \in ℕ_{0} ⟼ if (x = 0, X, 0_{R}))$
10	8 9	fvmptg	$⊢ (0 \in ℕ_{0} \land X \in K) \to (x \in ℕ_{0} ⟼ if (x = 0, X, 0_{R})) (0) = X$
11	7 10	mpan	$⊢ X \in K \to (x \in ℕ_{0} ⟼ if (x = 0, X, 0_{R})) (0) = X$
12	11	adantl	$⊢ (R \in Ring \land X \in K) \to (x \in ℕ_{0} ⟼ if (x = 0, X, 0_{R})) (0) = X$
13	6 12	eqtr2d	$⊢ (R \in Ring \land X \in K) \to X = {coe}_{1} (A (X)) (0)$

Metamath Proof Explorer