Metamath Proof Explorer

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 
|- P = ( Poly1 ` R )
ply1degltlss.d 
|- D = ( deg1 ` R )
ply1degltlss.1 
|- S = ( `' D " ( -oo [,) N ) )
ply1degltlss.3 
|- ( ph -> N e. NN0 )
ply1degltlss.2 
|- ( ph -> R e. Ring )
ply1degltel.1 
|- B = ( Base ` P )
Assertion ply1degltel 
|- ( ph -> ( F e. S <-> ( F e. B /\ ( D ` F ) <_ ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 ply1degltlss.p 
 |-  P = ( Poly1 ` R )
2 ply1degltlss.d 
 |-  D = ( deg1 ` R )
3 ply1degltlss.1 
 |-  S = ( `' D " ( -oo [,) N ) )
4 ply1degltlss.3 
 |-  ( ph -> N e. NN0 )
5 ply1degltlss.2 
 |-  ( ph -> R e. Ring )
6 ply1degltel.1 
 |-  B = ( Base ` P )
7 simpr 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> F = ( 0g ` P ) )
8 2 1 6 deg1xrf 
 |-  D : B --> RR*
9 8 a1i 
 |-  ( ph -> D : B --> RR* )
10 9 ffnd 
 |-  ( ph -> D Fn B )
11 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
12 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
13 6 12 ring0cl 
 |-  ( P e. Ring -> ( 0g ` P ) e. B )
14 5 11 13 3syl 
 |-  ( ph -> ( 0g ` P ) e. B )
15 2 1 12 deg1z 
 |-  ( R e. Ring -> ( D ` ( 0g ` P ) ) = -oo )
16 5 15 syl 
 |-  ( ph -> ( D ` ( 0g ` P ) ) = -oo )
17 mnfxr 
 |-  -oo e. RR*
18 17 a1i 
 |-  ( ph -> -oo e. RR* )
19 4 nn0red 
 |-  ( ph -> N e. RR )
20 19 rexrd 
 |-  ( ph -> N e. RR* )
21 18 xrleidd 
 |-  ( ph -> -oo <_ -oo )
22 19 mnfltd 
 |-  ( ph -> -oo < N )
23 18 20 18 21 22 elicod 
 |-  ( ph -> -oo e. ( -oo [,) N ) )
24 16 23 eqeltrd 
 |-  ( ph -> ( D ` ( 0g ` P ) ) e. ( -oo [,) N ) )
25 10 14 24 elpreimad 
 |-  ( ph -> ( 0g ` P ) e. ( `' D " ( -oo [,) N ) ) )
26 25 3 eleqtrrdi 
 |-  ( ph -> ( 0g ` P ) e. S )
27 26 adantr 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( 0g ` P ) e. S )
28 7 27 eqeltrd 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> F e. S )
29 cnvimass 
 |-  ( `' D " ( -oo [,) N ) ) C_ dom D
30 3 29 eqsstri 
 |-  S C_ dom D
31 8 fdmi 
 |-  dom D = B
32 30 31 sseqtri 
 |-  S C_ B
33 32 28 sselid 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> F e. B )
34 7 fveq2d 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( D ` F ) = ( D ` ( 0g ` P ) ) )
35 16 adantr 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( D ` ( 0g ` P ) ) = -oo )
36 34 35 eqtrd 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( D ` F ) = -oo )
37 1red 
 |-  ( ph -> 1 e. RR )
38 19 37 resubcld 
 |-  ( ph -> ( N - 1 ) e. RR )
39 38 rexrd 
 |-  ( ph -> ( N - 1 ) e. RR* )
40 39 adantr 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( N - 1 ) e. RR* )
41 40 mnfled 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> -oo <_ ( N - 1 ) )
42 36 41 eqbrtrd 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( D ` F ) <_ ( N - 1 ) )
43 pm5.1 
 |-  ( ( F e. S /\ ( F e. B /\ ( D ` F ) <_ ( N - 1 ) ) ) -> ( F e. S <-> ( F e. B /\ ( D ` F ) <_ ( N - 1 ) ) ) )
44 28 33 42 43 syl12anc 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( F e. S <-> ( F e. B /\ ( D ` F ) <_ ( N - 1 ) ) ) )
45 3 eleq2i 
 |-  ( F e. S <-> F e. ( `' D " ( -oo [,) N ) ) )
46 10 adantr 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> D Fn B )
47 elpreima 
 |-  ( D Fn B -> ( F e. ( `' D " ( -oo [,) N ) ) <-> ( F e. B /\ ( D ` F ) e. ( -oo [,) N ) ) ) )
48 46 47 syl 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> ( F e. ( `' D " ( -oo [,) N ) ) <-> ( F e. B /\ ( D ` F ) e. ( -oo [,) N ) ) ) )
49 45 48 bitrid 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> ( F e. S <-> ( F e. B /\ ( D ` F ) e. ( -oo [,) N ) ) ) )
50 17 a1i 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> -oo e. RR* )
51 20 ad2antrr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> N e. RR* )
52 elico1 
 |-  ( ( -oo e. RR* /\ N e. RR* ) -> ( ( D ` F ) e. ( -oo [,) N ) <-> ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) /\ ( D ` F ) < N ) ) )
53 50 51 52 syl2anc 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) e. ( -oo [,) N ) <-> ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) /\ ( D ` F ) < N ) ) )
54 df-3an 
 |-  ( ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) /\ ( D ` F ) < N ) <-> ( ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) ) /\ ( D ` F ) < N ) )
55 53 54 bitrdi 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) e. ( -oo [,) N ) <-> ( ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) ) /\ ( D ` F ) < N ) ) )
56 5 ad2antrr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> R e. Ring )
57 simpr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> F e. B )
58 simplr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> F =/= ( 0g ` P ) )
59 2 1 12 6 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= ( 0g ` P ) ) -> ( D ` F ) e. NN0 )
60 56 57 58 59 syl3anc 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( D ` F ) e. NN0 )
61 60 nn0red 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( D ` F ) e. RR )
62 61 rexrd 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( D ` F ) e. RR* )
63 62 mnfled 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> -oo <_ ( D ` F ) )
64 62 63 jca 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) ) )
65 64 biantrurd 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) < N <-> ( ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) ) /\ ( D ` F ) < N ) ) )
66 60 nn0zd 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( D ` F ) e. ZZ )
67 4 nn0zd 
 |-  ( ph -> N e. ZZ )
68 67 ad2antrr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> N e. ZZ )
69 zltlem1 
 |-  ( ( ( D ` F ) e. ZZ /\ N e. ZZ ) -> ( ( D ` F ) < N <-> ( D ` F ) <_ ( N - 1 ) ) )
70 66 68 69 syl2anc 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) < N <-> ( D ` F ) <_ ( N - 1 ) ) )
71 55 65 70 3bitr2d 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) e. ( -oo [,) N ) <-> ( D ` F ) <_ ( N - 1 ) ) )
72 71 pm5.32da 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> ( ( F e. B /\ ( D ` F ) e. ( -oo [,) N ) ) <-> ( F e. B /\ ( D ` F ) <_ ( N - 1 ) ) ) )
73 49 72 bitrd 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> ( F e. S <-> ( F e. B /\ ( D ` F ) <_ ( N - 1 ) ) ) )
74 44 73 pm2.61dane 
 |-  ( ph -> ( F e. S <-> ( F e. B /\ ( D ` F ) <_ ( N - 1 ) ) ) )