Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . 7
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
2 | | mdegvscale.p |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑌) |
3 | | mdegvscale.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝑅) |
4 | | mdegvscale.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑌) |
5 | | eqid 2738 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
6 | | eqid 2738 |
. . . . . . 7
⊢ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin} |
7 | | mdegvscale.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ 𝐾) |
8 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐹 ∈ 𝐾) |
9 | | mdegvscale.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐺 ∈ 𝐵) |
11 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
12 | 1, 2, 3, 4, 5, 6, 8, 10, 11 | mplvscaval 21220 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹 · 𝐺)‘𝑥) = (𝐹(.r‘𝑅)(𝐺‘𝑥))) |
13 | 12 | adantrr 714 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) → ((𝐹 · 𝐺)‘𝑥) = (𝐹(.r‘𝑅)(𝐺‘𝑥))) |
14 | | mdegaddle.d |
. . . . . . 7
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
15 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝑅) = (0g‘𝑅) |
16 | | eqid 2738 |
. . . . . . 7
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
17 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) → 𝐺 ∈ 𝐵) |
18 | | simprl 768 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) → 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
19 | | simprr 770 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) → (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥)) |
20 | 14, 1, 4, 15, 6, 16, 17, 18, 19 | mdeglt 25230 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) → (𝐺‘𝑥) = (0g‘𝑅)) |
21 | 20 | oveq2d 7291 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) → (𝐹(.r‘𝑅)(𝐺‘𝑥)) = (𝐹(.r‘𝑅)(0g‘𝑅))) |
22 | | mdegaddle.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
23 | 3, 5, 15 | ringrz 19827 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
24 | 22, 7, 23 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
25 | 24 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) → (𝐹(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
26 | 13, 21, 25 | 3eqtrd 2782 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥))) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)) |
27 | 26 | expr 457 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅))) |
28 | 27 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ((𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅))) |
29 | | mdegaddle.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
30 | 1 | mpllmod 21223 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ LMod) |
31 | 29, 22, 30 | syl2anc 584 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ LMod) |
32 | 1, 29, 22 | mplsca 21217 |
. . . . . . 7
⊢ (𝜑 → 𝑅 = (Scalar‘𝑌)) |
33 | 32 | fveq2d 6778 |
. . . . . 6
⊢ (𝜑 → (Base‘𝑅) =
(Base‘(Scalar‘𝑌))) |
34 | 3, 33 | eqtrid 2790 |
. . . . 5
⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑌))) |
35 | 7, 34 | eleqtrd 2841 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (Base‘(Scalar‘𝑌))) |
36 | | eqid 2738 |
. . . . 5
⊢
(Scalar‘𝑌) =
(Scalar‘𝑌) |
37 | | eqid 2738 |
. . . . 5
⊢
(Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌)) |
38 | 4, 36, 2, 37 | lmodvscl 20140 |
. . . 4
⊢ ((𝑌 ∈ LMod ∧ 𝐹 ∈
(Base‘(Scalar‘𝑌)) ∧ 𝐺 ∈ 𝐵) → (𝐹 · 𝐺) ∈ 𝐵) |
39 | 31, 35, 9, 38 | syl3anc 1370 |
. . 3
⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵) |
40 | 14, 1, 4 | mdegxrcl 25232 |
. . . 4
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) ∈
ℝ*) |
41 | 9, 40 | syl 17 |
. . 3
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℝ*) |
42 | 14, 1, 4, 15, 6, 16 | mdegleb 25229 |
. . 3
⊢ (((𝐹 · 𝐺) ∈ 𝐵 ∧ (𝐷‘𝐺) ∈ ℝ*) → ((𝐷‘(𝐹 · 𝐺)) ≤ (𝐷‘𝐺) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ((𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)))) |
43 | 39, 41, 42 | syl2anc 584 |
. 2
⊢ (𝜑 → ((𝐷‘(𝐹 · 𝐺)) ≤ (𝐷‘𝐺) ↔ ∀𝑥 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ((𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)))) |
44 | 28, 43 | mpbird 256 |
1
⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐷‘𝐺)) |