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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐷 ‘ 𝐹 ) < 𝑁 ) ) )