Metamath Proof Explorer


Theorem ismhp

Description: Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023)

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
Assertion ismhp φ X H N X B X supp 0 ˙ g D | fld 𝑠 0 g = 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 reldmmhp Rel dom mHomP
8 id X H N X H N
9 7 1 8 elfvov1 X H N I V
10 7 1 8 elfvov2 X H N R V
11 9 10 jca X H N I V R V
12 11 anim2i φ X H N φ I V R V
13 reldmmpl Rel dom mPoly
14 13 2 3 elbasov X B I V R V
15 14 adantr X B X supp 0 ˙ g D | fld 𝑠 0 g = N I V R V
16 15 anim2i φ X B X supp 0 ˙ g D | fld 𝑠 0 g = N φ I V R V
17 simprl φ I V R V I V
18 simprr φ I V R V R V
19 6 adantr φ I V R V N 0
20 1 2 3 4 5 17 18 19 mhpval φ I V R V H N = f B | f supp 0 ˙ g D | fld 𝑠 0 g = N
21 20 eleq2d φ I V R V X H N X f B | f supp 0 ˙ g D | fld 𝑠 0 g = N
22 oveq1 f = X f supp 0 ˙ = X supp 0 ˙
23 22 sseq1d f = X f supp 0 ˙ g D | fld 𝑠 0 g = N X supp 0 ˙ g D | fld 𝑠 0 g = N
24 23 elrab X f B | f supp 0 ˙ g D | fld 𝑠 0 g = N X B X supp 0 ˙ g D | fld 𝑠 0 g = N
25 21 24 bitrdi φ I V R V X H N X B X supp 0 ˙ g D | fld 𝑠 0 g = N
26 12 16 25 pm5.21nd φ X H N X B X supp 0 ˙ g D | fld 𝑠 0 g = N