Metamath Proof Explorer


Theorem ismhp3

Description: A polynomial is homogeneous iff the degree of every nonzero term is the same. (Contributed by SN, 22-Jul-2024)

Ref Expression
Hypotheses mhpfval.h H=ImHomPR
mhpfval.p P=ImPolyR
mhpfval.b B=BaseP
mhpfval.0 0˙=0R
mhpfval.d D=h0I|h-1Fin
mhpfval.i φIV
mhpfval.r φRW
mhpval.n φN0
ismhp2.1 φXB
Assertion ismhp3 φXHNdDXd0˙fld𝑠0d=N

Proof

Step Hyp Ref Expression
1 mhpfval.h H=ImHomPR
2 mhpfval.p P=ImPolyR
3 mhpfval.b B=BaseP
4 mhpfval.0 0˙=0R
5 mhpfval.d D=h0I|h-1Fin
6 mhpfval.i φIV
7 mhpfval.r φRW
8 mhpval.n φN0
9 ismhp2.1 φXB
10 1 2 3 4 5 6 7 8 ismhp φXHNXBXsupp0˙gD|fld𝑠0g=N
11 9 biantrurd φXsupp0˙gD|fld𝑠0g=NXBXsupp0˙gD|fld𝑠0g=N
12 eqid BaseR=BaseR
13 2 12 3 5 9 mplelf φX:DBaseR
14 13 ffnd φXFnD
15 4 fvexi 0˙V
16 15 a1i φ0˙V
17 elsuppfng XFnDXB0˙Vdsupp0˙XdDXd0˙
18 14 9 16 17 syl3anc φdsupp0˙XdDXd0˙
19 oveq2 g=dfld𝑠0g=fld𝑠0d
20 19 eqeq1d g=dfld𝑠0g=Nfld𝑠0d=N
21 20 elrab dgD|fld𝑠0g=NdDfld𝑠0d=N
22 21 a1i φdgD|fld𝑠0g=NdDfld𝑠0d=N
23 18 22 imbi12d φdsupp0˙XdgD|fld𝑠0g=NdDXd0˙dDfld𝑠0d=N
24 imdistan dDXd0˙fld𝑠0d=NdDXd0˙dDfld𝑠0d=N
25 23 24 bitr4di φdsupp0˙XdgD|fld𝑠0g=NdDXd0˙fld𝑠0d=N
26 25 albidv φddsupp0˙XdgD|fld𝑠0g=NddDXd0˙fld𝑠0d=N
27 dfss2 Xsupp0˙gD|fld𝑠0g=Nddsupp0˙XdgD|fld𝑠0g=N
28 df-ral dDXd0˙fld𝑠0d=NddDXd0˙fld𝑠0d=N
29 26 27 28 3bitr4g φXsupp0˙gD|fld𝑠0g=NdDXd0˙fld𝑠0d=N
30 10 11 29 3bitr2d φXHNdDXd0˙fld𝑠0d=N