Description: Deduce a homogeneous polynomial from its properties. (Contributed by SN, 25-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ismhp.h | ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 ) | |
ismhp.p | ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) | ||
ismhp.b | ⊢ 𝐵 = ( Base ‘ 𝑃 ) | ||
ismhp.0 | ⊢ 0 = ( 0g ‘ 𝑅 ) | ||
ismhp.d | ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } | ||
ismhp.n | ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) | ||
ismhp2.1 | ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) | ||
ismhp2.2 | ⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) | ||
Assertion | ismhp2 | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismhp.h | ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 ) | |
2 | ismhp.p | ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 ) | |
3 | ismhp.b | ⊢ 𝐵 = ( Base ‘ 𝑃 ) | |
4 | ismhp.0 | ⊢ 0 = ( 0g ‘ 𝑅 ) | |
5 | ismhp.d | ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin } | |
6 | ismhp.n | ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) | |
7 | ismhp2.1 | ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) | |
8 | ismhp2.2 | ⊢ ( 𝜑 → ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) | |
9 | 1 2 3 4 5 6 | ismhp | ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ) ) |
10 | 7 8 9 | mpbir2and | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ) |