Step | Hyp | Ref
| Expression |
1 | | deg1mul3le.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
2 | 1 | ply1ring 21417 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
3 | 2 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝑃 ∈ Ring) |
4 | | deg1mul3le.a |
. . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) |
5 | | deg1mul3le.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
6 | | deg1mul3le.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑃) |
7 | 1, 4, 5, 6 | ply1sclf 21454 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝐴:𝐾⟶𝐵) |
8 | 7 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐴:𝐾⟶𝐵) |
9 | | simp2 1136 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐾) |
10 | 8, 9 | ffvelrnd 6959 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐴‘𝐹) ∈ 𝐵) |
11 | | simp3 1137 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
12 | | deg1mul3le.t |
. . . . . . 7
⊢ · =
(.r‘𝑃) |
13 | 6, 12 | ringcl 19798 |
. . . . . 6
⊢ ((𝑃 ∈ Ring ∧ (𝐴‘𝐹) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐴‘𝐹) · 𝐺) ∈ 𝐵) |
14 | 3, 10, 11, 13 | syl3anc 1370 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((𝐴‘𝐹) · 𝐺) ∈ 𝐵) |
15 | | eqid 2740 |
. . . . . 6
⊢
(coe1‘((𝐴‘𝐹) · 𝐺)) = (coe1‘((𝐴‘𝐹) · 𝐺)) |
16 | 15, 6, 1, 5 | coe1f 21380 |
. . . . 5
⊢ (((𝐴‘𝐹) · 𝐺) ∈ 𝐵 → (coe1‘((𝐴‘𝐹) · 𝐺)):ℕ0⟶𝐾) |
17 | 14, 16 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (coe1‘((𝐴‘𝐹) · 𝐺)):ℕ0⟶𝐾) |
18 | | eldifi 4066 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
∖ ((coe1‘𝐺) supp (0g‘𝑅))) → 𝑎 ∈ ℕ0) |
19 | | simpl1 1190 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝑅 ∈ Ring) |
20 | | simpl2 1191 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝐹 ∈ 𝐾) |
21 | | simpl3 1192 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝐺 ∈ 𝐵) |
22 | | simpr 485 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝑎 ∈
ℕ0) |
23 | | eqid 2740 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
24 | 1, 6, 5, 4, 12, 23 | coe1sclmulfv 21452 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) →
((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
25 | 19, 20, 21, 22, 24 | syl121anc 1374 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) →
((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
26 | 18, 25 | sylan2 593 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
27 | | eqid 2740 |
. . . . . . . . 9
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
28 | 27, 6, 1, 5 | coe1f 21380 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝐵 → (coe1‘𝐺):ℕ0⟶𝐾) |
29 | 28 | 3ad2ant3 1134 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (coe1‘𝐺):ℕ0⟶𝐾) |
30 | | ssidd 3949 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ((coe1‘𝐺) supp (0g‘𝑅))) |
31 | | nn0ex 12239 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ℕ0 ∈
V) |
33 | | fvexd 6786 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (0g‘𝑅) ∈ V) |
34 | 29, 30, 32, 33 | suppssr 8003 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘𝐺)‘𝑎) = (0g‘𝑅)) |
35 | 34 | oveq2d 7287 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎)) = (𝐹(.r‘𝑅)(0g‘𝑅))) |
36 | | eqid 2740 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
37 | 5, 23, 36 | ringrz 19825 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
38 | 37 | 3adant3 1131 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
39 | 38 | adantr 481 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
40 | 26, 35, 39 | 3eqtrd 2784 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (0g‘𝑅)) |
41 | 17, 40 | suppss 8001 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)) ⊆
((coe1‘𝐺)
supp (0g‘𝑅))) |
42 | | suppssdm 7984 |
. . . . 5
⊢
((coe1‘𝐺) supp (0g‘𝑅)) ⊆ dom
(coe1‘𝐺) |
43 | 42, 29 | fssdm 6618 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℕ0) |
44 | | nn0ssre 12237 |
. . . . 5
⊢
ℕ0 ⊆ ℝ |
45 | | ressxr 11020 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
46 | 44, 45 | sstri 3935 |
. . . 4
⊢
ℕ0 ⊆ ℝ* |
47 | 43, 46 | sstrdi 3938 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℝ*) |
48 | | supxrss 13065 |
. . 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 25259 |
. . 3
⊢ (((𝐴‘𝐹) · 𝐺) ∈ 𝐵 → (𝐷‘((𝐴‘𝐹) · 𝐺)) = sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, <
)) |
52 | 14, 51 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) = sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, <
)) |
53 | 50, 1, 6, 36, 27 | deg1val 25259 |
. . 3
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) = sup(((coe1‘𝐺) supp
(0g‘𝑅)),
ℝ*, < )) |
54 | 53 | 3ad2ant3 1134 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐺) = sup(((coe1‘𝐺) supp
(0g‘𝑅)),
ℝ*, < )) |
55 | 49, 52, 54 | 3brtr4d 5111 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) ≤ (𝐷‘𝐺)) |