Metamath Proof Explorer


Theorem mdeg0

Description: Degree of the zero polynomial. (Contributed by Stefan O'Rear, 20-Mar-2015) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses mdeg0.d 𝐷 = ( 𝐼 mDeg 𝑅 )
mdeg0.p 𝑃 = ( 𝐼 mPoly 𝑅 )
mdeg0.z 0 = ( 0g𝑃 )
Assertion mdeg0 ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( 𝐷0 ) = -∞ )

Proof

Step Hyp Ref Expression
1 mdeg0.d 𝐷 = ( 𝐼 mDeg 𝑅 )
2 mdeg0.p 𝑃 = ( 𝐼 mPoly 𝑅 )
3 mdeg0.z 0 = ( 0g𝑃 )
4 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
5 2 mplgrp ( ( 𝐼𝑉𝑅 ∈ Grp ) → 𝑃 ∈ Grp )
6 4 5 sylan2 ( ( 𝐼𝑉𝑅 ∈ Ring ) → 𝑃 ∈ Grp )
7 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
8 7 3 grpidcl ( 𝑃 ∈ Grp → 0 ∈ ( Base ‘ 𝑃 ) )
9 eqid ( 0g𝑅 ) = ( 0g𝑅 )
10 eqid { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } = { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin }
11 eqid ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) = ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) )
12 1 2 7 9 10 11 mdegval ( 0 ∈ ( Base ‘ 𝑃 ) → ( 𝐷0 ) = sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 0 supp ( 0g𝑅 ) ) ) , ℝ* , < ) )
13 6 8 12 3syl ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( 𝐷0 ) = sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 0 supp ( 0g𝑅 ) ) ) , ℝ* , < ) )
14 simpl ( ( 𝐼𝑉𝑅 ∈ Ring ) → 𝐼𝑉 )
15 4 adantl ( ( 𝐼𝑉𝑅 ∈ Ring ) → 𝑅 ∈ Grp )
16 2 10 9 3 14 15 mpl0 ( ( 𝐼𝑉𝑅 ∈ Ring ) → 0 = ( { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } × { ( 0g𝑅 ) } ) )
17 fvex ( 0g𝑅 ) ∈ V
18 fnconstg ( ( 0g𝑅 ) ∈ V → ( { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } × { ( 0g𝑅 ) } ) Fn { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } )
19 17 18 mp1i ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } × { ( 0g𝑅 ) } ) Fn { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } )
20 16 fneq1d ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( 0 Fn { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↔ ( { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } × { ( 0g𝑅 ) } ) Fn { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ) )
21 19 20 mpbird ( ( 𝐼𝑉𝑅 ∈ Ring ) → 0 Fn { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } )
22 ovex ( ℕ0m 𝐼 ) ∈ V
23 22 rabex { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ∈ V
24 23 a1i ( ( 𝐼𝑉𝑅 ∈ Ring ) → { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ∈ V )
25 17 a1i ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( 0g𝑅 ) ∈ V )
26 fnsuppeq0 ( ( 0 Fn { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ∧ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ∈ V ∧ ( 0g𝑅 ) ∈ V ) → ( ( 0 supp ( 0g𝑅 ) ) = ∅ ↔ 0 = ( { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } × { ( 0g𝑅 ) } ) ) )
27 21 24 25 26 syl3anc ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( ( 0 supp ( 0g𝑅 ) ) = ∅ ↔ 0 = ( { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } × { ( 0g𝑅 ) } ) ) )
28 16 27 mpbird ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( 0 supp ( 0g𝑅 ) ) = ∅ )
29 28 imaeq2d ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 0 supp ( 0g𝑅 ) ) ) = ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ∅ ) )
30 ima0 ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ∅ ) = ∅
31 29 30 eqtrdi ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 0 supp ( 0g𝑅 ) ) ) = ∅ )
32 31 supeq1d ( ( 𝐼𝑉𝑅 ∈ Ring ) → sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 0 supp ( 0g𝑅 ) ) ) , ℝ* , < ) = sup ( ∅ , ℝ* , < ) )
33 xrsup0 sup ( ∅ , ℝ* , < ) = -∞
34 32 33 eqtrdi ( ( 𝐼𝑉𝑅 ∈ Ring ) → sup ( ( ( 𝑦 ∈ { 𝑥 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑥 “ ℕ ) ∈ Fin } ↦ ( ℂfld Σg 𝑦 ) ) “ ( 0 supp ( 0g𝑅 ) ) ) , ℝ* , < ) = -∞ )
35 13 34 eqtrd ( ( 𝐼𝑉𝑅 ∈ Ring ) → ( 𝐷0 ) = -∞ )