Theorem ply1degltel

Description: Characterize elementhood in the set S of polynomials of degree less than N . (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	ply1degltlss.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1degltlss.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	ply1degltlss.1	⊢ 𝑆 = ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
	ply1degltlss.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	ply1degltlss.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1degltel.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
Assertion	ply1degltel	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1degltlss.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1degltlss.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		ply1degltlss.1	⊢ 𝑆 = ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) )
4		ply1degltlss.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		ply1degltlss.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		ply1degltel.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
7		simpr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → 𝐹 = ( 0g ‘ 𝑃 ) )
8	2 1 6	deg1xrf	⊢ 𝐷 : 𝐵 ⟶ ℝ*
9	8	a1i	⊢ ( 𝜑 → 𝐷 : 𝐵 ⟶ ℝ* )
10	9	ffnd	⊢ ( 𝜑 → 𝐷 Fn 𝐵 )
11	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
13	6 12	ring0cl	⊢ ( 𝑃 ∈ Ring → ( 0g ‘ 𝑃 ) ∈ 𝐵 )
14	5 11 13	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝐵 )
15	2 1 12	deg1z	⊢ ( 𝑅 ∈ Ring → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
16	5 15	syl	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
17		mnfxr	⊢ -∞ ∈ ℝ*
18	17	a1i	⊢ ( 𝜑 → -∞ ∈ ℝ* )
19	4	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
20	19	rexrd	⊢ ( 𝜑 → 𝑁 ∈ ℝ* )
21	18	xrleidd	⊢ ( 𝜑 → -∞ ≤ -∞ )
22	19	mnfltd	⊢ ( 𝜑 → -∞ < 𝑁 )
23	18 20 18 21 22	elicod	⊢ ( 𝜑 → -∞ ∈ ( -∞ [,) 𝑁 ) )
24	16 23	eqeltrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) ∈ ( -∞ [,) 𝑁 ) )
25	10 14 24	elpreimad	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
26	25 3	eleqtrrdi	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝑆 )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 0g ‘ 𝑃 ) ∈ 𝑆 )
28	7 27	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → 𝐹 ∈ 𝑆 )
29		cnvimass	⊢ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ⊆ dom 𝐷
30	3 29	eqsstri	⊢ 𝑆 ⊆ dom 𝐷
31	8	fdmi	⊢ dom 𝐷 = 𝐵
32	30 31	sseqtri	⊢ 𝑆 ⊆ 𝐵
33	32 28	sselid	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → 𝐹 ∈ 𝐵 )
34	7	fveq2d	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) )
35	16	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ ( 0g ‘ 𝑃 ) ) = -∞ )
36	34 35	eqtrd	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐹 ) = -∞ )
37		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
38	19 37	resubcld	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ )
39	38	rexrd	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℝ* )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 𝑁 − 1 ) ∈ ℝ* )
41	40	mnfled	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → -∞ ≤ ( 𝑁 − 1 ) )
42	36 41	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) )
43		pm5.1	⊢ ( ( 𝐹 ∈ 𝑆 ∧ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) ) )
44	28 33 42 43	syl12anc	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) ) )
45	3	eleq2i	⊢ ( 𝐹 ∈ 𝑆 ↔ 𝐹 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
46	10	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → 𝐷 Fn 𝐵 )
47		elpreima	⊢ ( 𝐷 Fn 𝐵 → ( 𝐹 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ) ) )
48	46 47	syl	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐹 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ) ) )
49	45 48	bitrid	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ) ) )
50	17	a1i	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → -∞ ∈ ℝ* )
51	20	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝑁 ∈ ℝ* )
52		elico1	⊢ ( ( -∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
53	50 51 52	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
54		df-3an	⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ↔ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) )
55	53 54	bitrdi	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
56	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝑅 ∈ Ring )
57		simpr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
58		simplr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ≠ ( 0g ‘ 𝑃 ) )
59	2 1 12 6	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
60	56 57 58 59	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
61	60	nn0red	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ )
62	61	rexrd	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
63	62	mnfled	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → -∞ ≤ ( 𝐷 ‘ 𝐹 ) )
64	62 63	jca	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ) )
65	64	biantrurd	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) < 𝑁 ↔ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
66	60	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℤ )
67	4	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
68	67	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝑁 ∈ ℤ )
69		zltlem1	⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐷 ‘ 𝐹 ) < 𝑁 ↔ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) )
70	66 68 69	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) < 𝑁 ↔ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) )
71	55 65 70	3bitr2d	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) )
72	71	pm5.32da	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ) ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) ) )
73	49 72	bitrd	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) ) )
74	44 73	pm2.61dane	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ≤ ( 𝑁 − 1 ) ) ) )