Step | Hyp | Ref
| Expression |
1 | | deg1mul3le.p |
. . . . . . . 8
⊢ 𝑃 = (Poly1‘𝑅) |
2 | 1 | ply1ring 19618 |
. . . . . . 7
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
3 | 2 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝑃 ∈ Ring) |
4 | | deg1mul3le.a |
. . . . . . . . 9
⊢ 𝐴 = (algSc‘𝑃) |
5 | | deg1mul3le.k |
. . . . . . . . 9
⊢ 𝐾 = (Base‘𝑅) |
6 | | deg1mul3le.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑃) |
7 | 1, 4, 5, 6 | ply1sclf 19655 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝐴:𝐾⟶𝐵) |
8 | 7 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐴:𝐾⟶𝐵) |
9 | | simp2 1062 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐹 ∈ 𝐾) |
10 | 8, 9 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐴‘𝐹) ∈ 𝐵) |
11 | | simp3 1063 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ 𝐵) |
12 | | deg1mul3le.t |
. . . . . . 7
⊢ · =
(.r‘𝑃) |
13 | 6, 12 | ringcl 18561 |
. . . . . 6
⊢ ((𝑃 ∈ Ring ∧ (𝐴‘𝐹) ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → ((𝐴‘𝐹) · 𝐺) ∈ 𝐵) |
14 | 3, 10, 11, 13 | syl3anc 1326 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((𝐴‘𝐹) · 𝐺) ∈ 𝐵) |
15 | | eqid 2622 |
. . . . . 6
⊢
(coe1‘((𝐴‘𝐹) · 𝐺)) = (coe1‘((𝐴‘𝐹) · 𝐺)) |
16 | 15, 6, 1, 5 | coe1f 19581 |
. . . . 5
⊢ (((𝐴‘𝐹) · 𝐺) ∈ 𝐵 → (coe1‘((𝐴‘𝐹) · 𝐺)):ℕ0⟶𝐾) |
17 | 14, 16 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (coe1‘((𝐴‘𝐹) · 𝐺)):ℕ0⟶𝐾) |
18 | | eldifi 3732 |
. . . . . 6
⊢ (𝑎 ∈ (ℕ0
∖ ((coe1‘𝐺) supp (0g‘𝑅))) → 𝑎 ∈ ℕ0) |
19 | | simpl1 1064 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝑅 ∈ Ring) |
20 | | simpl2 1065 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝐹 ∈ 𝐾) |
21 | | simpl3 1066 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝐺 ∈ 𝐵) |
22 | | simpr 477 |
. . . . . . 7
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) → 𝑎 ∈
ℕ0) |
23 | | eqid 2622 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
24 | 1, 6, 5, 4, 12, 23 | coe1sclmulfv 19653 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ (𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) →
((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
25 | 19, 20, 21, 22, 24 | syl121anc 1331 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ ℕ0) →
((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
26 | 18, 25 | sylan2 491 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎))) |
27 | | eqid 2622 |
. . . . . . . . 9
⊢
(coe1‘𝐺) = (coe1‘𝐺) |
28 | 27, 6, 1, 5 | coe1f 19581 |
. . . . . . . 8
⊢ (𝐺 ∈ 𝐵 → (coe1‘𝐺):ℕ0⟶𝐾) |
29 | 28 | 3ad2ant3 1084 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (coe1‘𝐺):ℕ0⟶𝐾) |
30 | | ssid 3624 |
. . . . . . . 8
⊢
((coe1‘𝐺) supp (0g‘𝑅)) ⊆
((coe1‘𝐺)
supp (0g‘𝑅)) |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ((coe1‘𝐺) supp (0g‘𝑅))) |
32 | | nn0ex 11298 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ℕ0 ∈
V) |
34 | | fvexd 6203 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (0g‘𝑅) ∈ V) |
35 | 29, 31, 33, 34 | suppssr 7326 |
. . . . . 6
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘𝐺)‘𝑎) = (0g‘𝑅)) |
36 | 35 | oveq2d 6666 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → (𝐹(.r‘𝑅)((coe1‘𝐺)‘𝑎)) = (𝐹(.r‘𝑅)(0g‘𝑅))) |
37 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
38 | 5, 23, 37 | ringrz 18588 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
39 | 38 | 3adant3 1081 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
40 | 39 | adantr 481 |
. . . . 5
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
41 | 26, 36, 40 | 3eqtrd 2660 |
. . . 4
⊢ (((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) ∧ 𝑎 ∈ (ℕ0 ∖
((coe1‘𝐺)
supp (0g‘𝑅)))) → ((coe1‘((𝐴‘𝐹) · 𝐺))‘𝑎) = (0g‘𝑅)) |
42 | 17, 41 | suppss 7325 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)) ⊆
((coe1‘𝐺)
supp (0g‘𝑅))) |
43 | | suppssdm 7308 |
. . . . 5
⊢
((coe1‘𝐺) supp (0g‘𝑅)) ⊆ dom
(coe1‘𝐺) |
44 | | fdm 6051 |
. . . . . 6
⊢
((coe1‘𝐺):ℕ0⟶𝐾 → dom
(coe1‘𝐺) =
ℕ0) |
45 | 29, 44 | syl 17 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → dom (coe1‘𝐺) =
ℕ0) |
46 | 43, 45 | syl5sseq 3653 |
. . . 4
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℕ0) |
47 | | nn0ssre 11296 |
. . . . 5
⊢
ℕ0 ⊆ ℝ |
48 | | ressxr 10083 |
. . . . 5
⊢ ℝ
⊆ ℝ* |
49 | 47, 48 | sstri 3612 |
. . . 4
⊢
ℕ0 ⊆ ℝ* |
50 | 46, 49 | syl6ss 3615 |
. . 3
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℝ*) |
51 | | supxrss 12162 |
. . 3
⊢
((((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)) ⊆
((coe1‘𝐺)
supp (0g‘𝑅)) ∧ ((coe1‘𝐺) supp
(0g‘𝑅))
⊆ ℝ*) → sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, < )
≤ sup(((coe1‘𝐺) supp (0g‘𝑅)), ℝ*, <
)) |
52 | 42, 50, 51 | syl2anc 693 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, < )
≤ sup(((coe1‘𝐺) supp (0g‘𝑅)), ℝ*, <
)) |
53 | | deg1mul3le.d |
. . . 4
⊢ 𝐷 = ( deg1
‘𝑅) |
54 | 53, 1, 6, 37, 15 | deg1val 23856 |
. . 3
⊢ (((𝐴‘𝐹) · 𝐺) ∈ 𝐵 → (𝐷‘((𝐴‘𝐹) · 𝐺)) = sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, <
)) |
55 | 14, 54 | syl 17 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) = sup(((coe1‘((𝐴‘𝐹) · 𝐺)) supp (0g‘𝑅)), ℝ*, <
)) |
56 | 53, 1, 6, 37, 27 | deg1val 23856 |
. . 3
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) = sup(((coe1‘𝐺) supp
(0g‘𝑅)),
ℝ*, < )) |
57 | 56 | 3ad2ant3 1084 |
. 2
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘𝐺) = sup(((coe1‘𝐺) supp
(0g‘𝑅)),
ℝ*, < )) |
58 | 52, 55, 57 | 3brtr4d 4685 |
1
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐺 ∈ 𝐵) → (𝐷‘((𝐴‘𝐹) · 𝐺)) ≤ (𝐷‘𝐺)) |