Metamath Proof Explorer

Theorem ply1unit

Description: In a field F , a polynomial C is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit . (Contributed by Thierry Arnoux, 25-Apr-2025)

Ref Expression
Hypotheses ply1asclunit.1 
|- P = ( Poly1 ` F )
ply1asclunit.2 
|- A = ( algSc ` P )
ply1asclunit.3 
|- B = ( Base ` F )
ply1asclunit.4 
|- .0. = ( 0g ` F )
ply1asclunit.5 
|- ( ph -> F e. Field )
ply1unit.d 
|- D = ( deg1 ` F )
ply1unit.f 
|- ( ph -> C e. ( Base ` P ) )
Assertion ply1unit 
|- ( ph -> ( C e. ( Unit ` P ) <-> ( D ` C ) = 0 ) )

Proof

Step Hyp Ref Expression
1 ply1asclunit.1 
 |-  P = ( Poly1 ` F )
2 ply1asclunit.2 
 |-  A = ( algSc ` P )
3 ply1asclunit.3 
 |-  B = ( Base ` F )
4 ply1asclunit.4 
 |-  .0. = ( 0g ` F )
5 ply1asclunit.5 
 |-  ( ph -> F e. Field )
6 ply1unit.d 
 |-  D = ( deg1 ` F )
7 ply1unit.f 
 |-  ( ph -> C e. ( Base ` P ) )
8 5 fldcrngd 
 |-  ( ph -> F e. CRing )
9 8 crngringd 
 |-  ( ph -> F e. Ring )
10 9 adantr 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> F e. Ring )
11 1 ply1ring 
 |-  ( F e. Ring -> P e. Ring )
12 9 11 syl 
 |-  ( ph -> P e. Ring )
13 eqid 
 |-  ( Unit ` P ) = ( Unit ` P )
14 eqid 
 |-  ( invr ` P ) = ( invr ` P )
15 13 14 unitinvcl 
 |-  ( ( P e. Ring /\ C e. ( Unit ` P ) ) -> ( ( invr ` P ) ` C ) e. ( Unit ` P ) )
16 12 15 sylan 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( invr ` P ) ` C ) e. ( Unit ` P ) )
17 eqid 
 |-  ( Base ` P ) = ( Base ` P )
18 17 13 unitcl 
 |-  ( ( ( invr ` P ) ` C ) e. ( Unit ` P ) -> ( ( invr ` P ) ` C ) e. ( Base ` P ) )
19 16 18 syl 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( invr ` P ) ` C ) e. ( Base ` P ) )
20 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
21 5 flddrngd 
 |-  ( ph -> F e. DivRing )
22 drngnzr 
 |-  ( F e. DivRing -> F e. NzRing )
23 1 ply1nz 
 |-  ( F e. NzRing -> P e. NzRing )
24 21 22 23 3syl 
 |-  ( ph -> P e. NzRing )
25 24 adantr 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> P e. NzRing )
26 13 20 25 16 unitnz 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( invr ` P ) ` C ) =/= ( 0g ` P ) )
27 6 1 20 17 deg1nn0cl 
 |-  ( ( F e. Ring /\ ( ( invr ` P ) ` C ) e. ( Base ` P ) /\ ( ( invr ` P ) ` C ) =/= ( 0g ` P ) ) -> ( D ` ( ( invr ` P ) ` C ) ) e. NN0 )
28 10 19 26 27 syl3anc 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( D ` ( ( invr ` P ) ` C ) ) e. NN0 )
29 28 nn0red 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( D ` ( ( invr ` P ) ` C ) ) e. RR )
30 28 nn0ge0d 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> 0 <_ ( D ` ( ( invr ` P ) ` C ) ) )
31 29 30 jca 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( D ` ( ( invr ` P ) ` C ) ) e. RR /\ 0 <_ ( D ` ( ( invr ` P ) ` C ) ) ) )
32 7 adantr 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> C e. ( Base ` P ) )
33 simpr 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> C e. ( Unit ` P ) )
34 13 20 25 33 unitnz 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> C =/= ( 0g ` P ) )
35 6 1 20 17 deg1nn0cl 
 |-  ( ( F e. Ring /\ C e. ( Base ` P ) /\ C =/= ( 0g ` P ) ) -> ( D ` C ) e. NN0 )
36 10 32 34 35 syl3anc 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( D ` C ) e. NN0 )
37 36 nn0red 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( D ` C ) e. RR )
38 36 nn0ge0d 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> 0 <_ ( D ` C ) )
39 eqid 
 |-  ( .r ` P ) = ( .r ` P )
40 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
41 13 14 39 40 unitlinv 
 |-  ( ( P e. Ring /\ C e. ( Unit ` P ) ) -> ( ( ( invr ` P ) ` C ) ( .r ` P ) C ) = ( 1r ` P ) )
42 12 41 sylan 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( ( invr ` P ) ` C ) ( .r ` P ) C ) = ( 1r ` P ) )
43 42 fveq2d 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( D ` ( ( ( invr ` P ) ` C ) ( .r ` P ) C ) ) = ( D ` ( 1r ` P ) ) )
44 eqid 
 |-  ( RLReg ` F ) = ( RLReg ` F )
45 drngdomn 
 |-  ( F e. DivRing -> F e. Domn )
46 21 45 syl 
 |-  ( ph -> F e. Domn )
47 46 adantr 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> F e. Domn )
48 eqid 
 |-  ( coe1 ` ( ( invr ` P ) ` C ) ) = ( coe1 ` ( ( invr ` P ) ` C ) )
49 48 17 1 3 coe1fvalcl 
 |-  ( ( ( ( invr ` P ) ` C ) e. ( Base ` P ) /\ ( D ` ( ( invr ` P ) ` C ) ) e. NN0 ) -> ( ( coe1 ` ( ( invr ` P ) ` C ) ) ` ( D ` ( ( invr ` P ) ` C ) ) ) e. B )
50 19 28 49 syl2anc 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( coe1 ` ( ( invr ` P ) ` C ) ) ` ( D ` ( ( invr ` P ) ` C ) ) ) e. B )
51 6 1 20 17 4 48 deg1ldg 
 |-  ( ( F e. Ring /\ ( ( invr ` P ) ` C ) e. ( Base ` P ) /\ ( ( invr ` P ) ` C ) =/= ( 0g ` P ) ) -> ( ( coe1 ` ( ( invr ` P ) ` C ) ) ` ( D ` ( ( invr ` P ) ` C ) ) ) =/= .0. )
52 10 19 26 51 syl3anc 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( coe1 ` ( ( invr ` P ) ` C ) ) ` ( D ` ( ( invr ` P ) ` C ) ) ) =/= .0. )
53 3 44 4 domnrrg 
 |-  ( ( F e. Domn /\ ( ( coe1 ` ( ( invr ` P ) ` C ) ) ` ( D ` ( ( invr ` P ) ` C ) ) ) e. B /\ ( ( coe1 ` ( ( invr ` P ) ` C ) ) ` ( D ` ( ( invr ` P ) ` C ) ) ) =/= .0. ) -> ( ( coe1 ` ( ( invr ` P ) ` C ) ) ` ( D ` ( ( invr ` P ) ` C ) ) ) e. ( RLReg ` F ) )
54 47 50 52 53 syl3anc 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( coe1 ` ( ( invr ` P ) ` C ) ) ` ( D ` ( ( invr ` P ) ` C ) ) ) e. ( RLReg ` F ) )
55 6 1 44 17 39 20 10 19 26 54 32 34 deg1mul2 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( D ` ( ( ( invr ` P ) ` C ) ( .r ` P ) C ) ) = ( ( D ` ( ( invr ` P ) ` C ) ) + ( D ` C ) ) )
56 eqid 
 |-  ( Monic1p ` F ) = ( Monic1p ` F )
57 1 40 56 6 mon1pid 
 |-  ( F e. NzRing -> ( ( 1r ` P ) e. ( Monic1p ` F ) /\ ( D ` ( 1r ` P ) ) = 0 ) )
58 57 simprd 
 |-  ( F e. NzRing -> ( D ` ( 1r ` P ) ) = 0 )
59 21 22 58 3syl 
 |-  ( ph -> ( D ` ( 1r ` P ) ) = 0 )
60 59 adantr 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( D ` ( 1r ` P ) ) = 0 )
61 43 55 60 3eqtr3d 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( ( D ` ( ( invr ` P ) ` C ) ) + ( D ` C ) ) = 0 )
62 add20 
 |-  ( ( ( ( D ` ( ( invr ` P ) ` C ) ) e. RR /\ 0 <_ ( D ` ( ( invr ` P ) ` C ) ) ) /\ ( ( D ` C ) e. RR /\ 0 <_ ( D ` C ) ) ) -> ( ( ( D ` ( ( invr ` P ) ` C ) ) + ( D ` C ) ) = 0 <-> ( ( D ` ( ( invr ` P ) ` C ) ) = 0 /\ ( D ` C ) = 0 ) ) )
63 62 anassrs 
 |-  ( ( ( ( ( D ` ( ( invr ` P ) ` C ) ) e. RR /\ 0 <_ ( D ` ( ( invr ` P ) ` C ) ) ) /\ ( D ` C ) e. RR ) /\ 0 <_ ( D ` C ) ) -> ( ( ( D ` ( ( invr ` P ) ` C ) ) + ( D ` C ) ) = 0 <-> ( ( D ` ( ( invr ` P ) ` C ) ) = 0 /\ ( D ` C ) = 0 ) ) )
64 63 simplbda 
 |-  ( ( ( ( ( ( D ` ( ( invr ` P ) ` C ) ) e. RR /\ 0 <_ ( D ` ( ( invr ` P ) ` C ) ) ) /\ ( D ` C ) e. RR ) /\ 0 <_ ( D ` C ) ) /\ ( ( D ` ( ( invr ` P ) ` C ) ) + ( D ` C ) ) = 0 ) -> ( D ` C ) = 0 )
65 31 37 38 61 64 syl1111anc 
 |-  ( ( ph /\ C e. ( Unit ` P ) ) -> ( D ` C ) = 0 )
66 9 adantr 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> F e. Ring )
67 7 adantr 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> C e. ( Base ` P ) )
68 6 1 17 deg1xrcl 
 |-  ( C e. ( Base ` P ) -> ( D ` C ) e. RR* )
69 7 68 syl 
 |-  ( ph -> ( D ` C ) e. RR* )
70 0xr 
 |-  0 e. RR*
71 xeqlelt 
 |-  ( ( ( D ` C ) e. RR* /\ 0 e. RR* ) -> ( ( D ` C ) = 0 <-> ( ( D ` C ) <_ 0 /\ -. ( D ` C ) < 0 ) ) )
72 69 70 71 sylancl 
 |-  ( ph -> ( ( D ` C ) = 0 <-> ( ( D ` C ) <_ 0 /\ -. ( D ` C ) < 0 ) ) )
73 72 simprbda 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> ( D ` C ) <_ 0 )
74 6 1 17 2 deg1le0 
 |-  ( ( F e. Ring /\ C e. ( Base ` P ) ) -> ( ( D ` C ) <_ 0 <-> C = ( A ` ( ( coe1 ` C ) ` 0 ) ) ) )
75 74 biimpa 
 |-  ( ( ( F e. Ring /\ C e. ( Base ` P ) ) /\ ( D ` C ) <_ 0 ) -> C = ( A ` ( ( coe1 ` C ) ` 0 ) ) )
76 66 67 73 75 syl21anc 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> C = ( A ` ( ( coe1 ` C ) ` 0 ) ) )
77 5 adantr 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> F e. Field )
78 0nn0 
 |-  0 e. NN0
79 eqid 
 |-  ( coe1 ` C ) = ( coe1 ` C )
80 79 17 1 3 coe1fvalcl 
 |-  ( ( C e. ( Base ` P ) /\ 0 e. NN0 ) -> ( ( coe1 ` C ) ` 0 ) e. B )
81 67 78 80 sylancl 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> ( ( coe1 ` C ) ` 0 ) e. B )
82 simpl 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> ph )
83 72 simplbda 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> -. ( D ` C ) < 0 )
84 6 1 20 17 deg1lt0 
 |-  ( ( F e. Ring /\ C e. ( Base ` P ) ) -> ( ( D ` C ) < 0 <-> C = ( 0g ` P ) ) )
85 84 necon3bbid 
 |-  ( ( F e. Ring /\ C e. ( Base ` P ) ) -> ( -. ( D ` C ) < 0 <-> C =/= ( 0g ` P ) ) )
86 85 biimpa 
 |-  ( ( ( F e. Ring /\ C e. ( Base ` P ) ) /\ -. ( D ` C ) < 0 ) -> C =/= ( 0g ` P ) )
87 66 67 83 86 syl21anc 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> C =/= ( 0g ` P ) )
88 9 adantr 
 |-  ( ( ph /\ ( D ` C ) <_ 0 ) -> F e. Ring )
89 7 adantr 
 |-  ( ( ph /\ ( D ` C ) <_ 0 ) -> C e. ( Base ` P ) )
90 simpr 
 |-  ( ( ph /\ ( D ` C ) <_ 0 ) -> ( D ` C ) <_ 0 )
91 6 1 4 17 20 88 89 90 deg1le0eq0 
 |-  ( ( ph /\ ( D ` C ) <_ 0 ) -> ( C = ( 0g ` P ) <-> ( ( coe1 ` C ) ` 0 ) = .0. ) )
92 91 necon3bid 
 |-  ( ( ph /\ ( D ` C ) <_ 0 ) -> ( C =/= ( 0g ` P ) <-> ( ( coe1 ` C ) ` 0 ) =/= .0. ) )
93 92 biimpa 
 |-  ( ( ( ph /\ ( D ` C ) <_ 0 ) /\ C =/= ( 0g ` P ) ) -> ( ( coe1 ` C ) ` 0 ) =/= .0. )
94 82 73 87 93 syl21anc 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> ( ( coe1 ` C ) ` 0 ) =/= .0. )
95 1 2 3 4 77 81 94 ply1asclunit 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> ( A ` ( ( coe1 ` C ) ` 0 ) ) e. ( Unit ` P ) )
96 76 95 eqeltrd 
 |-  ( ( ph /\ ( D ` C ) = 0 ) -> C e. ( Unit ` P ) )
97 65 96 impbida 
 |-  ( ph -> ( C e. ( Unit ` P ) <-> ( D ` C ) = 0 ) )