Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . . . . . . 11
|
2 | | ig1peu.u |
. . . . . . . . . . 11
LIdeal |
3 | 1, 2 | lidlss 19210 |
. . . . . . . . . 10
|
4 | 3 | 3ad2ant2 1083 |
. . . . . . . . 9
|
5 | 4 | ssdifd 3746 |
. . . . . . . 8
|
6 | | imass2 5501 |
. . . . . . . 8
|
7 | 5, 6 | syl 17 |
. . . . . . 7
|
8 | | drngring 18754 |
. . . . . . . . 9
|
9 | 8 | 3ad2ant1 1082 |
. . . . . . . 8
|
10 | | ig1peu.d |
. . . . . . . . 9
deg1 |
11 | | ig1peu.p |
. . . . . . . . 9
Poly1 |
12 | | ig1peu.z |
. . . . . . . . 9
|
13 | 10, 11, 12, 1 | deg1n0ima 23849 |
. . . . . . . 8
|
14 | 9, 13 | syl 17 |
. . . . . . 7
|
15 | 7, 14 | sstrd 3613 |
. . . . . 6
|
16 | | nn0uz 11722 |
. . . . . 6
|
17 | 15, 16 | syl6sseq 3651 |
. . . . 5
|
18 | 11 | ply1ring 19618 |
. . . . . . . . . 10
|
19 | 9, 18 | syl 17 |
. . . . . . . . 9
|
20 | | simp2 1062 |
. . . . . . . . 9
|
21 | 2, 12 | lidl0cl 19212 |
. . . . . . . . 9
|
22 | 19, 20, 21 | syl2anc 693 |
. . . . . . . 8
|
23 | 22 | snssd 4340 |
. . . . . . 7
|
24 | | simp3 1063 |
. . . . . . . 8
|
25 | 24 | necomd 2849 |
. . . . . . 7
|
26 | | pssdifn0 3944 |
. . . . . . 7
|
27 | 23, 25, 26 | syl2anc 693 |
. . . . . 6
|
28 | 10, 11, 1 | deg1xrf 23841 |
. . . . . . . . . 10
|
29 | | ffn 6045 |
. . . . . . . . . 10
|
30 | 28, 29 | ax-mp 5 |
. . . . . . . . 9
|
31 | 30 | a1i 11 |
. . . . . . . 8
|
32 | 4 | ssdifssd 3748 |
. . . . . . . 8
|
33 | | fnimaeq0 6013 |
. . . . . . . 8
|
34 | 31, 32, 33 | syl2anc 693 |
. . . . . . 7
|
35 | 34 | necon3bid 2838 |
. . . . . 6
|
36 | 27, 35 | mpbird 247 |
. . . . 5
|
37 | | infssuzcl 11772 |
. . . . 5
inf
|
38 | 17, 36, 37 | syl2anc 693 |
. . . 4
inf |
39 | | fvelimab 6253 |
. . . . 5
inf
inf |
40 | 31, 32, 39 | syl2anc 693 |
. . . 4
inf
inf |
41 | 38, 40 | mpbid 222 |
. . 3
inf
|
42 | 19 | adantr 481 |
. . . . . . . 8
|
43 | | simpl2 1065 |
. . . . . . . 8
|
44 | 9 | adantr 481 |
. . . . . . . . . 10
|
45 | | eqid 2622 |
. . . . . . . . . . 11
algSc algSc |
46 | | eqid 2622 |
. . . . . . . . . . 11
|
47 | 11, 45, 46, 1 | ply1sclf 19655 |
. . . . . . . . . 10
algSc |
48 | 44, 47 | syl 17 |
. . . . . . . . 9
algSc |
49 | | simpl1 1064 |
. . . . . . . . . . . . 13
|
50 | 32 | sselda 3603 |
. . . . . . . . . . . . 13
|
51 | | eldifsni 4320 |
. . . . . . . . . . . . . 14
|
52 | 51 | adantl 482 |
. . . . . . . . . . . . 13
|
53 | | eqid 2622 |
. . . . . . . . . . . . . 14
Unic1p Unic1p |
54 | 11, 1, 12, 53 | drnguc1p 23930 |
. . . . . . . . . . . . 13
Unic1p |
55 | 49, 50, 52, 54 | syl3anc 1326 |
. . . . . . . . . . . 12
Unic1p |
56 | | eqid 2622 |
. . . . . . . . . . . . 13
Unit Unit |
57 | 10, 56, 53 | uc1pldg 23908 |
. . . . . . . . . . . 12
Unic1p coe1 Unit |
58 | 55, 57 | syl 17 |
. . . . . . . . . . 11
coe1 Unit |
59 | | eqid 2622 |
. . . . . . . . . . . 12
|
60 | 56, 59 | unitinvcl 18674 |
. . . . . . . . . . 11
coe1 Unit coe1 Unit |
61 | 44, 58, 60 | syl2anc 693 |
. . . . . . . . . 10
coe1 Unit |
62 | 46, 56 | unitcl 18659 |
. . . . . . . . . 10
coe1 Unit coe1 |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
coe1 |
64 | 48, 63 | ffvelrnd 6360 |
. . . . . . . 8
algSccoe1 |
65 | | eldifi 3732 |
. . . . . . . . 9
|
66 | 65 | adantl 482 |
. . . . . . . 8
|
67 | | eqid 2622 |
. . . . . . . . 9
|
68 | 2, 1, 67 | lidlmcl 19217 |
. . . . . . . 8
algSccoe1
algSccoe1 |
69 | 42, 43, 64, 66, 68 | syl22anc 1327 |
. . . . . . 7
algSccoe1 |
70 | | ig1peu.m |
. . . . . . . . 9
Monic1p |
71 | 53, 70, 11, 67, 45, 10, 59 | uc1pmon1p 23911 |
. . . . . . . 8
Unic1p algSccoe1 |
72 | 44, 55, 71 | syl2anc 693 |
. . . . . . 7
algSccoe1 |
73 | 69, 72 | elind 3798 |
. . . . . 6
algSccoe1 |
74 | | eqid 2622 |
. . . . . . . . . 10
RLReg RLReg |
75 | 74, 56 | unitrrg 19293 |
. . . . . . . . 9
Unit RLReg |
76 | 44, 75 | syl 17 |
. . . . . . . 8
Unit RLReg |
77 | 76, 61 | sseldd 3604 |
. . . . . . 7
coe1 RLReg |
78 | 10, 11, 74, 1, 67, 45 | deg1mul3 23875 |
. . . . . . 7
coe1 RLReg algSccoe1 |
79 | 44, 77, 50, 78 | syl3anc 1326 |
. . . . . 6
algSccoe1 |
80 | | fveq2 6191 |
. . . . . . . 8
algSccoe1 algSccoe1 |
81 | 80 | eqeq1d 2624 |
. . . . . . 7
algSccoe1
algSccoe1 |
82 | 81 | rspcev 3309 |
. . . . . 6
algSccoe1 algSccoe1 |
83 | 73, 79, 82 | syl2anc 693 |
. . . . 5
|
84 | | eqeq2 2633 |
. . . . . 6
inf inf
|
85 | 84 | rexbidv 3052 |
. . . . 5
inf
inf |
86 | 83, 85 | syl5ibcom 235 |
. . . 4
inf inf
|
87 | 86 | rexlimdva 3031 |
. . 3
inf inf |
88 | 41, 87 | mpd 15 |
. 2
inf |
89 | | eqid 2622 |
. . . . . . 7
|
90 | 9 | ad2antrr 762 |
. . . . . . 7
inf
inf |
91 | | inss2 3834 |
. . . . . . . . 9
|
92 | | simprl 794 |
. . . . . . . . 9
|
93 | 91, 92 | sseldi 3601 |
. . . . . . . 8
|
94 | 93 | adantr 481 |
. . . . . . 7
inf
inf |
95 | | simprl 794 |
. . . . . . 7
inf
inf inf |
96 | | simprr 796 |
. . . . . . . . 9
|
97 | 91, 96 | sseldi 3601 |
. . . . . . . 8
|
98 | 97 | adantr 481 |
. . . . . . 7
inf
inf |
99 | | simprr 796 |
. . . . . . 7
inf
inf inf |
100 | 10, 70, 11, 89, 90, 94, 95, 98, 99 | deg1submon1p 23912 |
. . . . . 6
inf
inf inf |
101 | 100 | ex 450 |
. . . . 5
inf
inf
inf |
102 | 17 | ad2antrr 762 |
. . . . . . . . 9
|
103 | 30 | a1i 11 |
. . . . . . . . . 10
|
104 | 32 | ad2antrr 762 |
. . . . . . . . . 10
|
105 | 19 | adantr 481 |
. . . . . . . . . . . . 13
|
106 | | simpl2 1065 |
. . . . . . . . . . . . 13
|
107 | | inss1 3833 |
. . . . . . . . . . . . . 14
|
108 | 107, 92 | sseldi 3601 |
. . . . . . . . . . . . 13
|
109 | 107, 96 | sseldi 3601 |
. . . . . . . . . . . . 13
|
110 | 2, 89 | lidlsubcl 19216 |
. . . . . . . . . . . . 13
|
111 | 105, 106,
108, 109, 110 | syl22anc 1327 |
. . . . . . . . . . . 12
|
112 | 111 | adantr 481 |
. . . . . . . . . . 11
|
113 | | simpr 477 |
. . . . . . . . . . 11
|
114 | | eldifsn 4317 |
. . . . . . . . . . 11
|
115 | 112, 113,
114 | sylanbrc 698 |
. . . . . . . . . 10
|
116 | | fnfvima 6496 |
. . . . . . . . . 10
|
117 | 103, 104,
115, 116 | syl3anc 1326 |
. . . . . . . . 9
|
118 | | infssuzle 11771 |
. . . . . . . . 9
inf |
119 | 102, 117,
118 | syl2anc 693 |
. . . . . . . 8
inf |
120 | 119 | ex 450 |
. . . . . . 7
inf |
121 | | imassrn 5477 |
. . . . . . . . . . 11
|
122 | | frn 6053 |
. . . . . . . . . . . 12
|
123 | 28, 122 | ax-mp 5 |
. . . . . . . . . . 11
|
124 | 121, 123 | sstri 3612 |
. . . . . . . . . 10
|
125 | 124, 38 | sseldi 3601 |
. . . . . . . . 9
inf |
126 | 125 | adantr 481 |
. . . . . . . 8
inf |
127 | | ringgrp 18552 |
. . . . . . . . . . . 12
|
128 | 19, 127 | syl 17 |
. . . . . . . . . . 11
|
129 | 128 | adantr 481 |
. . . . . . . . . 10
|
130 | 107, 4 | syl5ss 3614 |
. . . . . . . . . . . 12
|
131 | 130 | adantr 481 |
. . . . . . . . . . 11
|
132 | 131, 92 | sseldd 3604 |
. . . . . . . . . 10
|
133 | 131, 96 | sseldd 3604 |
. . . . . . . . . 10
|
134 | 1, 89 | grpsubcl 17495 |
. . . . . . . . . 10
|
135 | 129, 132,
133, 134 | syl3anc 1326 |
. . . . . . . . 9
|
136 | 10, 11, 1 | deg1xrcl 23842 |
. . . . . . . . 9
|
137 | 135, 136 | syl 17 |
. . . . . . . 8
|
138 | | xrlenlt 10103 |
. . . . . . . 8
inf inf inf |
139 | 126, 137,
138 | syl2anc 693 |
. . . . . . 7
inf inf |
140 | 120, 139 | sylibd 229 |
. . . . . 6
inf |
141 | 140 | necon4ad 2813 |
. . . . 5
inf |
142 | 101, 141 | syld 47 |
. . . 4
inf
inf
|
143 | 1, 12, 89 | grpsubeq0 17501 |
. . . . 5
|
144 | 129, 132,
133, 143 | syl3anc 1326 |
. . . 4
|
145 | 142, 144 | sylibd 229 |
. . 3
inf
inf
|
146 | 145 | ralrimivva 2971 |
. 2
inf inf |
147 | | fveq2 6191 |
. . . 4
|
148 | 147 | eqeq1d 2624 |
. . 3
inf
inf
|
149 | 148 | reu4 3400 |
. 2
inf inf
inf inf
|
150 | 88, 146, 149 | sylanbrc 698 |
1
inf
|