Step | Hyp | Ref
| Expression |
1 | | deg1mul3le.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
2 | 1 | ply1ring 21447 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
3 | 2 | 3ad2ant1 1131 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝑃 ∈ Ring) |
4 | | deg1mul3le.a |
. . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) |
5 | | deg1mul3le.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
6 | | deg1mul3le.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑃) |
7 | 1, 4, 5, 6 | ply1sclf 21484 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝐴:𝐾⟶𝐵) |
8 | 7 | 3ad2ant1 1131 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐴:𝐾⟶𝐵) |
9 | | simp2 1135 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐾) |
10 | 8, 9 | ffvelcdmd 6982 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐴‘𝐹) ∈ 𝐵) |
11 | | simp3 1136 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
12 | | deg1mul3le.t |
. . . . . . 7
⊢ · =
(.r‘𝑃) |
13 | 6, 12 | ringcl 19828 |
. . . . . 6
⊢ ((𝑃 ∈ Ring ∧ (𝐴‘𝐹) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐴‘𝐹) · 𝐺) ∈ 𝐵) |
14 | 3, 10, 11, 13 | syl3anc 1369 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((𝐴‘𝐹) · 𝐺) ∈ 𝐵) |
15 | | eqid 2733 |
. . . . . 6
⊢
(coe1‘((𝐴‘𝐹) · 𝐺)) = (coe1‘((𝐴‘𝐹) · 𝐺)) |
16 | 15, 6, 1, 5 | coe1f 21410 |
. . . . 5
⊢ (((𝐴‘𝐹) · 𝐺) ∈ 𝐵 → (coe1‘((𝐴‘𝐹) · 𝐺)):ℕ0⟶𝐾) |
17 | 14, 16 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (coe1‘((𝐴‘𝐹) · 𝐺)):ℕ0⟶𝐾) |
18 | | eldifi 4064 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
∖ ((coe1‘𝐺) supp (0g‘𝑅))) → 𝑎 ∈ ℕ0) |
19 | | simpl1 1189 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝑅 ∈ Ring) |
20 | | simpl2 1190 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝐹 ∈ 𝐾) |
21 | | simpl3 1191 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝐺 ∈ 𝐵) |
22 | | simpr 484 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝑎 ∈
ℕ0) |
23 | | eqid 2733 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
24 | 1, 6, 5, 4, 12, 23 | coe1sclmulfv 21482 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) →
((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
25 | 19, 20, 21, 22, 24 | syl121anc 1373 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) →
((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
26 | 18, 25 | sylan2 592 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
27 | | eqid 2733 |
. . . . . . . . 9
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
28 | 27, 6, 1, 5 | coe1f 21410 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝐵 → (coe1‘𝐺):ℕ0⟶𝐾) |
29 | 28 | 3ad2ant3 1133 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (coe1‘𝐺):ℕ0⟶𝐾) |
30 | | ssidd 3946 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ((coe1‘𝐺) supp (0g‘𝑅))) |
31 | | nn0ex 12267 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
32 | 31 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ℕ0 ∈
V) |
33 | | fvexd 6807 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (0g‘𝑅) ∈ V) |
34 | 29, 30, 32, 33 | suppssr 8032 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘𝐺)‘𝑎) = (0g‘𝑅)) |
35 | 34 | oveq2d 7311 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎)) = (𝐹(.r‘𝑅)(0g‘𝑅))) |
36 | | eqid 2733 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
37 | 5, 23, 36 | ringrz 19855 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
38 | 37 | 3adant3 1130 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
39 | 38 | adantr 480 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
40 | 26, 35, 39 | 3eqtrd 2777 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (0g‘𝑅)) |
41 | 17, 40 | suppss 8030 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)) ⊆
((coe1‘𝐺)
supp (0g‘𝑅))) |
42 | | suppssdm 8013 |
. . . . 5
⊢
((coe1‘𝐺) supp (0g‘𝑅)) ⊆ dom
(coe1‘𝐺) |
43 | 42, 29 | fssdm 6638 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℕ0) |
44 | | nn0ssre 12265 |
. . . . 5
⊢
ℕ0 ⊆ ℝ |
45 | | ressxr 11047 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
46 | 44, 45 | sstri 3932 |
. . . 4
⊢
ℕ0 ⊆ ℝ* |
47 | 43, 46 | sstrdi 3935 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℝ*) |
48 | | supxrss 13094 |
. . 3
⊢
((((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)) ⊆
((coe1‘𝐺)
supp (0g‘𝑅)) ∧ ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℝ*) → sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, < )
≤ sup(((coe1‘𝐺) supp (0g‘𝑅)), ℝ*, <
)) |
49 | 41, 47, 48 | syl2anc 583 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, < )
≤ sup(((coe1‘𝐺) supp (0g‘𝑅)), ℝ*, <
)) |
50 | | deg1mul3le.d |
. . . 4
⊢ 𝐷 = ( deg1
‘𝑅) |
51 | 50, 1, 6, 36, 15 | deg1val 25289 |
. . 3
⊢ (((𝐴‘𝐹) · 𝐺) ∈ 𝐵 → (𝐷‘((𝐴‘𝐹) · 𝐺)) = sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, <
)) |
52 | 14, 51 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) = sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, <
)) |
53 | 50, 1, 6, 36, 27 | deg1val 25289 |
. . 3
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) = sup(((coe1‘𝐺) supp
(0g‘𝑅)),
ℝ*, < )) |
54 | 53 | 3ad2ant3 1133 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐺) = sup(((coe1‘𝐺) supp
(0g‘𝑅)),
ℝ*, < )) |
55 | 49, 52, 54 | 3brtr4d 5109 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) ≤ (𝐷‘𝐺)) |