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 
|- 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 ply1degleel 
|- ( ph -> ( F e. S <-> ( F e. B /\ ( D ` F ) < N ) ) )

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 19 adantr 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> N e. RR )
38 37 mnfltd 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> -oo < N )
39 36 38 eqbrtrd 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( D ` F ) < N )
40 pm5.1 
 |-  ( ( F e. S /\ ( F e. B /\ ( D ` F ) < N ) ) -> ( F e. S <-> ( F e. B /\ ( D ` F ) < N ) ) )
41 28 33 39 40 syl12anc 
 |-  ( ( ph /\ F = ( 0g ` P ) ) -> ( F e. S <-> ( F e. B /\ ( D ` F ) < N ) ) )
42 3 eleq2i 
 |-  ( F e. S <-> F e. ( `' D " ( -oo [,) N ) ) )
43 10 adantr 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> D Fn B )
44 elpreima 
 |-  ( D Fn B -> ( F e. ( `' D " ( -oo [,) N ) ) <-> ( F e. B /\ ( D ` F ) e. ( -oo [,) N ) ) ) )
45 43 44 syl 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> ( F e. ( `' D " ( -oo [,) N ) ) <-> ( F e. B /\ ( D ` F ) e. ( -oo [,) N ) ) ) )
46 42 45 bitrid 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> ( F e. S <-> ( F e. B /\ ( D ` F ) e. ( -oo [,) N ) ) ) )
47 5 ad2antrr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> R e. Ring )
48 simpr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> F e. B )
49 simplr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> F =/= ( 0g ` P ) )
50 2 1 12 6 deg1nn0cl 
 |-  ( ( R e. Ring /\ F e. B /\ F =/= ( 0g ` P ) ) -> ( D ` F ) e. NN0 )
51 47 48 49 50 syl3anc 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( D ` F ) e. NN0 )
52 51 nn0red 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( D ` F ) e. RR )
53 52 rexrd 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( D ` F ) e. RR* )
54 53 mnfled 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> -oo <_ ( D ` F ) )
55 53 54 jca 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) ) )
56 20 ad2antrr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> N e. RR* )
57 elico1 
 |-  ( ( -oo e. RR* /\ N e. RR* ) -> ( ( D ` F ) e. ( -oo [,) N ) <-> ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) /\ ( D ` F ) < N ) ) )
58 17 56 57 sylancr 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) e. ( -oo [,) N ) <-> ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) /\ ( D ` F ) < N ) ) )
59 df-3an 
 |-  ( ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) /\ ( D ` F ) < N ) <-> ( ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) ) /\ ( D ` F ) < N ) )
60 58 59 bitrdi 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) e. ( -oo [,) N ) <-> ( ( ( D ` F ) e. RR* /\ -oo <_ ( D ` F ) ) /\ ( D ` F ) < N ) ) )
61 55 60 mpbirand 
 |-  ( ( ( ph /\ F =/= ( 0g ` P ) ) /\ F e. B ) -> ( ( D ` F ) e. ( -oo [,) N ) <-> ( D ` F ) < N ) )
62 61 pm5.32da 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> ( ( F e. B /\ ( D ` F ) e. ( -oo [,) N ) ) <-> ( F e. B /\ ( D ` F ) < N ) ) )
63 46 62 bitrd 
 |-  ( ( ph /\ F =/= ( 0g ` P ) ) -> ( F e. S <-> ( F e. B /\ ( D ` F ) < N ) ) )
64 41 63 pm2.61dane 
 |-  ( ph -> ( F e. S <-> ( F e. B /\ ( D ` F ) < N ) ) )