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 ismhp.h H = I mHomP R
ismhp.p P = I mPoly R
ismhp.b B = Base P
ismhp.0 0 ˙ = 0 R
ismhp.d D = h 0 I | h -1 Fin
ismhp.n φ N 0
ismhp2.1 φ X B
Assertion ismhp3 φ X H N d D X d 0 ˙ fld 𝑠 0 d = N

Proof

Step Hyp Ref Expression
1 ismhp.h H = I mHomP R
2 ismhp.p P = I mPoly R
3 ismhp.b B = Base P
4 ismhp.0 0 ˙ = 0 R
5 ismhp.d D = h 0 I | h -1 Fin
6 ismhp.n φ N 0
7 ismhp2.1 φ X B
8 1 2 3 4 5 6 ismhp φ X H N X B X supp 0 ˙ g D | fld 𝑠 0 g = N
9 7 biantrurd φ X supp 0 ˙ g D | fld 𝑠 0 g = N X B X supp 0 ˙ g D | fld 𝑠 0 g = N
10 eqid Base R = Base R
11 2 10 3 5 7 mplelf φ X : D Base R
12 11 ffnd φ X Fn D
13 4 fvexi 0 ˙ V
14 13 a1i φ 0 ˙ V
15 elsuppfng X Fn D X B 0 ˙ V d supp 0 ˙ X d D X d 0 ˙
16 12 7 14 15 syl3anc φ d supp 0 ˙ X d D X d 0 ˙
17 oveq2 g = d fld 𝑠 0 g = fld 𝑠 0 d
18 17 eqeq1d g = d fld 𝑠 0 g = N fld 𝑠 0 d = N
19 18 elrab d g D | fld 𝑠 0 g = N d D fld 𝑠 0 d = N
20 19 a1i φ d g D | fld 𝑠 0 g = N d D fld 𝑠 0 d = N
21 16 20 imbi12d φ d supp 0 ˙ X d g D | fld 𝑠 0 g = N d D X d 0 ˙ d D fld 𝑠 0 d = N
22 imdistan d D X d 0 ˙ fld 𝑠 0 d = N d D X d 0 ˙ d D fld 𝑠 0 d = N
23 21 22 bitr4di φ d supp 0 ˙ X d g D | fld 𝑠 0 g = N d D X d 0 ˙ fld 𝑠 0 d = N
24 23 albidv φ d d supp 0 ˙ X d g D | fld 𝑠 0 g = N d d D X d 0 ˙ fld 𝑠 0 d = N
25 df-ss X supp 0 ˙ g D | fld 𝑠 0 g = N d d supp 0 ˙ X d g D | fld 𝑠 0 g = N
26 df-ral d D X d 0 ˙ fld 𝑠 0 d = N d d D X d 0 ˙ fld 𝑠 0 d = N
27 24 25 26 3bitr4g φ X supp 0 ˙ g D | fld 𝑠 0 g = N d D X d 0 ˙ fld 𝑠 0 d = N
28 8 9 27 3bitr2d φ X H N d D X d 0 ˙ fld 𝑠 0 d = N