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 = deg 1 R
deg1mhm.b B = Base P
deg1mhm.p P = Poly 1 R
deg1mhm.z 0 ˙ = 0 P
deg1mhm.y Y = mulGrp P 𝑠 B 0 ˙
deg1mhm.n N = fld 𝑠 0
Assertion deg1mhm R Domn D B 0 ˙ Y MndHom N

Proof

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