| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hbtlem3.ij | . 2
⊢ (𝜑 → 𝐼 ⊆ 𝐽) | 
| 2 |  | hbtlem3.j | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ 𝑈) | 
| 3 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘𝑃) =
(Base‘𝑃) | 
| 4 |  | hbtlem.u | . . . . . . . 8
⊢ 𝑈 = (LIdeal‘𝑃) | 
| 5 | 3, 4 | lidlss 21223 | . . . . . . 7
⊢ (𝐽 ∈ 𝑈 → 𝐽 ⊆ (Base‘𝑃)) | 
| 6 | 2, 5 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐽 ⊆ (Base‘𝑃)) | 
| 7 | 6 | sselda 3982 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → 𝑎 ∈ (Base‘𝑃)) | 
| 8 |  | eqid 2736 | . . . . . 6
⊢
(deg1‘𝑅) = (deg1‘𝑅) | 
| 9 |  | hbtlem.p | . . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) | 
| 10 | 8, 9, 3 | deg1cl 26123 | . . . . 5
⊢ (𝑎 ∈ (Base‘𝑃) →
((deg1‘𝑅)‘𝑎) ∈ (ℕ0 ∪
{-∞})) | 
| 11 | 7, 10 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → ((deg1‘𝑅)‘𝑎) ∈ (ℕ0 ∪
{-∞})) | 
| 12 |  | elun 4152 | . . . . 5
⊢
(((deg1‘𝑅)‘𝑎) ∈ (ℕ0 ∪
{-∞}) ↔ (((deg1‘𝑅)‘𝑎) ∈ ℕ0 ∨
((deg1‘𝑅)‘𝑎) ∈ {-∞})) | 
| 13 |  | nnssnn0 12531 | . . . . . . 7
⊢ ℕ
⊆ ℕ0 | 
| 14 |  | nn0re 12537 | . . . . . . . 8
⊢
(((deg1‘𝑅)‘𝑎) ∈ ℕ0 →
((deg1‘𝑅)‘𝑎) ∈ ℝ) | 
| 15 |  | arch 12525 | . . . . . . . 8
⊢
(((deg1‘𝑅)‘𝑎) ∈ ℝ → ∃𝑏 ∈ ℕ
((deg1‘𝑅)‘𝑎) < 𝑏) | 
| 16 | 14, 15 | syl 17 | . . . . . . 7
⊢
(((deg1‘𝑅)‘𝑎) ∈ ℕ0 →
∃𝑏 ∈ ℕ
((deg1‘𝑅)‘𝑎) < 𝑏) | 
| 17 |  | ssrexv 4052 | . . . . . . 7
⊢ (ℕ
⊆ ℕ0 → (∃𝑏 ∈ ℕ ((deg1‘𝑅)‘𝑎) < 𝑏 → ∃𝑏 ∈ ℕ0
((deg1‘𝑅)‘𝑎) < 𝑏)) | 
| 18 | 13, 16, 17 | mpsyl 68 | . . . . . 6
⊢
(((deg1‘𝑅)‘𝑎) ∈ ℕ0 →
∃𝑏 ∈
ℕ0 ((deg1‘𝑅)‘𝑎) < 𝑏) | 
| 19 |  | elsni 4642 | . . . . . . 7
⊢
(((deg1‘𝑅)‘𝑎) ∈ {-∞} →
((deg1‘𝑅)‘𝑎) = -∞) | 
| 20 |  | 0nn0 12543 | . . . . . . . . 9
⊢ 0 ∈
ℕ0 | 
| 21 |  | mnflt0 13168 | . . . . . . . . 9
⊢ -∞
< 0 | 
| 22 |  | breq2 5146 | . . . . . . . . . 10
⊢ (𝑏 = 0 → (-∞ < 𝑏 ↔ -∞ <
0)) | 
| 23 | 22 | rspcev 3621 | . . . . . . . . 9
⊢ ((0
∈ ℕ0 ∧ -∞ < 0) → ∃𝑏 ∈ ℕ0
-∞ < 𝑏) | 
| 24 | 20, 21, 23 | mp2an 692 | . . . . . . . 8
⊢
∃𝑏 ∈
ℕ0 -∞ < 𝑏 | 
| 25 |  | breq1 5145 | . . . . . . . . 9
⊢
(((deg1‘𝑅)‘𝑎) = -∞ →
(((deg1‘𝑅)‘𝑎) < 𝑏 ↔ -∞ < 𝑏)) | 
| 26 | 25 | rexbidv 3178 | . . . . . . . 8
⊢
(((deg1‘𝑅)‘𝑎) = -∞ → (∃𝑏 ∈ ℕ0
((deg1‘𝑅)‘𝑎) < 𝑏 ↔ ∃𝑏 ∈ ℕ0 -∞ <
𝑏)) | 
| 27 | 24, 26 | mpbiri 258 | . . . . . . 7
⊢
(((deg1‘𝑅)‘𝑎) = -∞ → ∃𝑏 ∈ ℕ0
((deg1‘𝑅)‘𝑎) < 𝑏) | 
| 28 | 19, 27 | syl 17 | . . . . . 6
⊢
(((deg1‘𝑅)‘𝑎) ∈ {-∞} → ∃𝑏 ∈ ℕ0
((deg1‘𝑅)‘𝑎) < 𝑏) | 
| 29 | 18, 28 | jaoi 857 | . . . . 5
⊢
((((deg1‘𝑅)‘𝑎) ∈ ℕ0 ∨
((deg1‘𝑅)‘𝑎) ∈ {-∞}) → ∃𝑏 ∈ ℕ0
((deg1‘𝑅)‘𝑎) < 𝑏) | 
| 30 | 12, 29 | sylbi 217 | . . . 4
⊢
(((deg1‘𝑅)‘𝑎) ∈ (ℕ0 ∪
{-∞}) → ∃𝑏
∈ ℕ0 ((deg1‘𝑅)‘𝑎) < 𝑏) | 
| 31 | 11, 30 | syl 17 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → ∃𝑏 ∈ ℕ0
((deg1‘𝑅)‘𝑎) < 𝑏) | 
| 32 |  | breq2 5146 | . . . . . . . . . . 11
⊢ (𝑐 = 0 →
(((deg1‘𝑅)‘𝑎) < 𝑐 ↔ ((deg1‘𝑅)‘𝑎) < 0)) | 
| 33 | 32 | imbi1d 341 | . . . . . . . . . 10
⊢ (𝑐 = 0 →
((((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼) ↔ (((deg1‘𝑅)‘𝑎) < 0 → 𝑎 ∈ 𝐼))) | 
| 34 | 33 | ralbidv 3177 | . . . . . . . . 9
⊢ (𝑐 = 0 → (∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼) ↔ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 0 → 𝑎 ∈ 𝐼))) | 
| 35 | 34 | imbi2d 340 | . . . . . . . 8
⊢ (𝑐 = 0 → ((𝜑 → ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼)) ↔ (𝜑 → ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 0 → 𝑎 ∈ 𝐼)))) | 
| 36 |  | breq2 5146 | . . . . . . . . . . 11
⊢ (𝑐 = 𝑏 → (((deg1‘𝑅)‘𝑎) < 𝑐 ↔ ((deg1‘𝑅)‘𝑎) < 𝑏)) | 
| 37 | 36 | imbi1d 341 | . . . . . . . . . 10
⊢ (𝑐 = 𝑏 → ((((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼) ↔ (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼))) | 
| 38 | 37 | ralbidv 3177 | . . . . . . . . 9
⊢ (𝑐 = 𝑏 → (∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼) ↔ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼))) | 
| 39 | 38 | imbi2d 340 | . . . . . . . 8
⊢ (𝑐 = 𝑏 → ((𝜑 → ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼)) ↔ (𝜑 → ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)))) | 
| 40 |  | breq2 5146 | . . . . . . . . . . . 12
⊢ (𝑐 = (𝑏 + 1) → (((deg1‘𝑅)‘𝑎) < 𝑐 ↔ ((deg1‘𝑅)‘𝑎) < (𝑏 + 1))) | 
| 41 | 40 | imbi1d 341 | . . . . . . . . . . 11
⊢ (𝑐 = (𝑏 + 1) → ((((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼) ↔ (((deg1‘𝑅)‘𝑎) < (𝑏 + 1) → 𝑎 ∈ 𝐼))) | 
| 42 | 41 | ralbidv 3177 | . . . . . . . . . 10
⊢ (𝑐 = (𝑏 + 1) → (∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼) ↔ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < (𝑏 + 1) → 𝑎 ∈ 𝐼))) | 
| 43 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝑑 → ((deg1‘𝑅)‘𝑎) = ((deg1‘𝑅)‘𝑑)) | 
| 44 | 43 | breq1d 5152 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑑 → (((deg1‘𝑅)‘𝑎) < (𝑏 + 1) ↔ ((deg1‘𝑅)‘𝑑) < (𝑏 + 1))) | 
| 45 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑑 → (𝑎 ∈ 𝐼 ↔ 𝑑 ∈ 𝐼)) | 
| 46 | 44, 45 | imbi12d 344 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑑 → ((((deg1‘𝑅)‘𝑎) < (𝑏 + 1) → 𝑎 ∈ 𝐼) ↔ (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) → 𝑑 ∈ 𝐼))) | 
| 47 | 46 | cbvralvw 3236 | . . . . . . . . . 10
⊢
(∀𝑎 ∈
𝐽
(((deg1‘𝑅)‘𝑎) < (𝑏 + 1) → 𝑎 ∈ 𝐼) ↔ ∀𝑑 ∈ 𝐽 (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) → 𝑑 ∈ 𝐼)) | 
| 48 | 42, 47 | bitrdi 287 | . . . . . . . . 9
⊢ (𝑐 = (𝑏 + 1) → (∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼) ↔ ∀𝑑 ∈ 𝐽 (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) → 𝑑 ∈ 𝐼))) | 
| 49 | 48 | imbi2d 340 | . . . . . . . 8
⊢ (𝑐 = (𝑏 + 1) → ((𝜑 → ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑐 → 𝑎 ∈ 𝐼)) ↔ (𝜑 → ∀𝑑 ∈ 𝐽 (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) → 𝑑 ∈ 𝐼)))) | 
| 50 |  | hbtlem3.r | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 51 | 50 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → 𝑅 ∈ Ring) | 
| 52 |  | eqid 2736 | . . . . . . . . . . . 12
⊢
(0g‘𝑃) = (0g‘𝑃) | 
| 53 | 8, 9, 52, 3 | deg1lt0 26131 | . . . . . . . . . . 11
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑃)) →
(((deg1‘𝑅)‘𝑎) < 0 ↔ 𝑎 = (0g‘𝑃))) | 
| 54 | 51, 7, 53 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → (((deg1‘𝑅)‘𝑎) < 0 ↔ 𝑎 = (0g‘𝑃))) | 
| 55 | 9 | ply1ring 22250 | . . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) | 
| 56 | 50, 55 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑃 ∈ Ring) | 
| 57 |  | hbtlem3.i | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐼 ∈ 𝑈) | 
| 58 | 4, 52 | lidl0cl 21231 | . . . . . . . . . . . . 13
⊢ ((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (0g‘𝑃) ∈ 𝐼) | 
| 59 | 56, 57, 58 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝑃) ∈ 𝐼) | 
| 60 |  | eleq1a 2835 | . . . . . . . . . . . 12
⊢
((0g‘𝑃) ∈ 𝐼 → (𝑎 = (0g‘𝑃) → 𝑎 ∈ 𝐼)) | 
| 61 | 59, 60 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑎 = (0g‘𝑃) → 𝑎 ∈ 𝐼)) | 
| 62 | 61 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → (𝑎 = (0g‘𝑃) → 𝑎 ∈ 𝐼)) | 
| 63 | 54, 62 | sylbid 240 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → (((deg1‘𝑅)‘𝑎) < 0 → 𝑎 ∈ 𝐼)) | 
| 64 | 63 | ralrimiva 3145 | . . . . . . . 8
⊢ (𝜑 → ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 0 → 𝑎 ∈ 𝐼)) | 
| 65 | 6 | 3ad2ant2 1134 | . . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) → 𝐽 ⊆ (Base‘𝑃)) | 
| 66 | 65 | sselda 3982 | . . . . . . . . . . . . . 14
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ 𝑑 ∈ 𝐽) → 𝑑 ∈ (Base‘𝑃)) | 
| 67 | 8, 9, 3 | deg1cl 26123 | . . . . . . . . . . . . . 14
⊢ (𝑑 ∈ (Base‘𝑃) →
((deg1‘𝑅)‘𝑑) ∈ (ℕ0 ∪
{-∞})) | 
| 68 | 66, 67 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ 𝑑 ∈ 𝐽) → ((deg1‘𝑅)‘𝑑) ∈ (ℕ0 ∪
{-∞})) | 
| 69 |  | simpl1 1191 | . . . . . . . . . . . . . 14
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ 𝑑 ∈ 𝐽) → 𝑏 ∈ ℕ0) | 
| 70 | 69 | nn0zd 12641 | . . . . . . . . . . . . 13
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ 𝑑 ∈ 𝐽) → 𝑏 ∈ ℤ) | 
| 71 |  | degltp1le 26113 | . . . . . . . . . . . . 13
⊢
((((deg1‘𝑅)‘𝑑) ∈ (ℕ0 ∪
{-∞}) ∧ 𝑏 ∈
ℤ) → (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) ↔ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) | 
| 72 | 68, 70, 71 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ 𝑑 ∈ 𝐽) → (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) ↔ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) | 
| 73 |  | hbtlem5.e | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥)) | 
| 74 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑏 → ((𝑆‘𝐽)‘𝑥) = ((𝑆‘𝐽)‘𝑏)) | 
| 75 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑏 → ((𝑆‘𝐼)‘𝑥) = ((𝑆‘𝐼)‘𝑏)) | 
| 76 | 74, 75 | sseq12d 4016 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑏 → (((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥) ↔ ((𝑆‘𝐽)‘𝑏) ⊆ ((𝑆‘𝐼)‘𝑏))) | 
| 77 | 76 | rspcva 3619 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 ((𝑆‘𝐽)‘𝑥) ⊆ ((𝑆‘𝐼)‘𝑥)) → ((𝑆‘𝐽)‘𝑏) ⊆ ((𝑆‘𝐼)‘𝑏)) | 
| 78 | 73, 77 | sylan2 593 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑) → ((𝑆‘𝐽)‘𝑏) ⊆ ((𝑆‘𝐼)‘𝑏)) | 
| 79 | 50 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑) → 𝑅 ∈ Ring) | 
| 80 | 2 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑) → 𝐽 ∈ 𝑈) | 
| 81 |  | simpl 482 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑) → 𝑏 ∈
ℕ0) | 
| 82 |  | hbtlem.s | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑆 = (ldgIdlSeq‘𝑅) | 
| 83 | 9, 4, 82, 8 | hbtlem1 43140 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Ring ∧ 𝐽 ∈ 𝑈 ∧ 𝑏 ∈ ℕ0) → ((𝑆‘𝐽)‘𝑏) = {𝑐 ∣ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 84 | 79, 80, 81, 83 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑) → ((𝑆‘𝐽)‘𝑏) = {𝑐 ∣ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 85 | 57 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑) → 𝐼 ∈ 𝑈) | 
| 86 | 9, 4, 82, 8 | hbtlem1 43140 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑏 ∈ ℕ0) → ((𝑆‘𝐼)‘𝑏) = {𝑐 ∣ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 87 | 79, 85, 81, 86 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑) → ((𝑆‘𝐼)‘𝑏) = {𝑐 ∣ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 88 | 78, 84, 87 | 3sstr3d 4037 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑) → {𝑐 ∣ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))} ⊆ {𝑐 ∣ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 89 | 88 | 3adant3 1132 | . . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) → {𝑐 ∣ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))} ⊆ {𝑐 ∣ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 90 | 89 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) → {𝑐 ∣ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))} ⊆ {𝑐 ∣ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 91 |  | simpl 482 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏) → 𝑑 ∈ 𝐽) | 
| 92 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏) → ((deg1‘𝑅)‘𝑑) ≤ 𝑏) | 
| 93 |  | eqidd 2737 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏) → ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑑)‘𝑏)) | 
| 94 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑑 → ((deg1‘𝑅)‘𝑒) = ((deg1‘𝑅)‘𝑑)) | 
| 95 | 94 | breq1d 5152 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑑 → (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ↔ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) | 
| 96 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 = 𝑑 → (coe1‘𝑒) = (coe1‘𝑑)) | 
| 97 | 96 | fveq1d 6907 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑑 → ((coe1‘𝑒)‘𝑏) = ((coe1‘𝑑)‘𝑏)) | 
| 98 | 97 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑑 → (((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏) ↔ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑑)‘𝑏))) | 
| 99 | 95, 98 | anbi12d 632 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝑑 → ((((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)) ↔ (((deg1‘𝑅)‘𝑑) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑑)‘𝑏)))) | 
| 100 | 99 | rspcev 3621 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ∈ 𝐽 ∧ (((deg1‘𝑅)‘𝑑) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑑)‘𝑏))) → ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏))) | 
| 101 | 91, 92, 93, 100 | syl12anc 836 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏) → ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏))) | 
| 102 |  | fvex 6918 | . . . . . . . . . . . . . . . . . 18
⊢
((coe1‘𝑑)‘𝑏) ∈ V | 
| 103 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 = ((coe1‘𝑑)‘𝑏) → (𝑐 = ((coe1‘𝑒)‘𝑏) ↔ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏))) | 
| 104 | 103 | anbi2d 630 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 = ((coe1‘𝑑)‘𝑏) → ((((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏)) ↔ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) | 
| 105 | 104 | rexbidv 3178 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = ((coe1‘𝑑)‘𝑏) → (∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏)) ↔ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) | 
| 106 | 102, 105 | elab 3678 | . . . . . . . . . . . . . . . . 17
⊢
(((coe1‘𝑑)‘𝑏) ∈ {𝑐 ∣ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))} ↔ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏))) | 
| 107 | 101, 106 | sylibr 234 | . . . . . . . . . . . . . . . 16
⊢ ((𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏) → ((coe1‘𝑑)‘𝑏) ∈ {𝑐 ∣ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 108 | 107 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) → ((coe1‘𝑑)‘𝑏) ∈ {𝑐 ∣ ∃𝑒 ∈ 𝐽 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 109 | 90, 108 | sseldd 3983 | . . . . . . . . . . . . . 14
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) → ((coe1‘𝑑)‘𝑏) ∈ {𝑐 ∣ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))}) | 
| 110 | 104 | rexbidv 3178 | . . . . . . . . . . . . . . . 16
⊢ (𝑐 = ((coe1‘𝑑)‘𝑏) → (∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏)) ↔ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) | 
| 111 | 102, 110 | elab 3678 | . . . . . . . . . . . . . . 15
⊢
(((coe1‘𝑑)‘𝑏) ∈ {𝑐 ∣ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))} ↔ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏))) | 
| 112 |  | simpll2 1213 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝜑) | 
| 113 | 112, 56 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑃 ∈ Ring) | 
| 114 |  | ringgrp 20236 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑃 ∈ Ring → 𝑃 ∈ Grp) | 
| 115 | 113, 114 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑃 ∈ Grp) | 
| 116 | 112, 6 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝐽 ⊆ (Base‘𝑃)) | 
| 117 |  | simplrl 776 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑑 ∈ 𝐽) | 
| 118 | 116, 117 | sseldd 3983 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑑 ∈ (Base‘𝑃)) | 
| 119 | 3, 4 | lidlss 21223 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐼 ∈ 𝑈 → 𝐼 ⊆ (Base‘𝑃)) | 
| 120 | 57, 119 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐼 ⊆ (Base‘𝑃)) | 
| 121 | 112, 120 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝐼 ⊆ (Base‘𝑃)) | 
| 122 |  | simprl 770 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑒 ∈ 𝐼) | 
| 123 | 121, 122 | sseldd 3983 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑒 ∈ (Base‘𝑃)) | 
| 124 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(+g‘𝑃) = (+g‘𝑃) | 
| 125 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(-g‘𝑃) = (-g‘𝑃) | 
| 126 | 3, 124, 125 | grpnpcan 19051 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ Grp ∧ 𝑑 ∈ (Base‘𝑃) ∧ 𝑒 ∈ (Base‘𝑃)) → ((𝑑(-g‘𝑃)𝑒)(+g‘𝑃)𝑒) = 𝑑) | 
| 127 | 115, 118,
123, 126 | syl3anc 1372 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → ((𝑑(-g‘𝑃)𝑒)(+g‘𝑃)𝑒) = 𝑑) | 
| 128 | 57 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) → 𝐼 ∈ 𝑈) | 
| 129 | 128 | ad2antrr 726 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝐼 ∈ 𝑈) | 
| 130 |  | simpll1 1212 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑏 ∈ ℕ0) | 
| 131 | 112, 50 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑅 ∈ Ring) | 
| 132 |  | simplrr 777 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → ((deg1‘𝑅)‘𝑑) ≤ 𝑏) | 
| 133 |  | simprrl 780 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → ((deg1‘𝑅)‘𝑒) ≤ 𝑏) | 
| 134 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(coe1‘𝑑) = (coe1‘𝑑) | 
| 135 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . 20
⊢
(coe1‘𝑒) = (coe1‘𝑒) | 
| 136 |  | simprrr 781 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)) | 
| 137 | 8, 9, 3, 125, 130, 131, 118, 132, 123, 133, 134, 135, 136 | deg1sublt 26150 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → ((deg1‘𝑅)‘(𝑑(-g‘𝑃)𝑒)) < 𝑏) | 
| 138 | 112, 2 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝐽 ∈ 𝑈) | 
| 139 | 1 | 3ad2ant2 1134 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) → 𝐼 ⊆ 𝐽) | 
| 140 | 139 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝐼 ⊆ 𝐽) | 
| 141 | 140, 122 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑒 ∈ 𝐽) | 
| 142 | 4, 125 | lidlsubcl 21235 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 ∈ Ring ∧ 𝐽 ∈ 𝑈) ∧ (𝑑 ∈ 𝐽 ∧ 𝑒 ∈ 𝐽)) → (𝑑(-g‘𝑃)𝑒) ∈ 𝐽) | 
| 143 | 113, 138,
117, 141, 142 | syl22anc 838 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → (𝑑(-g‘𝑃)𝑒) ∈ 𝐽) | 
| 144 |  | simpll3 1214 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) | 
| 145 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = (𝑑(-g‘𝑃)𝑒) → ((deg1‘𝑅)‘𝑎) = ((deg1‘𝑅)‘(𝑑(-g‘𝑃)𝑒))) | 
| 146 | 145 | breq1d 5152 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (𝑑(-g‘𝑃)𝑒) → (((deg1‘𝑅)‘𝑎) < 𝑏 ↔ ((deg1‘𝑅)‘(𝑑(-g‘𝑃)𝑒)) < 𝑏)) | 
| 147 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 = (𝑑(-g‘𝑃)𝑒) → (𝑎 ∈ 𝐼 ↔ (𝑑(-g‘𝑃)𝑒) ∈ 𝐼)) | 
| 148 | 146, 147 | imbi12d 344 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = (𝑑(-g‘𝑃)𝑒) → ((((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼) ↔ (((deg1‘𝑅)‘(𝑑(-g‘𝑃)𝑒)) < 𝑏 → (𝑑(-g‘𝑃)𝑒) ∈ 𝐼))) | 
| 149 | 148 | rspcva 3619 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑(-g‘𝑃)𝑒) ∈ 𝐽 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) → (((deg1‘𝑅)‘(𝑑(-g‘𝑃)𝑒)) < 𝑏 → (𝑑(-g‘𝑃)𝑒) ∈ 𝐼)) | 
| 150 | 143, 144,
149 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → (((deg1‘𝑅)‘(𝑑(-g‘𝑃)𝑒)) < 𝑏 → (𝑑(-g‘𝑃)𝑒) ∈ 𝐼)) | 
| 151 | 137, 150 | mpd 15 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → (𝑑(-g‘𝑃)𝑒) ∈ 𝐼) | 
| 152 | 4, 124 | lidlacl 21232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑃 ∈ Ring ∧ 𝐼 ∈ 𝑈) ∧ ((𝑑(-g‘𝑃)𝑒) ∈ 𝐼 ∧ 𝑒 ∈ 𝐼)) → ((𝑑(-g‘𝑃)𝑒)(+g‘𝑃)𝑒) ∈ 𝐼) | 
| 153 | 113, 129,
151, 122, 152 | syl22anc 838 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → ((𝑑(-g‘𝑃)𝑒)(+g‘𝑃)𝑒) ∈ 𝐼) | 
| 154 | 127, 153 | eqeltrrd 2841 | . . . . . . . . . . . . . . . 16
⊢ ((((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) ∧ (𝑒 ∈ 𝐼 ∧ (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)))) → 𝑑 ∈ 𝐼) | 
| 155 | 154 | rexlimdvaa 3155 | . . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) → (∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ ((coe1‘𝑑)‘𝑏) = ((coe1‘𝑒)‘𝑏)) → 𝑑 ∈ 𝐼)) | 
| 156 | 111, 155 | biimtrid 242 | . . . . . . . . . . . . . 14
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) → (((coe1‘𝑑)‘𝑏) ∈ {𝑐 ∣ ∃𝑒 ∈ 𝐼 (((deg1‘𝑅)‘𝑒) ≤ 𝑏 ∧ 𝑐 = ((coe1‘𝑒)‘𝑏))} → 𝑑 ∈ 𝐼)) | 
| 157 | 109, 156 | mpd 15 | . . . . . . . . . . . . 13
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ (𝑑 ∈ 𝐽 ∧ ((deg1‘𝑅)‘𝑑) ≤ 𝑏)) → 𝑑 ∈ 𝐼) | 
| 158 | 157 | expr 456 | . . . . . . . . . . . 12
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ 𝑑 ∈ 𝐽) → (((deg1‘𝑅)‘𝑑) ≤ 𝑏 → 𝑑 ∈ 𝐼)) | 
| 159 | 72, 158 | sylbid 240 | . . . . . . . . . . 11
⊢ (((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) ∧ 𝑑 ∈ 𝐽) → (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) → 𝑑 ∈ 𝐼)) | 
| 160 | 159 | ralrimiva 3145 | . . . . . . . . . 10
⊢ ((𝑏 ∈ ℕ0
∧ 𝜑 ∧ ∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) → ∀𝑑 ∈ 𝐽 (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) → 𝑑 ∈ 𝐼)) | 
| 161 | 160 | 3exp 1119 | . . . . . . . . 9
⊢ (𝑏 ∈ ℕ0
→ (𝜑 →
(∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼) → ∀𝑑 ∈ 𝐽 (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) → 𝑑 ∈ 𝐼)))) | 
| 162 | 161 | a2d 29 | . . . . . . . 8
⊢ (𝑏 ∈ ℕ0
→ ((𝜑 →
∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) → (𝜑 → ∀𝑑 ∈ 𝐽 (((deg1‘𝑅)‘𝑑) < (𝑏 + 1) → 𝑑 ∈ 𝐼)))) | 
| 163 | 35, 39, 49, 39, 64, 162 | nn0ind 12715 | . . . . . . 7
⊢ (𝑏 ∈ ℕ0
→ (𝜑 →
∀𝑎 ∈ 𝐽 (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼))) | 
| 164 |  | rsp 3246 | . . . . . . 7
⊢
(∀𝑎 ∈
𝐽
(((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼) → (𝑎 ∈ 𝐽 → (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼))) | 
| 165 | 163, 164 | syl6com 37 | . . . . . 6
⊢ (𝜑 → (𝑏 ∈ ℕ0 → (𝑎 ∈ 𝐽 → (((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)))) | 
| 166 | 165 | com23 86 | . . . . 5
⊢ (𝜑 → (𝑎 ∈ 𝐽 → (𝑏 ∈ ℕ0 →
(((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)))) | 
| 167 | 166 | imp 406 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → (𝑏 ∈ ℕ0 →
(((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼))) | 
| 168 | 167 | rexlimdv 3152 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → (∃𝑏 ∈ ℕ0
((deg1‘𝑅)‘𝑎) < 𝑏 → 𝑎 ∈ 𝐼)) | 
| 169 | 31, 168 | mpd 15 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐽) → 𝑎 ∈ 𝐼) | 
| 170 | 1, 169 | eqelssd 4004 | 1
⊢ (𝜑 → 𝐼 = 𝐽) |