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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
ismhp.n ( 𝜑𝑁 ∈ ℕ0 )
ismhp2.1 ( 𝜑𝑋𝐵 )
Assertion ismhp3 ( 𝜑 → ( 𝑋 ∈ ( 𝐻𝑁 ) ↔ ∀ 𝑑𝐷 ( ( 𝑋𝑑 ) ≠ 0 → ( ( ℂflds0 ) Σ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 𝐷 = { ∈ ( ℕ0m 𝐼 ) ∣ ( “ ℕ ) ∈ Fin }
6 ismhp.n ( 𝜑𝑁 ∈ ℕ0 )
7 ismhp2.1 ( 𝜑𝑋𝐵 )
8 1 2 3 4 5 6 ismhp ( 𝜑 → ( 𝑋 ∈ ( 𝐻𝑁 ) ↔ ( 𝑋𝐵 ∧ ( 𝑋 supp 0 ) ⊆ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ) ) )
9 7 biantrurd ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ↔ ( 𝑋𝐵 ∧ ( 𝑋 supp 0 ) ⊆ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σ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 ( 𝑔 = 𝑑 → ( ( ℂflds0 ) Σg 𝑔 ) = ( ( ℂflds0 ) Σg 𝑑 ) )
18 17 eqeq1d ( 𝑔 = 𝑑 → ( ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 ↔ ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) )
19 18 elrab ( 𝑑 ∈ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ↔ ( 𝑑𝐷 ∧ ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) )
20 19 a1i ( 𝜑 → ( 𝑑 ∈ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ↔ ( 𝑑𝐷 ∧ ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) )
21 16 20 imbi12d ( 𝜑 → ( ( 𝑑 ∈ ( 𝑋 supp 0 ) → 𝑑 ∈ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ) ↔ ( ( 𝑑𝐷 ∧ ( 𝑋𝑑 ) ≠ 0 ) → ( 𝑑𝐷 ∧ ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) ) )
22 imdistan ( ( 𝑑𝐷 → ( ( 𝑋𝑑 ) ≠ 0 → ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) ↔ ( ( 𝑑𝐷 ∧ ( 𝑋𝑑 ) ≠ 0 ) → ( 𝑑𝐷 ∧ ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) )
23 21 22 bitr4di ( 𝜑 → ( ( 𝑑 ∈ ( 𝑋 supp 0 ) → 𝑑 ∈ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ) ↔ ( 𝑑𝐷 → ( ( 𝑋𝑑 ) ≠ 0 → ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) ) )
24 23 albidv ( 𝜑 → ( ∀ 𝑑 ( 𝑑 ∈ ( 𝑋 supp 0 ) → 𝑑 ∈ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ) ↔ ∀ 𝑑 ( 𝑑𝐷 → ( ( 𝑋𝑑 ) ≠ 0 → ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) ) )
25 df-ss ( ( 𝑋 supp 0 ) ⊆ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ↔ ∀ 𝑑 ( 𝑑 ∈ ( 𝑋 supp 0 ) → 𝑑 ∈ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ) )
26 df-ral ( ∀ 𝑑𝐷 ( ( 𝑋𝑑 ) ≠ 0 → ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ↔ ∀ 𝑑 ( 𝑑𝐷 → ( ( 𝑋𝑑 ) ≠ 0 → ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) )
27 24 25 26 3bitr4g ( 𝜑 → ( ( 𝑋 supp 0 ) ⊆ { 𝑔𝐷 ∣ ( ( ℂflds0 ) Σg 𝑔 ) = 𝑁 } ↔ ∀ 𝑑𝐷 ( ( 𝑋𝑑 ) ≠ 0 → ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) )
28 8 9 27 3bitr2d ( 𝜑 → ( 𝑋 ∈ ( 𝐻𝑁 ) ↔ ∀ 𝑑𝐷 ( ( 𝑋𝑑 ) ≠ 0 → ( ( ℂflds0 ) Σg 𝑑 ) = 𝑁 ) ) )