Metamath Proof Explorer

Theorem mdegnn0cl

Description: Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)

		Ref	Expression
	Hypotheses	mdeg0.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
		mdeg0.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
		mdeg0.z	⊢ 0 = ( 0_g ‘ 𝑃 )
		mdegnn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	Assertion	mdegnn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ₀ )

Proof

Step	Hyp	Ref	Expression
1		mdeg0.d	⊢ 𝐷 = ( 𝐼 mDeg 𝑅 )
2		mdeg0.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mdeg0.z	⊢ 0 = ( 0_g ‘ 𝑃 )
4		mdegnn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		eqid	⊢ ( 0_g ‘ 𝑅 ) = ( 0_g ‘ 𝑅 )
6		eqid	⊢ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } = { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin }
7		eqid	⊢ ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) = ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) )
8	1 2 4 5 6 7 3	mdegldg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ∃ 𝑥 ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ( ( 𝐹 ‘ 𝑥 ) ≠ ( 0_g ‘ 𝑅 ) ∧ ( ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) )
9	6 7	tdeglem1	⊢ ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) : { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ⟶ ℕ₀
10	9	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) : { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ⟶ ℕ₀ )
11	10	ffvelrnda	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑥 ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ) → ( ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) ‘ 𝑥 ) ∈ ℕ₀ )
12		eleq1	⊢ ( ( ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) → ( ( ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) ‘ 𝑥 ) ∈ ℕ₀ ↔ ( 𝐷 ‘ 𝐹 ) ∈ ℕ₀ ) )
13	11 12	syl5ibcom	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑥 ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ) → ( ( ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ₀ ) )
14	13	adantld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑥 ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ) → ( ( ( 𝐹 ‘ 𝑥 ) ≠ ( 0_g ‘ 𝑅 ) ∧ ( ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ₀ ) )
15	14	rexlimdva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑥 ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ( ( 𝐹 ‘ 𝑥 ) ≠ ( 0_g ‘ 𝑅 ) ∧ ( ( ℎ ∈ { 𝑚 ∈ ( ℕ₀ ↑_m 𝐼 ) ∣ ( ^◡ 𝑚 “ ℕ ) ∈ Fin } ↦ ( ℂ_fld Σ_g ℎ ) ) ‘ 𝑥 ) = ( 𝐷 ‘ 𝐹 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ₀ ) )
16	8 15	mpd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ₀ )