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