Metamath Proof Explorer


Theorem fply1

Description: Conditions for a function to be a univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023)

Ref Expression
Hypotheses fply1.1 0˙=0R
fply1.2 B=BaseR
fply1.3 P=BasePoly1R
fply1.4 φF:01𝑜B
fply1.5 φfinSupp0˙F
Assertion fply1 φFP

Proof

Step Hyp Ref Expression
1 fply1.1 0˙=0R
2 fply1.2 B=BaseR
3 fply1.3 P=BasePoly1R
4 fply1.4 φF:01𝑜B
5 fply1.5 φfinSupp0˙F
6 2 fvexi BV
7 ovex 01𝑜V
8 6 7 elmap FB01𝑜F:01𝑜B
9 4 8 sylibr φFB01𝑜
10 df1o2 1𝑜=
11 snfi Fin
12 10 11 eqeltri 1𝑜Fin
13 12 a1i f01𝑜1𝑜Fin
14 elmapi f01𝑜f:1𝑜0
15 13 14 fisuppfi f01𝑜f-1Fin
16 15 rabeqc f01𝑜|f-1Fin=01𝑜
17 16 oveq2i Bf01𝑜|f-1Fin=B01𝑜
18 9 17 eleqtrrdi φFBf01𝑜|f-1Fin
19 eqid 1𝑜mPwSerR=1𝑜mPwSerR
20 eqid f01𝑜|f-1Fin=f01𝑜|f-1Fin
21 eqid Base1𝑜mPwSerR=Base1𝑜mPwSerR
22 1oex 1𝑜V
23 22 a1i φ1𝑜V
24 19 2 20 21 23 psrbas φBase1𝑜mPwSerR=Bf01𝑜|f-1Fin
25 18 24 eleqtrrd φFBase1𝑜mPwSerR
26 eqid 1𝑜mPolyR=1𝑜mPolyR
27 eqid Poly1R=Poly1R
28 eqid PwSer1R=PwSer1R
29 27 28 3 ply1bas P=Base1𝑜mPolyR
30 26 19 21 1 29 mplelbas FPFBase1𝑜mPwSerRfinSupp0˙F
31 25 5 30 sylanbrc φFP