Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . . 8
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
2 | | mdegmulle2.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑌) |
3 | | eqid 2778 |
. . . . . . . 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 19940 |
. . . . . . 7
⊢ (𝜑 → (𝐹 · 𝐺) = (𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))) |
9 | 8 | fveq1d 6503 |
. . . . . 6
⊢ (𝜑 → ((𝐹 · 𝐺)‘𝑥) = ((𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))‘𝑥)) |
10 | 9 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → ((𝐹 · 𝐺)‘𝑥) = ((𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))‘𝑥)) |
11 | | breq2 4934 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑥 → (𝑒 ∘𝑟 ≤ 𝑐 ↔ 𝑒 ∘𝑟 ≤ 𝑥)) |
12 | 11 | rabbidv 3403 |
. . . . . . . . 9
⊢ (𝑐 = 𝑥 → {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} = {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) |
13 | | fvoveq1 7001 |
. . . . . . . . . 10
⊢ (𝑐 = 𝑥 → (𝐺‘(𝑐 ∘𝑓 − 𝑑)) = (𝐺‘(𝑥 ∘𝑓 − 𝑑))) |
14 | 13 | oveq2d 6994 |
. . . . . . . . 9
⊢ (𝑐 = 𝑥 → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))) = ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))) |
15 | 12, 14 | mpteq12dv 5013 |
. . . . . . . 8
⊢ (𝑐 = 𝑥 → (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑)))) = (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))))) |
16 | 15 | oveq2d 6994 |
. . . . . . 7
⊢ (𝑐 = 𝑥 → (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))) = (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))))) |
17 | | eqid 2778 |
. . . . . . 7
⊢ (𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑)))))) = (𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑)))))) |
18 | | ovex 7010 |
. . . . . . 7
⊢ (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))))) ∈ V |
19 | 16, 17, 18 | fvmpt 6597 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → ((𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))‘𝑥) = (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))))) |
20 | 19 | ad2antrl 715 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → ((𝑐 ∈ 𝐴 ↦ (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑐} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑐 ∘𝑓 − 𝑑))))))‘𝑥) = (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))))) |
21 | | mdegaddle.d |
. . . . . . . . . . . . 13
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
22 | | eqid 2778 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑅) = (0g‘𝑅) |
23 | | mdegmullem.h |
. . . . . . . . . . . . 13
⊢ 𝐻 = (𝑏 ∈ 𝐴 ↦ (ℂfld
Σg 𝑏)) |
24 | 6 | ad2antrr 713 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → 𝐹 ∈ 𝐵) |
25 | | elrabi 3590 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} → 𝑑 ∈ 𝐴) |
26 | 25 | adantl 474 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝑑 ∈ 𝐴) |
27 | 26 | adantrr 704 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → 𝑑 ∈ 𝐴) |
28 | 21, 1, 2 | mdegxrcl 24367 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈
ℝ*) |
29 | 6, 28 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℝ*) |
30 | 29 | ad2antrr 713 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐷‘𝐹) ∈
ℝ*) |
31 | | nn0ssre 11714 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 ⊆ ℝ |
32 | | ressxr 10486 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ
⊆ ℝ* |
33 | 31, 32 | sstri 3869 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 ⊆ ℝ* |
34 | | mdegmulle2.j1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
35 | 33, 34 | sseldi 3858 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐽 ∈
ℝ*) |
36 | 35 | ad2antrr 713 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐽 ∈
ℝ*) |
37 | | mdegaddle.i |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
38 | 5, 23 | tdeglem1 24358 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐼 ∈ 𝑉 → 𝐻:𝐴⟶ℕ0) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐻:𝐴⟶ℕ0) |
40 | 39 | ad2antrr 713 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐻:𝐴⟶ℕ0) |
41 | 40, 26 | ffvelrnd 6679 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑑) ∈
ℕ0) |
42 | 33, 41 | sseldi 3858 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑑) ∈
ℝ*) |
43 | 30, 36, 42 | 3jca 1108 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐷‘𝐹) ∈ ℝ* ∧ 𝐽 ∈ ℝ*
∧ (𝐻‘𝑑) ∈
ℝ*)) |
44 | 43 | adantrr 704 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((𝐷‘𝐹) ∈ ℝ* ∧ 𝐽 ∈ ℝ*
∧ (𝐻‘𝑑) ∈
ℝ*)) |
45 | | mdegmulle2.j2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘𝐹) ≤ 𝐽) |
46 | 45 | ad2antrr 713 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐷‘𝐹) ≤ 𝐽) |
47 | 46 | anim1i 605 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) ∧ 𝐽 < (𝐻‘𝑑)) → ((𝐷‘𝐹) ≤ 𝐽 ∧ 𝐽 < (𝐻‘𝑑))) |
48 | 47 | anasss 459 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((𝐷‘𝐹) ≤ 𝐽 ∧ 𝐽 < (𝐻‘𝑑))) |
49 | | xrlelttr 12369 |
. . . . . . . . . . . . . 14
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ 𝐽 ∈ ℝ*
∧ (𝐻‘𝑑) ∈ ℝ*)
→ (((𝐷‘𝐹) ≤ 𝐽 ∧ 𝐽 < (𝐻‘𝑑)) → (𝐷‘𝐹) < (𝐻‘𝑑))) |
50 | 44, 48, 49 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → (𝐷‘𝐹) < (𝐻‘𝑑)) |
51 | 21, 1, 2, 22, 5, 23, 24, 27, 50 | mdeglt 24365 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → (𝐹‘𝑑) = (0g‘𝑅)) |
52 | 51 | oveq1d 6993 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) =
((0g‘𝑅)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))) |
53 | | mdegaddle.r |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ Ring) |
54 | 53 | ad2antrr 713 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝑅 ∈ Ring) |
55 | | eqid 2778 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝑅) =
(Base‘𝑅) |
56 | 1, 55, 2, 5, 7 | mplelf 19930 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐺:𝐴⟶(Base‘𝑅)) |
57 | 56 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐺:𝐴⟶(Base‘𝑅)) |
58 | | ssrab2 3948 |
. . . . . . . . . . . . . . 15
⊢ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ⊆ 𝐴 |
59 | 37 | ad2antrr 713 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐼 ∈ 𝑉) |
60 | | simplrl 764 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝑥 ∈ 𝐴) |
61 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) |
62 | | eqid 2778 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} = {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} |
63 | 5, 62 | psrbagconcl 19870 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑑) ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) |
64 | 59, 60, 61, 63 | syl3anc 1351 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑑) ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) |
65 | 58, 64 | sseldi 3858 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝑥 ∘𝑓 − 𝑑) ∈ 𝐴) |
66 | 57, 65 | ffvelrnd 6679 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐺‘(𝑥 ∘𝑓 − 𝑑)) ∈ (Base‘𝑅)) |
67 | 55, 3, 22 | ringlz 19063 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝐺‘(𝑥 ∘𝑓 − 𝑑)) ∈ (Base‘𝑅)) →
((0g‘𝑅)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
68 | 54, 66, 67 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) →
((0g‘𝑅)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
69 | 68 | adantrr 704 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((0g‘𝑅)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
70 | 52, 69 | eqtrd 2814 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐽 < (𝐻‘𝑑))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
71 | 70 | anassrs 460 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) ∧ 𝐽 < (𝐻‘𝑑)) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
72 | 7 | ad2antrr 713 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → 𝐺 ∈ 𝐵) |
73 | 65 | adantrr 704 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → (𝑥 ∘𝑓 − 𝑑) ∈ 𝐴) |
74 | 21, 1, 2 | mdegxrcl 24367 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) ∈
ℝ*) |
75 | 7, 74 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℝ*) |
76 | 75 | ad2antrr 713 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐷‘𝐺) ∈
ℝ*) |
77 | | mdegmulle2.k1 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
78 | 33, 77 | sseldi 3858 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈
ℝ*) |
79 | 78 | ad2antrr 713 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐾 ∈
ℝ*) |
80 | 40, 65 | ffvelrnd 6679 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ∈
ℕ0) |
81 | 33, 80 | sseldi 3858 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ∈
ℝ*) |
82 | 76, 79, 81 | 3jca 1108 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐷‘𝐺) ∈ ℝ* ∧ 𝐾 ∈ ℝ*
∧ (𝐻‘(𝑥 ∘𝑓
− 𝑑)) ∈
ℝ*)) |
83 | 82 | adantrr 704 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐷‘𝐺) ∈ ℝ* ∧ 𝐾 ∈ ℝ*
∧ (𝐻‘(𝑥 ∘𝑓
− 𝑑)) ∈
ℝ*)) |
84 | | mdegmulle2.k2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷‘𝐺) ≤ 𝐾) |
85 | 84 | ad2antrr 713 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐷‘𝐺) ≤ 𝐾) |
86 | 85 | anim1i 605 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) → ((𝐷‘𝐺) ≤ 𝐾 ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
87 | 86 | anasss 459 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐷‘𝐺) ≤ 𝐾 ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
88 | | xrlelttr 12369 |
. . . . . . . . . . . . . 14
⊢ (((𝐷‘𝐺) ∈ ℝ* ∧ 𝐾 ∈ ℝ*
∧ (𝐻‘(𝑥 ∘𝑓
− 𝑑)) ∈
ℝ*) → (((𝐷‘𝐺) ≤ 𝐾 ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) → (𝐷‘𝐺) < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
89 | 83, 87, 88 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → (𝐷‘𝐺) < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) |
90 | 21, 1, 2, 22, 5, 23, 72, 73, 89 | mdeglt 24365 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → (𝐺‘(𝑥 ∘𝑓 − 𝑑)) = (0g‘𝑅)) |
91 | 90 | oveq2d 6994 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = ((𝐹‘𝑑)(.r‘𝑅)(0g‘𝑅))) |
92 | 1, 55, 2, 5, 6 | mplelf 19930 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐴⟶(Base‘𝑅)) |
93 | 92 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐹:𝐴⟶(Base‘𝑅)) |
94 | 93, 26 | ffvelrnd 6679 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐹‘𝑑) ∈ (Base‘𝑅)) |
95 | 55, 3, 22 | ringrz 19064 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Ring ∧ (𝐹‘𝑑) ∈ (Base‘𝑅)) → ((𝐹‘𝑑)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
96 | 54, 94, 95 | syl2anc 576 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐹‘𝑑)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
97 | 96 | adantrr 704 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐹‘𝑑)(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
98 | 91, 97 | eqtrd 2814 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
99 | 98 | anassrs 460 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) ∧ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
100 | | simplrr 765 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐽 + 𝐾) < (𝐻‘𝑥)) |
101 | 41 | nn0red 11771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑑) ∈ ℝ) |
102 | 80 | nn0red 11771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ∈
ℝ) |
103 | 34 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐽 ∈
ℕ0) |
104 | 103 | nn0red 11771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐽 ∈ ℝ) |
105 | 77 | ad2antrr 713 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐾 ∈
ℕ0) |
106 | 105 | nn0red 11771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → 𝐾 ∈ ℝ) |
107 | | le2add 10925 |
. . . . . . . . . . . . 13
⊢ ((((𝐻‘𝑑) ∈ ℝ ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ∈ ℝ) ∧ (𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ)) →
(((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) → ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑))) ≤ (𝐽 + 𝐾))) |
108 | 101, 102,
104, 106, 107 | syl22anc 826 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) → ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑))) ≤ (𝐽 + 𝐾))) |
109 | 5, 23 | tdeglem3 24359 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ (𝑥 ∘𝑓 − 𝑑) ∈ 𝐴) → (𝐻‘(𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑))) = ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
110 | 59, 26, 65, 109 | syl3anc 1351 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑))) = ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
111 | 5 | psrbagf 19862 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴) → 𝑑:𝐼⟶ℕ0) |
112 | 111 | 3adant3 1112 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑑:𝐼⟶ℕ0) |
113 | 112 | ffvelrnda 6678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑑‘𝑏) ∈
ℕ0) |
114 | 113 | nn0cnd 11772 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑑‘𝑏) ∈ ℂ) |
115 | 5 | psrbagf 19862 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴) → 𝑥:𝐼⟶ℕ0) |
116 | 115 | 3adant2 1111 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥:𝐼⟶ℕ0) |
117 | 116 | ffvelrnda 6678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈
ℕ0) |
118 | 117 | nn0cnd 11772 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ ℂ) |
119 | 114, 118 | pncan3d 10803 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → ((𝑑‘𝑏) + ((𝑥‘𝑏) − (𝑑‘𝑏))) = (𝑥‘𝑏)) |
120 | 119 | mpteq2dva 5023 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑏 ∈ 𝐼 ↦ ((𝑑‘𝑏) + ((𝑥‘𝑏) − (𝑑‘𝑏)))) = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏))) |
121 | | simp1 1116 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝐼 ∈ 𝑉) |
122 | | fvexd 6516 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑑‘𝑏) ∈ V) |
123 | | ovexd 7012 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → ((𝑥‘𝑏) − (𝑑‘𝑏)) ∈ V) |
124 | 112 | feqmptd 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑑 = (𝑏 ∈ 𝐼 ↦ (𝑑‘𝑏))) |
125 | | fvexd 6516 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ 𝑏 ∈ 𝐼) → (𝑥‘𝑏) ∈ V) |
126 | 116 | feqmptd 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → 𝑥 = (𝑏 ∈ 𝐼 ↦ (𝑥‘𝑏))) |
127 | 121, 125,
122, 126, 124 | offval2 7246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∘𝑓 − 𝑑) = (𝑏 ∈ 𝐼 ↦ ((𝑥‘𝑏) − (𝑑‘𝑏)))) |
128 | 121, 122,
123, 124, 127 | offval2 7246 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑)) = (𝑏 ∈ 𝐼 ↦ ((𝑑‘𝑏) + ((𝑥‘𝑏) − (𝑑‘𝑏))))) |
129 | 120, 128,
126 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑑 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑)) = 𝑥) |
130 | 59, 26, 60, 129 | syl3anc 1351 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑)) = 𝑥) |
131 | 130 | fveq2d 6505 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘(𝑑 ∘𝑓 + (𝑥 ∘𝑓
− 𝑑))) = (𝐻‘𝑥)) |
132 | 110, 131 | eqtr3d 2816 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑))) = (𝐻‘𝑥)) |
133 | 132 | breq1d 4940 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) + (𝐻‘(𝑥 ∘𝑓 − 𝑑))) ≤ (𝐽 + 𝐾) ↔ (𝐻‘𝑥) ≤ (𝐽 + 𝐾))) |
134 | 108, 133 | sylibd 231 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) → (𝐻‘𝑥) ≤ (𝐽 + 𝐾))) |
135 | 101, 104 | lenltd 10588 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐻‘𝑑) ≤ 𝐽 ↔ ¬ 𝐽 < (𝐻‘𝑑))) |
136 | 102, 106 | lenltd 10588 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾 ↔ ¬ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
137 | 135, 136 | anbi12d 621 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) ↔ (¬ 𝐽 < (𝐻‘𝑑) ∧ ¬ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))))) |
138 | | ioran 966 |
. . . . . . . . . . . 12
⊢ (¬
(𝐽 < (𝐻‘𝑑) ∨ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) ↔ (¬ 𝐽 < (𝐻‘𝑑) ∧ ¬ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
139 | 137, 138 | syl6bbr 281 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (((𝐻‘𝑑) ≤ 𝐽 ∧ (𝐻‘(𝑥 ∘𝑓 − 𝑑)) ≤ 𝐾) ↔ ¬ (𝐽 < (𝐻‘𝑑) ∨ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))))) |
140 | 40, 60 | ffvelrnd 6679 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑥) ∈
ℕ0) |
141 | 140 | nn0red 11771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐻‘𝑥) ∈ ℝ) |
142 | 34, 77 | nn0addcld 11774 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐽 + 𝐾) ∈
ℕ0) |
143 | 142 | ad2antrr 713 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐽 + 𝐾) ∈
ℕ0) |
144 | 143 | nn0red 11771 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐽 + 𝐾) ∈ ℝ) |
145 | 141, 144 | lenltd 10588 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐻‘𝑥) ≤ (𝐽 + 𝐾) ↔ ¬ (𝐽 + 𝐾) < (𝐻‘𝑥))) |
146 | 134, 139,
145 | 3imtr3d 285 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (¬ (𝐽 < (𝐻‘𝑑) ∨ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑))) → ¬ (𝐽 + 𝐾) < (𝐻‘𝑥))) |
147 | 100, 146 | mt4d 154 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → (𝐽 < (𝐻‘𝑑) ∨ 𝐾 < (𝐻‘(𝑥 ∘𝑓 − 𝑑)))) |
148 | 71, 99, 147 | mpjaodan 941 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) ∧ 𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥}) → ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))) = (0g‘𝑅)) |
149 | 148 | mpteq2dva 5023 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑)))) = (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦
(0g‘𝑅))) |
150 | 149 | oveq2d 6994 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))))) = (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦
(0g‘𝑅)))) |
151 | | ringmnd 19032 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) |
152 | 53, 151 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Mnd) |
153 | 152 | adantr 473 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → 𝑅 ∈ Mnd) |
154 | | ovex 7010 |
. . . . . . . 8
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
155 | 5, 154 | rab2ex 5095 |
. . . . . . 7
⊢ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∈ V |
156 | 22 | gsumz 17845 |
. . . . . . 7
⊢ ((𝑅 ∈ Mnd ∧ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ∈ V) → (𝑅 Σg
(𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
157 | 153, 155,
156 | sylancl 577 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦
(0g‘𝑅))) =
(0g‘𝑅)) |
158 | 150, 157 | eqtrd 2814 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → (𝑅 Σg (𝑑 ∈ {𝑒 ∈ 𝐴 ∣ 𝑒 ∘𝑟 ≤ 𝑥} ↦ ((𝐹‘𝑑)(.r‘𝑅)(𝐺‘(𝑥 ∘𝑓 − 𝑑))))) =
(0g‘𝑅)) |
159 | 10, 20, 158 | 3eqtrd 2818 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ (𝐽 + 𝐾) < (𝐻‘𝑥))) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)) |
160 | 159 | expr 449 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐽 + 𝐾) < (𝐻‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅))) |
161 | 160 | ralrimiva 3132 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ((𝐽 + 𝐾) < (𝐻‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅))) |
162 | 1 | mplring 19949 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring) |
163 | 37, 53, 162 | syl2anc 576 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ Ring) |
164 | 2, 4 | ringcl 19037 |
. . . 4
⊢ ((𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 · 𝐺) ∈ 𝐵) |
165 | 163, 6, 7, 164 | syl3anc 1351 |
. . 3
⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵) |
166 | 33, 142 | sseldi 3858 |
. . 3
⊢ (𝜑 → (𝐽 + 𝐾) ∈
ℝ*) |
167 | 21, 1, 2, 22, 5, 23 | mdegleb 24364 |
. . 3
⊢ (((𝐹 · 𝐺) ∈ 𝐵 ∧ (𝐽 + 𝐾) ∈ ℝ*) → ((𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾) ↔ ∀𝑥 ∈ 𝐴 ((𝐽 + 𝐾) < (𝐻‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)))) |
168 | 165, 166,
167 | syl2anc 576 |
. 2
⊢ (𝜑 → ((𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾) ↔ ∀𝑥 ∈ 𝐴 ((𝐽 + 𝐾) < (𝐻‘𝑥) → ((𝐹 · 𝐺)‘𝑥) = (0g‘𝑅)))) |
169 | 161, 168 | mpbird 249 |
1
⊢ (𝜑 → (𝐷‘(𝐹 · 𝐺)) ≤ (𝐽 + 𝐾)) |