This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = ( 𝐼 mHomP 𝑅 )
ismhp.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
ismhp.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
ismhp.0 ⊢ 0 = ( 0g ‘ 𝑅 )
ismhp.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
ismhp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
ismhp2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion ismhp3 ( 𝜑 → ( 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ↔ ∀ 𝑑 ∈ 𝐷 ( ( 𝑋 ‘ 𝑑 ) ≠ 0 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) )

Proof

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 1 2 3 4 5 6 ismhp ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ) )
9 7 biantrurd ⊢ ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ) )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 2 10 3 5 7 mplelf ⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
12 11 ffnd ⊢ ( 𝜑 → 𝑋 Fn 𝐷 )
13 4 fvexi ⊢ 0 ∈ V
14 13 a1i ⊢ ( 𝜑 → 0 ∈ V )
15 elsuppfng ⊢ ( ( 𝑋 Fn 𝐷 ∧ 𝑋 ∈ 𝐵 ∧ 0 ∈ V ) → ( 𝑑 ∈ ( 𝑋 supp 0 ) ↔ ( 𝑑 ∈ 𝐷 ∧ ( 𝑋 ‘ 𝑑 ) ≠ 0 ) ) )
16 12 7 14 15 syl3anc ⊢ ( 𝜑 → ( 𝑑 ∈ ( 𝑋 supp 0 ) ↔ ( 𝑑 ∈ 𝐷 ∧ ( 𝑋 ‘ 𝑑 ) ≠ 0 ) ) )
17 oveq2 ⊢ ( 𝑔 = 𝑑 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) )
18 17 eqeq1d ⊢ ( 𝑔 = 𝑑 → ( ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 ↔ ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) )
19 18 elrab ⊢ ( 𝑑 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ↔ ( 𝑑 ∈ 𝐷 ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) )
20 19 a1i ⊢ ( 𝜑 → ( 𝑑 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ↔ ( 𝑑 ∈ 𝐷 ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) )
21 16 20 imbi12d ⊢ ( 𝜑 → ( ( 𝑑 ∈ ( 𝑋 supp 0 ) → 𝑑 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ↔ ( ( 𝑑 ∈ 𝐷 ∧ ( 𝑋 ‘ 𝑑 ) ≠ 0 ) → ( 𝑑 ∈ 𝐷 ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) ) )
22 imdistan ⊢ ( ( 𝑑 ∈ 𝐷 → ( ( 𝑋 ‘ 𝑑 ) ≠ 0 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) ↔ ( ( 𝑑 ∈ 𝐷 ∧ ( 𝑋 ‘ 𝑑 ) ≠ 0 ) → ( 𝑑 ∈ 𝐷 ∧ ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) )
23 21 22 bitr4di ⊢ ( 𝜑 → ( ( 𝑑 ∈ ( 𝑋 supp 0 ) → 𝑑 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ↔ ( 𝑑 ∈ 𝐷 → ( ( 𝑋 ‘ 𝑑 ) ≠ 0 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) ) )
24 23 albidv ⊢ ( 𝜑 → ( ∀ 𝑑 ( 𝑑 ∈ ( 𝑋 supp 0 ) → 𝑑 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) ↔ ∀ 𝑑 ( 𝑑 ∈ 𝐷 → ( ( 𝑋 ‘ 𝑑 ) ≠ 0 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) ) )
25 df-ss ⊢ ( ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ↔ ∀ 𝑑 ( 𝑑 ∈ ( 𝑋 supp 0 ) → 𝑑 ∈ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ) )
26 df-ral ⊢ ( ∀ 𝑑 ∈ 𝐷 ( ( 𝑋 ‘ 𝑑 ) ≠ 0 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ↔ ∀ 𝑑 ( 𝑑 ∈ 𝐷 → ( ( 𝑋 ‘ 𝑑 ) ≠ 0 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) )
27 24 25 26 3bitr4g ⊢ ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ { 𝑔 ∈ 𝐷 ∣ ( ( ℂfld ↾s ℕ0 ) Σg 𝑔 ) = 𝑁 } ↔ ∀ 𝑑 ∈ 𝐷 ( ( 𝑋 ‘ 𝑑 ) ≠ 0 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) )
28 8 9 27 3bitr2d ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐻 ‘ 𝑁 ) ↔ ∀ 𝑑 ∈ 𝐷 ( ( 𝑋 ‘ 𝑑 ) ≠ 0 → ( ( ℂfld ↾s ℕ0 ) Σg 𝑑 ) = 𝑁 ) ) )