Metamath Proof Explorer

Theorem deg1mhm

Description: Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015)

Ref Expression
Hypotheses deg1mhm.d 
|- D = ( deg1 ` R )
deg1mhm.b 
|- B = ( Base ` P )
deg1mhm.p 
|- P = ( Poly1 ` R )
deg1mhm.z 
|- .0. = ( 0g ` P )
deg1mhm.y 
|- Y = ( ( mulGrp ` P ) |`s ( B \ { .0. } ) )
deg1mhm.n 
|- N = ( CCfld |`s NN0 )
Assertion deg1mhm 
|- ( R e. Domn -> ( D |` ( B \ { .0. } ) ) e. ( Y MndHom N ) )

Proof

Step Hyp Ref Expression
1 deg1mhm.d 
 |-  D = ( deg1 ` R )
2 deg1mhm.b 
 |-  B = ( Base ` P )
3 deg1mhm.p 
 |-  P = ( Poly1 ` R )
4 deg1mhm.z 
 |-  .0. = ( 0g ` P )
5 deg1mhm.y 
 |-  Y = ( ( mulGrp ` P ) |`s ( B \ { .0. } ) )
6 deg1mhm.n 
 |-  N = ( CCfld |`s NN0 )
7 3 ply1domn 
 |-  ( R e. Domn -> P e. Domn )
8 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
9 2 4 8 isdomn3 
 |-  ( P e. Domn <-> ( P e. Ring /\ ( B \ { .0. } ) e. ( SubMnd ` ( mulGrp ` P ) ) ) )
10 9 simprbi 
 |-  ( P e. Domn -> ( B \ { .0. } ) e. ( SubMnd ` ( mulGrp ` P ) ) )
11 7 10 syl 
 |-  ( R e. Domn -> ( B \ { .0. } ) e. ( SubMnd ` ( mulGrp ` P ) ) )
12 5 submmnd 
 |-  ( ( B \ { .0. } ) e. ( SubMnd ` ( mulGrp ` P ) ) -> Y e. Mnd )
13 11 12 syl 
 |-  ( R e. Domn -> Y e. Mnd )
14 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
15 6 submmnd 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> N e. Mnd )
16 14 15 mp1i 
 |-  ( R e. Domn -> N e. Mnd )
17 13 16 jca 
 |-  ( R e. Domn -> ( Y e. Mnd /\ N e. Mnd ) )
18 1 3 2 deg1xrf 
 |-  D : B --> RR*
19 ffn 
 |-  ( D : B --> RR* -> D Fn B )
20 18 19 ax-mp 
 |-  D Fn B
21 difss 
 |-  ( B \ { .0. } ) C_ B
22 fnssres 
 |-  ( ( D Fn B /\ ( B \ { .0. } ) C_ B ) -> ( D |` ( B \ { .0. } ) ) Fn ( B \ { .0. } ) )
23 20 21 22 mp2an 
 |-  ( D |` ( B \ { .0. } ) ) Fn ( B \ { .0. } )
24 23 a1i 
 |-  ( R e. Domn -> ( D |` ( B \ { .0. } ) ) Fn ( B \ { .0. } ) )
25 fvres 
 |-  ( x e. ( B \ { .0. } ) -> ( ( D |` ( B \ { .0. } ) ) ` x ) = ( D ` x ) )
26 25 adantl 
 |-  ( ( R e. Domn /\ x e. ( B \ { .0. } ) ) -> ( ( D |` ( B \ { .0. } ) ) ` x ) = ( D ` x ) )
27 domnring 
 |-  ( R e. Domn -> R e. Ring )
28 27 adantr 
 |-  ( ( R e. Domn /\ x e. ( B \ { .0. } ) ) -> R e. Ring )
29 eldifi 
 |-  ( x e. ( B \ { .0. } ) -> x e. B )
30 29 adantl 
 |-  ( ( R e. Domn /\ x e. ( B \ { .0. } ) ) -> x e. B )
31 eldifsni 
 |-  ( x e. ( B \ { .0. } ) -> x =/= .0. )
32 31 adantl 
 |-  ( ( R e. Domn /\ x e. ( B \ { .0. } ) ) -> x =/= .0. )
33 1 3 4 2 deg1nn0cl 
 |-  ( ( R e. Ring /\ x e. B /\ x =/= .0. ) -> ( D ` x ) e. NN0 )
34 28 30 32 33 syl3anc 
 |-  ( ( R e. Domn /\ x e. ( B \ { .0. } ) ) -> ( D ` x ) e. NN0 )
35 26 34 eqeltrd 
 |-  ( ( R e. Domn /\ x e. ( B \ { .0. } ) ) -> ( ( D |` ( B \ { .0. } ) ) ` x ) e. NN0 )
36 35 ralrimiva 
 |-  ( R e. Domn -> A. x e. ( B \ { .0. } ) ( ( D |` ( B \ { .0. } ) ) ` x ) e. NN0 )
37 ffnfv 
 |-  ( ( D |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 <-> ( ( D |` ( B \ { .0. } ) ) Fn ( B \ { .0. } ) /\ A. x e. ( B \ { .0. } ) ( ( D |` ( B \ { .0. } ) ) ` x ) e. NN0 ) )
38 24 36 37 sylanbrc 
 |-  ( R e. Domn -> ( D |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 )
39 eqid 
 |-  ( RLReg ` R ) = ( RLReg ` R )
40 eqid 
 |-  ( .r ` P ) = ( .r ` P )
41 27 adantr 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> R e. Ring )
42 29 ad2antrl 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> x e. B )
43 31 ad2antrl 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> x =/= .0. )
44 simpl 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> R e. Domn )
45 eqid 
 |-  ( coe1 ` x ) = ( coe1 ` x )
46 1 3 4 2 39 45 deg1ldgdomn 
 |-  ( ( R e. Domn /\ x e. B /\ x =/= .0. ) -> ( ( coe1 ` x ) ` ( D ` x ) ) e. ( RLReg ` R ) )
47 44 42 43 46 syl3anc 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> ( ( coe1 ` x ) ` ( D ` x ) ) e. ( RLReg ` R ) )
48 eldifi 
 |-  ( y e. ( B \ { .0. } ) -> y e. B )
49 48 ad2antll 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> y e. B )
50 eldifsni 
 |-  ( y e. ( B \ { .0. } ) -> y =/= .0. )
51 50 ad2antll 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> y =/= .0. )
52 1 3 39 2 40 4 41 42 43 47 49 51 deg1mul2 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> ( D ` ( x ( .r ` P ) y ) ) = ( ( D ` x ) + ( D ` y ) ) )
53 domnring 
 |-  ( P e. Domn -> P e. Ring )
54 7 53 syl 
 |-  ( R e. Domn -> P e. Ring )
55 54 adantr 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> P e. Ring )
56 2 40 ringcl 
 |-  ( ( P e. Ring /\ x e. B /\ y e. B ) -> ( x ( .r ` P ) y ) e. B )
57 55 42 49 56 syl3anc 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> ( x ( .r ` P ) y ) e. B )
58 7 adantr 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> P e. Domn )
59 2 40 4 domnmuln0 
 |-  ( ( P e. Domn /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( x ( .r ` P ) y ) =/= .0. )
60 58 42 43 49 51 59 syl122anc 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> ( x ( .r ` P ) y ) =/= .0. )
61 eldifsn 
 |-  ( ( x ( .r ` P ) y ) e. ( B \ { .0. } ) <-> ( ( x ( .r ` P ) y ) e. B /\ ( x ( .r ` P ) y ) =/= .0. ) )
62 57 60 61 sylanbrc 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> ( x ( .r ` P ) y ) e. ( B \ { .0. } ) )
63 fvres 
 |-  ( ( x ( .r ` P ) y ) e. ( B \ { .0. } ) -> ( ( D |` ( B \ { .0. } ) ) ` ( x ( .r ` P ) y ) ) = ( D ` ( x ( .r ` P ) y ) ) )
64 62 63 syl 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> ( ( D |` ( B \ { .0. } ) ) ` ( x ( .r ` P ) y ) ) = ( D ` ( x ( .r ` P ) y ) ) )
65 fvres 
 |-  ( y e. ( B \ { .0. } ) -> ( ( D |` ( B \ { .0. } ) ) ` y ) = ( D ` y ) )
66 25 65 oveqan12d 
 |-  ( ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) -> ( ( ( D |` ( B \ { .0. } ) ) ` x ) + ( ( D |` ( B \ { .0. } ) ) ` y ) ) = ( ( D ` x ) + ( D ` y ) ) )
67 66 adantl 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> ( ( ( D |` ( B \ { .0. } ) ) ` x ) + ( ( D |` ( B \ { .0. } ) ) ` y ) ) = ( ( D ` x ) + ( D ` y ) ) )
68 52 64 67 3eqtr4d 
 |-  ( ( R e. Domn /\ ( x e. ( B \ { .0. } ) /\ y e. ( B \ { .0. } ) ) ) -> ( ( D |` ( B \ { .0. } ) ) ` ( x ( .r ` P ) y ) ) = ( ( ( D |` ( B \ { .0. } ) ) ` x ) + ( ( D |` ( B \ { .0. } ) ) ` y ) ) )
69 68 ralrimivva 
 |-  ( R e. Domn -> A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( ( D |` ( B \ { .0. } ) ) ` ( x ( .r ` P ) y ) ) = ( ( ( D |` ( B \ { .0. } ) ) ` x ) + ( ( D |` ( B \ { .0. } ) ) ` y ) ) )
70 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
71 2 70 ringidcl 
 |-  ( P e. Ring -> ( 1r ` P ) e. B )
72 54 71 syl 
 |-  ( R e. Domn -> ( 1r ` P ) e. B )
73 domnnzr 
 |-  ( P e. Domn -> P e. NzRing )
74 70 4 nzrnz 
 |-  ( P e. NzRing -> ( 1r ` P ) =/= .0. )
75 7 73 74 3syl 
 |-  ( R e. Domn -> ( 1r ` P ) =/= .0. )
76 eldifsn 
 |-  ( ( 1r ` P ) e. ( B \ { .0. } ) <-> ( ( 1r ` P ) e. B /\ ( 1r ` P ) =/= .0. ) )
77 72 75 76 sylanbrc 
 |-  ( R e. Domn -> ( 1r ` P ) e. ( B \ { .0. } ) )
78 fvres 
 |-  ( ( 1r ` P ) e. ( B \ { .0. } ) -> ( ( D |` ( B \ { .0. } ) ) ` ( 1r ` P ) ) = ( D ` ( 1r ` P ) ) )
79 77 78 syl 
 |-  ( R e. Domn -> ( ( D |` ( B \ { .0. } ) ) ` ( 1r ` P ) ) = ( D ` ( 1r ` P ) ) )
80 8 70 ringidval 
 |-  ( 1r ` P ) = ( 0g ` ( mulGrp ` P ) )
81 5 80 subm0 
 |-  ( ( B \ { .0. } ) e. ( SubMnd ` ( mulGrp ` P ) ) -> ( 1r ` P ) = ( 0g ` Y ) )
82 11 81 syl 
 |-  ( R e. Domn -> ( 1r ` P ) = ( 0g ` Y ) )
83 82 fveq2d 
 |-  ( R e. Domn -> ( ( D |` ( B \ { .0. } ) ) ` ( 1r ` P ) ) = ( ( D |` ( B \ { .0. } ) ) ` ( 0g ` Y ) ) )
84 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
85 eqid 
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
86 3 70 85 1 mon1pid 
 |-  ( R e. NzRing -> ( ( 1r ` P ) e. ( Monic1p ` R ) /\ ( D ` ( 1r ` P ) ) = 0 ) )
87 86 simprd 
 |-  ( R e. NzRing -> ( D ` ( 1r ` P ) ) = 0 )
88 84 87 syl 
 |-  ( R e. Domn -> ( D ` ( 1r ` P ) ) = 0 )
89 79 83 88 3eqtr3d 
 |-  ( R e. Domn -> ( ( D |` ( B \ { .0. } ) ) ` ( 0g ` Y ) ) = 0 )
90 38 69 89 3jca 
 |-  ( R e. Domn -> ( ( D |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( ( D |` ( B \ { .0. } ) ) ` ( x ( .r ` P ) y ) ) = ( ( ( D |` ( B \ { .0. } ) ) ` x ) + ( ( D |` ( B \ { .0. } ) ) ` y ) ) /\ ( ( D |` ( B \ { .0. } ) ) ` ( 0g ` Y ) ) = 0 ) )
91 8 2 mgpbas 
 |-  B = ( Base ` ( mulGrp ` P ) )
92 5 91 ressbas2 
 |-  ( ( B \ { .0. } ) C_ B -> ( B \ { .0. } ) = ( Base ` Y ) )
93 21 92 ax-mp 
 |-  ( B \ { .0. } ) = ( Base ` Y )
94 nn0sscn 
 |-  NN0 C_ CC
95 cnfldbas 
 |-  CC = ( Base ` CCfld )
96 6 95 ressbas2 
 |-  ( NN0 C_ CC -> NN0 = ( Base ` N ) )
97 94 96 ax-mp 
 |-  NN0 = ( Base ` N )
98 2 fvexi 
 |-  B e. _V
99 difexg 
 |-  ( B e. _V -> ( B \ { .0. } ) e. _V )
100 98 99 ax-mp 
 |-  ( B \ { .0. } ) e. _V
101 8 40 mgpplusg 
 |-  ( .r ` P ) = ( +g ` ( mulGrp ` P ) )
102 5 101 ressplusg 
 |-  ( ( B \ { .0. } ) e. _V -> ( .r ` P ) = ( +g ` Y ) )
103 100 102 ax-mp 
 |-  ( .r ` P ) = ( +g ` Y )
104 nn0ex 
 |-  NN0 e. _V
105 cnfldadd 
 |-  + = ( +g ` CCfld )
106 6 105 ressplusg 
 |-  ( NN0 e. _V -> + = ( +g ` N ) )
107 104 106 ax-mp 
 |-  + = ( +g ` N )
108 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
109 cnfld0 
 |-  0 = ( 0g ` CCfld )
110 6 109 subm0 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> 0 = ( 0g ` N ) )
111 14 110 ax-mp 
 |-  0 = ( 0g ` N )
112 93 97 103 107 108 111 ismhm 
 |-  ( ( D |` ( B \ { .0. } ) ) e. ( Y MndHom N ) <-> ( ( Y e. Mnd /\ N e. Mnd ) /\ ( ( D |` ( B \ { .0. } ) ) : ( B \ { .0. } ) --> NN0 /\ A. x e. ( B \ { .0. } ) A. y e. ( B \ { .0. } ) ( ( D |` ( B \ { .0. } ) ) ` ( x ( .r ` P ) y ) ) = ( ( ( D |` ( B \ { .0. } ) ) ` x ) + ( ( D |` ( B \ { .0. } ) ) ` y ) ) /\ ( ( D |` ( B \ { .0. } ) ) ` ( 0g ` Y ) ) = 0 ) ) )
113 17 90 112 sylanbrc 
 |-  ( R e. Domn -> ( D |` ( B \ { .0. } ) ) e. ( Y MndHom N ) )