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 | ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ) |