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 ) = -∞ )