Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . . 8
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
2 | | mdegmulle2.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) |
3 | | eqid 2610 |
. . . . . . . 8
⊢
(.r‘𝑅) = (.r‘𝑅) |
4 | | mdegmulle2.t |
. . . . . . . 8
⊢ · =
(.r‘𝑌) |
5 | | mdegmullem.a |
. . . . . . . 8
⊢ 𝐴 = {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
6 | | mdegmulle2.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
7 | | mdegmulle2.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
8 | 1, 2, 3, 4, 5, 6, 7 | mplmul 19264 |
. . . . . . 7
⊢ (𝜑 → (𝐹 · 𝐺) = (𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))) |
9 | 8 | fveq1d 6105 |
. . . . . 6
⊢ (𝜑 → ((𝐹 · 𝐺)‘𝑥) = ((𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))‘𝑥)) |
10 | 9 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → ((𝐹 · 𝐺)‘𝑥) = ((𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))‘𝑥)) |
11 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑥 → (𝑒 ∘𝑟 ≤ 𝑐 ↔ 𝑒 ∘𝑟 ≤ 𝑥)) |
12 | 11 | rabbidv 3164 |
. . . . . . . . 9
⊢ (𝑐 = 𝑥 → {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} = {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) |
13 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝑥 → (𝑐 ∘𝑓 − 𝑑) = (𝑥 ∘𝑓 − 𝑑)) |
14 | 13 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑥 → (𝐺‘(𝑐 ∘𝑓 − 𝑑)) = (𝐺‘(𝑥 ∘𝑓 − 𝑑))) |
15 | 14 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑐 = 𝑥 → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))) = ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))) |
16 | 12, 15 | mpteq12dv 4663 |
. . . . . . . 8
⊢ (𝑐 = 𝑥 → (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑)))) = (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))))) |
17 | 16 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑐 = 𝑥 → (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))) = (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))))) |
18 | | eqid 2610 |
. . . . . . 7
⊢ (𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑)))))) = (𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑)))))) |
19 | | ovex 6577 |
. . . . . . 7
⊢ (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))))) ∈ V |
20 | 17, 18, 19 | fvmpt 6191 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → ((𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))‘𝑥) = (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))))) |
21 | 20 | ad2antrl 760 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → ((𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))‘𝑥) = (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))))) |
22 | | mdegaddle.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
23 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) |
24 | | mdegmullem.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (𝑏 ∈ 𝐴 ↦ (ℂfld
Σg 𝑏)) |
25 | 6 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → 𝐹 ∈ 𝐵) |
26 | | elrabi 3328 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} → 𝑑 ∈ 𝐴) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝑑 ∈ 𝐴) |
28 | 27 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → 𝑑 ∈ 𝐴) |
29 | 22, 1, 2 | mdegxrcl 23631 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈
ℝ*) |
30 | 6, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℝ*) |
31 | 30 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐷‘𝐹) ∈
ℝ*) |
32 | | nn0ssre 11173 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 ⊆ ℝ |
33 | | ressxr 9962 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ
⊆ ℝ* |
34 | 32, 33 | sstri 3577 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 ⊆ ℝ* |
35 | | mdegmulle2.j1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
36 | 34, 35 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐽 ∈
ℝ*) |
37 | 36 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐽 ∈
ℝ*) |
38 | | mdegaddle.i |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
39 | 5, 24 | tdeglem1 23622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ 𝑉 → 𝐻:𝐴⟶ℕ0) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐻:𝐴⟶ℕ0) |
41 | 40 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐻:𝐴⟶ℕ0) |
42 | 41, 27 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑑) ∈
ℕ0) |
43 | 34, 42 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑑) ∈
ℝ*) |
44 | 31, 37, 43 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐷‘𝐹) ∈ ℝ* ∧ 𝐽 ∈ ℝ*
∧ (𝐻‘𝑑) ∈
ℝ*)) |
45 | 44 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((𝐷‘𝐹) ∈ ℝ* ∧ 𝐽 ∈ ℝ*
∧ (𝐻‘𝑑) ∈
ℝ*)) |
46 | | mdegmulle2.j2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) |
47 | 46 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐷‘𝐹) ≤ 𝐽) |
48 | 47 | anim1i 590 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) ∧ 𝐽 < (𝐻‘𝑑)) → ((𝐷‘𝐹) ≤ 𝐽 ∧ 𝐽 < (𝐻‘𝑑))) |
49 | 48 | anasss 677 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((𝐷‘𝐹) ≤ 𝐽 ∧ 𝐽 < (𝐻‘𝑑))) |
50 | | xrlelttr 11863 |
. . . . . . . . . . . . . 14
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ 𝐽 ∈ ℝ*
∧ (𝐻‘𝑑) ∈ ℝ*)
→ (((𝐷‘𝐹) ≤ 𝐽 ∧ 𝐽 < (𝐻‘𝑑)) → (𝐷‘𝐹) < (𝐻‘𝑑))) |
51 | 45, 49, 50 | sylc 63 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → (𝐷‘𝐹) < (𝐻‘𝑑)) |
52 | 22, 1, 2, 23, 5, 24, 25, 28, 51 | mdeglt 23629 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → (𝐹‘𝑑) = (0g‘𝑅)) |
53 | 52 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) =
((0g‘𝑅)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))) |
54 | | mdegaddle.r |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ Ring) |
55 | 54 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝑅 ∈ Ring) |
56 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑅) =
(Base‘𝑅) |
57 | 1, 56, 2, 5, 7 | mplelf 19254 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝐴⟶(Base‘𝑅)) |
58 | 57 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐺:𝐴⟶(Base‘𝑅)) |
59 | | ssrab2 3650 |
. . . . . . . . . . . . . . 15
⊢ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ⊆ 𝐴 |
60 | 38 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐼 ∈ 𝑉) |
61 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝑥 ∈ 𝐴) |
62 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) |
63 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} = {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} |
64 | 5, 63 | psrbagconcl 19194 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑑) ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) |
65 | 60, 61, 62, 64 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑑) ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) |
66 | 59, 65 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑑) ∈ 𝐴) |
67 | 58, 66 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐺‘(𝑥 ∘𝑓 − 𝑑)) ∈ (Base‘𝑅)) |
68 | 56, 3, 23 | ringlz 18410 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝐺‘(𝑥 ∘𝑓 − 𝑑)) ∈ (Base‘𝑅)) →
((0g‘𝑅)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
69 | 55, 67, 68 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) →
((0g‘𝑅)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
70 | 69 | adantrr 749 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((0g‘𝑅)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
71 | 53, 70 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
72 | 71 | anassrs 678 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) ∧ 𝐽 < (𝐻‘𝑑)) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
73 | 7 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → 𝐺 ∈ 𝐵) |
74 | 66 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → (𝑥 ∘𝑓 − 𝑑) ∈ 𝐴) |
75 | 22, 1, 2 | mdegxrcl 23631 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) ∈
ℝ*) |
76 | 7, 75 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℝ*) |
77 | 76 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐷‘𝐺) ∈
ℝ*) |
78 | | mdegmulle2.k1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
79 | 34, 78 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈
ℝ*) |
80 | 79 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐾 ∈
ℝ*) |
81 | 41, 66 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ∈
ℕ0) |
82 | 34, 81 | sseldi 3566 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ∈
ℝ*) |
83 | 77, 80, 82 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐷‘𝐺) ∈ ℝ* ∧ 𝐾 ∈ ℝ*
∧ (𝐻‘(𝑥 ∘𝑓
− 𝑑)) ∈
ℝ*)) |
84 | 83 | adantrr 749 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐷‘𝐺) ∈ ℝ* ∧ 𝐾 ∈ ℝ*
∧ (𝐻‘(𝑥 ∘𝑓
− 𝑑)) ∈
ℝ*)) |
85 | | mdegmulle2.k2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) |
86 | 85 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐷‘𝐺) ≤ 𝐾) |
87 | 86 | anim1i 590 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) → ((𝐷‘𝐺) ≤ 𝐾 ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
88 | 87 | anasss 677 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐷‘𝐺) ≤ 𝐾 ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
89 | | xrlelttr 11863 |
. . . . . . . . . . . . . 14
⊢ (((𝐷‘𝐺) ∈ ℝ* ∧ 𝐾 ∈ ℝ*
∧ (𝐻‘(𝑥 ∘𝑓
− 𝑑)) ∈
ℝ*) → (((𝐷‘𝐺) ≤ 𝐾 ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) → (𝐷‘𝐺) < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
90 | 84, 88, 89 | sylc 63 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → (𝐷‘𝐺) < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) |
91 | 22, 1, 2, 23, 5, 24, 73, 74, 90 | mdeglt 23629 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → (𝐺‘(𝑥 ∘𝑓 − 𝑑)) = (0g‘𝑅)) |
92 | 91 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = ((𝐹‘𝑑)(.r‘𝑅)(0g‘𝑅))) |
93 | 1, 56, 2, 5, 6 | mplelf 19254 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝑅)) |
94 | 93 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐹:𝐴⟶(Base‘𝑅)) |
95 | 94, 27 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐹‘𝑑) ∈ (Base‘𝑅)) |
96 | 56, 3, 23 | ringrz 18411 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝐹‘𝑑) ∈ (Base‘𝑅)) → ((𝐹‘𝑑)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
97 | 55, 95, 96 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐹‘𝑑)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
98 | 97 | adantrr 749 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐹‘𝑑)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
99 | 92, 98 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
100 | 99 | anassrs 678 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
101 | | simplrr 797 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐽 + 𝐾) < (𝐻‘𝑥)) |
102 | 42 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑑) ∈ ℝ) |
103 | 81 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ∈
ℝ) |
104 | 35 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐽 ∈
ℕ0) |
105 | 104 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐽 ∈ ℝ) |
106 | 78 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐾 ∈
ℕ0) |
107 | 106 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐾 ∈ ℝ) |
108 | | le2add 10389 |
. . . . . . . . . . . . 13
⊢ ((((𝐻‘𝑑) ∈ ℝ ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ∈ ℝ) ∧ (𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ)) →
(((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) → ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑))) ≤ (𝐽 + 𝐾))) |
109 | 102, 103,
105, 107, 108 | syl22anc 1319 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) → ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑))) ≤ (𝐽 + 𝐾))) |
110 | 5, 24 | tdeglem3 23623 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ (𝑥 ∘𝑓 − 𝑑) ∈ 𝐴) → (𝐻‘(𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑))) = ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
111 | 60, 27, 66, 110 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑))) = ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
112 | 5 | psrbagf 19186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴) → 𝑑:𝐼⟶ℕ0) |
113 | 112 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑑:𝐼⟶ℕ0) |
114 | 113 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑑‘𝑏) ∈
ℕ0) |
115 | 114 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑑‘𝑏) ∈ ℂ) |
116 | 5 | psrbagf 19186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝑥:𝐼⟶ℕ0) |
117 | 116 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥:𝐼⟶ℕ0) |
118 | 117 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈
ℕ0) |
119 | 118 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℂ) |
120 | 115, 119 | pncan3d 10274 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → ((𝑑‘𝑏) + ((𝑥‘𝑏) − (𝑑‘𝑏))) = (𝑥‘𝑏)) |
121 | 120 | mpteq2dva 4672 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑏 ∈ 𝐼 ↦ ((𝑑‘𝑏) + ((𝑥‘𝑏) − (𝑑‘𝑏)))) = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏))) |
122 | | simp1 1054 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐼 ∈ 𝑉) |
123 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑‘𝑏) ∈ V |
124 | 123 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑑‘𝑏) ∈ V) |
125 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥‘𝑏) − (𝑑‘𝑏)) ∈ V |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → ((𝑥‘𝑏) − (𝑑‘𝑏)) ∈ V) |
127 | 113 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑑 = (𝑏 ∈ 𝐼 ↦ (𝑑‘𝑏))) |
128 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥‘𝑏) ∈ V |
129 | 128 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ V) |
130 | 117 | feqmptd 6159 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏))) |
131 | 122, 129,
124, 130, 127 | offval2 6812 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∘𝑓 − 𝑑) = (𝑏 ∈ 𝐼 ↦ ((𝑥‘𝑏) − (𝑑‘𝑏)))) |
132 | 122, 124,
126, 127, 131 | offval2 6812 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑)) = (𝑏 ∈ 𝐼 ↦ ((𝑑‘𝑏) + ((𝑥‘𝑏) − (𝑑‘𝑏))))) |
133 | 121, 132,
130 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑)) = 𝑥) |
134 | 60, 27, 61, 133 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑)) = 𝑥) |
135 | 134 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑))) = (𝐻‘𝑥)) |
136 | 111, 135 | eqtr3d 2646 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑))) = (𝐻‘𝑥)) |
137 | 136 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑))) ≤ (𝐽 + 𝐾) ↔ (𝐻‘𝑥) ≤ (𝐽 + 𝐾))) |
138 | 109, 137 | sylibd 228 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) → (𝐻‘𝑥) ≤ (𝐽 + 𝐾))) |
139 | 102, 105 | lenltd 10062 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐻‘𝑑) ≤ 𝐽 ↔ ¬ 𝐽 < (𝐻‘𝑑))) |
140 | 103, 107 | lenltd 10062 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾 ↔ ¬ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
141 | 139, 140 | anbi12d 743 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) ↔ (¬ 𝐽 < (𝐻‘𝑑) ∧ ¬ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))))) |
142 | | ioran 510 |
. . . . . . . . . . . 12
⊢ (¬
(𝐽 < (𝐻‘𝑑) ∨ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) ↔ (¬ 𝐽 < (𝐻‘𝑑) ∧ ¬ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
143 | 141, 142 | syl6bbr 277 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) ↔ ¬ (𝐽 < (𝐻‘𝑑) ∨ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))))) |
144 | 41, 61 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑥) ∈
ℕ0) |
145 | 144 | nn0red 11229 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑥) ∈ ℝ) |
146 | 35, 78 | nn0addcld 11232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 + 𝐾) ∈
ℕ0) |
147 | 146 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐽 + 𝐾) ∈
ℕ0) |
148 | 147 | nn0red 11229 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐽 + 𝐾) ∈ ℝ) |
149 | 145, 148 | lenltd 10062 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐻‘𝑥) ≤ (𝐽 + 𝐾) ↔ ¬ (𝐽 + 𝐾) < (𝐻‘𝑥))) |
150 | 138, 143,
149 | 3imtr3d 281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (¬ (𝐽 < (𝐻‘𝑑) ∨ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) → ¬ (𝐽 + 𝐾) < (𝐻‘𝑥))) |
151 | 101, 150 | mt4d 151 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐽 < (𝐻‘𝑑) ∨ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
152 | 72, 100, 151 | mpjaodan 823 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
153 | 152 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))) = (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦
(0g‘𝑅))) |
154 | 153 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))))) = (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦
(0g‘𝑅)))) |
155 | | ringmnd 18379 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
156 | 54, 155 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Mnd) |
157 | 156 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → 𝑅 ∈ Mnd) |
158 | | ovex 6577 |
. . . . . . . 8
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
159 | 5, 158 | rab2ex 4743 |
. . . . . . 7
⊢ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∈ V |
160 | 23 | gsumz 17197 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∈ V) → (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
161 | 157, 159,
160 | sylancl 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
162 | 154, 161 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))))) =
(0g‘𝑅)) |
163 | 10, 21, 162 | 3eqtrd 2648 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)) |
164 | 163 | expr 641 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐽 + 𝐾) < (𝐻‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅))) |
165 | 164 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ((𝐽 + 𝐾) < (𝐻‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅))) |
166 | 1 | mplring 19273 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring) |
167 | 38, 54, 166 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ Ring) |
168 | 2, 4 | ringcl 18384 |
. . . 4
⊢ ((𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 · 𝐺) ∈ 𝐵) |
169 | 167, 6, 7, 168 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵) |
170 | 34, 146 | sseldi 3566 |
. . 3
⊢ (𝜑 → (𝐽 + 𝐾) ∈
ℝ*) |
171 | 22, 1, 2, 23, 5, 24 | mdegleb 23628 |
. . 3
⊢ (((𝐹 · 𝐺) ∈ 𝐵 ∧ (𝐽 + 𝐾) ∈ ℝ*) → ((𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾) ↔ ∀𝑥 ∈ 𝐴 ((𝐽 + 𝐾) < (𝐻‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)))) |
172 | 169, 170,
171 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾) ↔ ∀𝑥 ∈ 𝐴 ((𝐽 + 𝐾) < (𝐻‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)))) |
173 | 165, 172 | mpbird 246 |
1
⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) |