# Metamath Proof Explorer

## Theorem ply1sclid

Description: Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses ply1scl.p $⊢ P = Poly 1 ⁡ R$
ply1scl.a $⊢ A = algSc ⁡ P$
ply1sclid.k $⊢ K = Base R$
Assertion ply1sclid $⊢ R ∈ Ring ∧ X ∈ K → X = coe 1 ⁡ A ⁡ X ⁡ 0$

### Proof

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 ∈ Ring ∧ X ∈ K → coe 1 ⁡ A ⁡ X = x ∈ ℕ 0 ⟼ if x = 0 X 0 R$
6 5 fveq1d $⊢ R ∈ Ring ∧ X ∈ K → coe 1 ⁡ A ⁡ X ⁡ 0 = x ∈ ℕ 0 ⟼ if x = 0 X 0 R ⁡ 0$
7 0nn0 $⊢ 0 ∈ ℕ 0$
8 iftrue $⊢ x = 0 → if x = 0 X 0 R = X$
9 eqid $⊢ x ∈ ℕ 0 ⟼ if x = 0 X 0 R = x ∈ ℕ 0 ⟼ if x = 0 X 0 R$
10 8 9 fvmptg $⊢ 0 ∈ ℕ 0 ∧ X ∈ K → x ∈ ℕ 0 ⟼ if x = 0 X 0 R ⁡ 0 = X$
11 7 10 mpan $⊢ X ∈ K → x ∈ ℕ 0 ⟼ if x = 0 X 0 R ⁡ 0 = X$
12 11 adantl $⊢ R ∈ Ring ∧ X ∈ K → x ∈ ℕ 0 ⟼ if x = 0 X 0 R ⁡ 0 = X$
13 6 12 eqtr2d $⊢ R ∈ Ring ∧ X ∈ K → X = coe 1 ⁡ A ⁡ X ⁡ 0$