| Step | Hyp | Ref
| Expression |
| 1 | | deg1mul3le.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
| 2 | 1 | ply1ring 22249 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
| 3 | 2 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝑃 ∈ Ring) |
| 4 | | deg1mul3le.a |
. . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) |
| 5 | | deg1mul3le.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
| 6 | | deg1mul3le.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑃) |
| 7 | 1, 4, 5, 6 | ply1sclf 22288 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝐴:𝐾⟶𝐵) |
| 8 | 7 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐴:𝐾⟶𝐵) |
| 9 | | simp2 1138 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐾) |
| 10 | 8, 9 | ffvelcdmd 7105 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐴‘𝐹) ∈ 𝐵) |
| 11 | | simp3 1139 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
| 12 | | deg1mul3le.t |
. . . . . . 7
⊢ · =
(.r‘𝑃) |
| 13 | 6, 12 | ringcl 20247 |
. . . . . 6
⊢ ((𝑃 ∈ Ring ∧ (𝐴‘𝐹) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐴‘𝐹) · 𝐺) ∈ 𝐵) |
| 14 | 3, 10, 11, 13 | syl3anc 1373 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((𝐴‘𝐹) · 𝐺) ∈ 𝐵) |
| 15 | | eqid 2737 |
. . . . . 6
⊢
(coe1‘((𝐴‘𝐹) · 𝐺)) = (coe1‘((𝐴‘𝐹) · 𝐺)) |
| 16 | 15, 6, 1, 5 | coe1f 22213 |
. . . . 5
⊢ (((𝐴‘𝐹) · 𝐺) ∈ 𝐵 → (coe1‘((𝐴‘𝐹) · 𝐺)):ℕ0⟶𝐾) |
| 17 | 14, 16 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (coe1‘((𝐴‘𝐹) · 𝐺)):ℕ0⟶𝐾) |
| 18 | | eldifi 4131 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
∖ ((coe1‘𝐺) supp (0g‘𝑅))) → 𝑎 ∈ ℕ0) |
| 19 | | simpl1 1192 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝑅 ∈ Ring) |
| 20 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝐹 ∈ 𝐾) |
| 21 | | simpl3 1194 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝐺 ∈ 𝐵) |
| 22 | | simpr 484 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝑎 ∈
ℕ0) |
| 23 | | eqid 2737 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 24 | 1, 6, 5, 4, 12, 23 | coe1sclmulfv 22286 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) →
((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
| 25 | 19, 20, 21, 22, 24 | syl121anc 1377 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) →
((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
| 26 | 18, 25 | sylan2 593 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
| 27 | | eqid 2737 |
. . . . . . . . 9
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
| 28 | 27, 6, 1, 5 | coe1f 22213 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝐵 → (coe1‘𝐺):ℕ0⟶𝐾) |
| 29 | 28 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (coe1‘𝐺):ℕ0⟶𝐾) |
| 30 | | ssidd 4007 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ((coe1‘𝐺) supp (0g‘𝑅))) |
| 31 | | nn0ex 12532 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
| 32 | 31 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ℕ0 ∈
V) |
| 33 | | fvexd 6921 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (0g‘𝑅) ∈ V) |
| 34 | 29, 30, 32, 33 | suppssr 8220 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘𝐺)‘𝑎) = (0g‘𝑅)) |
| 35 | 34 | oveq2d 7447 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎)) = (𝐹(.r‘𝑅)(0g‘𝑅))) |
| 36 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 37 | 5, 23, 36 | ringrz 20291 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 38 | 37 | 3adant3 1133 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 39 | 38 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 40 | 26, 35, 39 | 3eqtrd 2781 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (0g‘𝑅)) |
| 41 | 17, 40 | suppss 8219 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)) ⊆
((coe1‘𝐺)
supp (0g‘𝑅))) |
| 42 | | suppssdm 8202 |
. . . . 5
⊢
((coe1‘𝐺) supp (0g‘𝑅)) ⊆ dom
(coe1‘𝐺) |
| 43 | 42, 29 | fssdm 6755 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℕ0) |
| 44 | | nn0ssre 12530 |
. . . . 5
⊢
ℕ0 ⊆ ℝ |
| 45 | | ressxr 11305 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
| 46 | 44, 45 | sstri 3993 |
. . . 4
⊢
ℕ0 ⊆ ℝ* |
| 47 | 43, 46 | sstrdi 3996 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℝ*) |
| 48 | | supxrss 13374 |
. . 3
⊢
((((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)) ⊆
((coe1‘𝐺)
supp (0g‘𝑅)) ∧ ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℝ*) → sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, < )
≤ sup(((coe1‘𝐺) supp (0g‘𝑅)), ℝ*, <
)) |
| 49 | 41, 47, 48 | syl2anc 584 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, < )
≤ sup(((coe1‘𝐺) supp (0g‘𝑅)), ℝ*, <
)) |
| 50 | | deg1mul3le.d |
. . . 4
⊢ 𝐷 = (deg1‘𝑅) |
| 51 | 50, 1, 6, 36, 15 | deg1val 26135 |
. . 3
⊢ (((𝐴‘𝐹) · 𝐺) ∈ 𝐵 → (𝐷‘((𝐴‘𝐹) · 𝐺)) = sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, <
)) |
| 52 | 14, 51 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) = sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, <
)) |
| 53 | 50, 1, 6, 36, 27 | deg1val 26135 |
. . 3
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) = sup(((coe1‘𝐺) supp
(0g‘𝑅)),
ℝ*, < )) |
| 54 | 53 | 3ad2ant3 1136 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐺) = sup(((coe1‘𝐺) supp
(0g‘𝑅)),
ℝ*, < )) |
| 55 | 49, 52, 54 | 3brtr4d 5175 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) ≤ (𝐷‘𝐺)) |