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

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