Metamath Proof Explorer


Theorem plyconst

Description: A constant function is a polynomial. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plyconst S A S × A Poly S

Proof

Step Hyp Ref Expression
1 exp0 z z 0 = 1
2 1 adantl S A S z z 0 = 1
3 2 oveq2d S A S z A z 0 = A 1
4 ssel2 S A S A
5 4 adantr S A S z A
6 5 mulid1d S A S z A 1 = A
7 3 6 eqtrd S A S z A z 0 = A
8 7 mpteq2dva S A S z A z 0 = z A
9 fconstmpt × A = z A
10 8 9 eqtr4di S A S z A z 0 = × A
11 0nn0 0 0
12 eqid z A z 0 = z A z 0
13 12 ply1term S A S 0 0 z A z 0 Poly S
14 11 13 mp3an3 S A S z A z 0 Poly S
15 10 14 eqeltrrd S A S × A Poly S