Theorem ply1degleel

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

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

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	19	adantr	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → 𝑁 ∈ ℝ )
38	37	mnfltd	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → -∞ < 𝑁 )
39	36 38	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐹 ) < 𝑁 )
40		pm5.1	⊢ ( ( 𝐹 ∈ 𝑆 ∧ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
41	28 33 39 40	syl12anc	⊢ ( ( 𝜑 ∧ 𝐹 = ( 0g ‘ 𝑃 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
42	3	eleq2i	⊢ ( 𝐹 ∈ 𝑆 ↔ 𝐹 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) )
43	10	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → 𝐷 Fn 𝐵 )
44		elpreima	⊢ ( 𝐷 Fn 𝐵 → ( 𝐹 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ) ) )
45	43 44	syl	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐹 ∈ ( ◡ 𝐷 “ ( -∞ [,) 𝑁 ) ) ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ) ) )
46	42 45	bitrid	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ) ) )
47	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝑅 ∈ Ring )
48		simpr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
49		simplr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝐹 ≠ ( 0g ‘ 𝑃 ) )
50	2 1 12 6	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
51	47 48 49 50	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
52	51	nn0red	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ )
53	52	rexrd	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℝ* )
54	53	mnfled	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → -∞ ≤ ( 𝐷 ‘ 𝐹 ) )
55	53 54	jca	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ) )
56	20	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → 𝑁 ∈ ℝ* )
57		elico1	⊢ ( ( -∞ ∈ ℝ* ∧ 𝑁 ∈ ℝ* ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
58	17 56 57	sylancr	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
59		df-3an	⊢ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ↔ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) )
60	58 59	bitrdi	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( ( ( 𝐷 ‘ 𝐹 ) ∈ ℝ* ∧ -∞ ≤ ( 𝐷 ‘ 𝐹 ) ) ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
61	55 60	mpbirand	⊢ ( ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) ∧ 𝐹 ∈ 𝐵 ) → ( ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ↔ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) )
62	61	pm5.32da	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) ∈ ( -∞ [,) 𝑁 ) ) ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
63	46 62	bitrd	⊢ ( ( 𝜑 ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )
64	41 63	pm2.61dane	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )