Metamath Proof Explorer

Theorem uc1pmon1p

Description: Make a unitic polynomial monic by multiplying a factor to normalize the leading coefficient. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses uc1pmon1p.c 
|- C = ( Unic1p ` R )
uc1pmon1p.m 
|- M = ( Monic1p ` R )
uc1pmon1p.p 
|- P = ( Poly1 ` R )
uc1pmon1p.t 
|- .x. = ( .r ` P )
uc1pmon1p.a 
|- A = ( algSc ` P )
uc1pmon1p.d 
|- D = ( deg1 ` R )
uc1pmon1p.i 
|- I = ( invr ` R )
Assertion uc1pmon1p 
|- ( ( R e. Ring /\ X e. C ) -> ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. M )

Proof

Step Hyp Ref Expression
1 uc1pmon1p.c 
 |-  C = ( Unic1p ` R )
2 uc1pmon1p.m 
 |-  M = ( Monic1p ` R )
3 uc1pmon1p.p 
 |-  P = ( Poly1 ` R )
4 uc1pmon1p.t 
 |-  .x. = ( .r ` P )
5 uc1pmon1p.a 
 |-  A = ( algSc ` P )
6 uc1pmon1p.d 
 |-  D = ( deg1 ` R )
7 uc1pmon1p.i 
 |-  I = ( invr ` R )
8 3 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
9 8 adantr 
 |-  ( ( R e. Ring /\ X e. C ) -> P e. Ring )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 eqid 
 |-  ( Base ` P ) = ( Base ` P )
12 3 5 10 11 ply1sclf 
 |-  ( R e. Ring -> A : ( Base ` R ) --> ( Base ` P ) )
13 12 adantr 
 |-  ( ( R e. Ring /\ X e. C ) -> A : ( Base ` R ) --> ( Base ` P ) )
14 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
15 6 14 1 uc1pldg 
 |-  ( X e. C -> ( ( coe1 ` X ) ` ( D ` X ) ) e. ( Unit ` R ) )
16 14 7 10 ringinvcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` X ) ` ( D ` X ) ) e. ( Unit ` R ) ) -> ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) e. ( Base ` R ) )
17 15 16 sylan2 
 |-  ( ( R e. Ring /\ X e. C ) -> ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) e. ( Base ` R ) )
18 13 17 ffvelrnd 
 |-  ( ( R e. Ring /\ X e. C ) -> ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) e. ( Base ` P ) )
19 3 11 1 uc1pcl 
 |-  ( X e. C -> X e. ( Base ` P ) )
20 19 adantl 
 |-  ( ( R e. Ring /\ X e. C ) -> X e. ( Base ` P ) )
21 11 4 ringcl 
 |-  ( ( P e. Ring /\ ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) e. ( Base ` P ) /\ X e. ( Base ` P ) ) -> ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. ( Base ` P ) )
22 9 18 20 21 syl3anc 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. ( Base ` P ) )
23 simpl 
 |-  ( ( R e. Ring /\ X e. C ) -> R e. Ring )
24 eqid 
 |-  ( RLReg ` R ) = ( RLReg ` R )
25 24 14 unitrrg 
 |-  ( R e. Ring -> ( Unit ` R ) C_ ( RLReg ` R ) )
26 25 adantr 
 |-  ( ( R e. Ring /\ X e. C ) -> ( Unit ` R ) C_ ( RLReg ` R ) )
27 14 7 unitinvcl 
 |-  ( ( R e. Ring /\ ( ( coe1 ` X ) ` ( D ` X ) ) e. ( Unit ` R ) ) -> ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) e. ( Unit ` R ) )
28 15 27 sylan2 
 |-  ( ( R e. Ring /\ X e. C ) -> ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) e. ( Unit ` R ) )
29 26 28 sseldd 
 |-  ( ( R e. Ring /\ X e. C ) -> ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) e. ( RLReg ` R ) )
30 6 3 24 11 4 5 deg1mul3 
 |-  ( ( R e. Ring /\ ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) e. ( RLReg ` R ) /\ X e. ( Base ` P ) ) -> ( D ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) = ( D ` X ) )
31 23 29 20 30 syl3anc 
 |-  ( ( R e. Ring /\ X e. C ) -> ( D ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) = ( D ` X ) )
32 6 1 uc1pdeg 
 |-  ( ( R e. Ring /\ X e. C ) -> ( D ` X ) e. NN0 )
33 31 32 eqeltrd 
 |-  ( ( R e. Ring /\ X e. C ) -> ( D ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) e. NN0 )
34 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
35 6 3 34 11 deg1nn0clb 
 |-  ( ( R e. Ring /\ ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. ( Base ` P ) ) -> ( ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) =/= ( 0g ` P ) <-> ( D ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) e. NN0 ) )
36 22 35 syldan 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) =/= ( 0g ` P ) <-> ( D ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) e. NN0 ) )
37 33 36 mpbird 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) =/= ( 0g ` P ) )
38 31 fveq2d 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( coe1 ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) ` ( D ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) ) = ( ( coe1 ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) ` ( D ` X ) ) )
39 eqid 
 |-  ( .r ` R ) = ( .r ` R )
40 3 11 10 5 4 39 coe1sclmul 
 |-  ( ( R e. Ring /\ ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) e. ( Base ` R ) /\ X e. ( Base ` P ) ) -> ( coe1 ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) = ( ( NN0 X. { ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) } ) oF ( .r ` R ) ( coe1 ` X ) ) )
41 23 17 20 40 syl3anc 
 |-  ( ( R e. Ring /\ X e. C ) -> ( coe1 ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) = ( ( NN0 X. { ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) } ) oF ( .r ` R ) ( coe1 ` X ) ) )
42 41 fveq1d 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( coe1 ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) ` ( D ` X ) ) = ( ( ( NN0 X. { ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) } ) oF ( .r ` R ) ( coe1 ` X ) ) ` ( D ` X ) ) )
43 nn0ex 
 |-  NN0 e. _V
44 43 a1i 
 |-  ( ( R e. Ring /\ X e. C ) -> NN0 e. _V )
45 fvexd 
 |-  ( ( R e. Ring /\ X e. C ) -> ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) e. _V )
46 eqid 
 |-  ( coe1 ` X ) = ( coe1 ` X )
47 46 11 3 10 coe1f 
 |-  ( X e. ( Base ` P ) -> ( coe1 ` X ) : NN0 --> ( Base ` R ) )
48 ffn 
 |-  ( ( coe1 ` X ) : NN0 --> ( Base ` R ) -> ( coe1 ` X ) Fn NN0 )
49 20 47 48 3syl 
 |-  ( ( R e. Ring /\ X e. C ) -> ( coe1 ` X ) Fn NN0 )
50 eqidd 
 |-  ( ( ( R e. Ring /\ X e. C ) /\ ( D ` X ) e. NN0 ) -> ( ( coe1 ` X ) ` ( D ` X ) ) = ( ( coe1 ` X ) ` ( D ` X ) ) )
51 44 45 49 50 ofc1 
 |-  ( ( ( R e. Ring /\ X e. C ) /\ ( D ` X ) e. NN0 ) -> ( ( ( NN0 X. { ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) } ) oF ( .r ` R ) ( coe1 ` X ) ) ` ( D ` X ) ) = ( ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ( .r ` R ) ( ( coe1 ` X ) ` ( D ` X ) ) ) )
52 32 51 mpdan 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( ( NN0 X. { ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) } ) oF ( .r ` R ) ( coe1 ` X ) ) ` ( D ` X ) ) = ( ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ( .r ` R ) ( ( coe1 ` X ) ` ( D ` X ) ) ) )
53 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
54 14 7 39 53 unitlinv 
 |-  ( ( R e. Ring /\ ( ( coe1 ` X ) ` ( D ` X ) ) e. ( Unit ` R ) ) -> ( ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ( .r ` R ) ( ( coe1 ` X ) ` ( D ` X ) ) ) = ( 1r ` R ) )
55 15 54 sylan2 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ( .r ` R ) ( ( coe1 ` X ) ` ( D ` X ) ) ) = ( 1r ` R ) )
56 52 55 eqtrd 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( ( NN0 X. { ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) } ) oF ( .r ` R ) ( coe1 ` X ) ) ` ( D ` X ) ) = ( 1r ` R ) )
57 38 42 56 3eqtrd 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( coe1 ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) ` ( D ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) ) = ( 1r ` R ) )
58 3 11 34 6 2 53 ismon1p 
 |-  ( ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. M <-> ( ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. ( Base ` P ) /\ ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) =/= ( 0g ` P ) /\ ( ( coe1 ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) ` ( D ` ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) ) ) = ( 1r ` R ) ) )
59 22 37 57 58 syl3anbrc 
 |-  ( ( R e. Ring /\ X e. C ) -> ( ( A ` ( I ` ( ( coe1 ` X ) ` ( D ` X ) ) ) ) .x. X ) e. M )