Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . . . . 10
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
2 | | mdegaddle.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑌) |
3 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | mdegaddle.p |
. . . . . . . . . 10
⊢ + =
(+g‘𝑌) |
5 | | mdegaddle.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
6 | | mdegaddle.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
7 | 1, 2, 3, 4, 5, 6 | mpladd 19263 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 + 𝐺) = (𝐹 ∘𝑓
(+g‘𝑅)𝐺)) |
8 | 7 | fveq1d 6105 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 + 𝐺)‘𝑐) = ((𝐹 ∘𝑓
(+g‘𝑅)𝐺)‘𝑐)) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹 + 𝐺)‘𝑐) = ((𝐹 ∘𝑓
(+g‘𝑅)𝐺)‘𝑐)) |
10 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
11 | | eqid 2610 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin} |
12 | 1, 10, 2, 11, 5 | mplelf 19254 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
13 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)
→ 𝐹 Fn {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐹 Fn {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
16 | 1, 10, 2, 11, 6 | mplelf 19254 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
17 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐺:{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)
→ 𝐺 Fn {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐺 Fn {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
20 | | ovex 6577 |
. . . . . . . . . 10
⊢
(ℕ0 ↑𝑚 𝐼) ∈ V |
21 | 20 | rabex 4740 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∈
V |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∈
V) |
23 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
24 | | fnfvof 6809 |
. . . . . . . 8
⊢ (((𝐹 Fn {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ 𝐺 Fn {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ ({𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∈ V ∧
𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin})) →
((𝐹
∘𝑓 (+g‘𝑅)𝐺)‘𝑐) = ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐))) |
25 | 15, 19, 22, 23, 24 | syl22anc 1319 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹 ∘𝑓
(+g‘𝑅)𝐺)‘𝑐) = ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐))) |
26 | 9, 25 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹 + 𝐺)‘𝑐) = ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐))) |
27 | 26 | adantrr 749 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐹 + 𝐺)‘𝑐) = ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐))) |
28 | | mdegaddle.d |
. . . . . . . 8
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
29 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
30 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
31 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → 𝐹 ∈ 𝐵) |
32 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}) |
33 | 28, 1, 2 | mdegxrcl 23631 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈
ℝ*) |
34 | 5, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℝ*) |
35 | 34 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝐷‘𝐹) ∈
ℝ*) |
36 | 28, 1, 2 | mdegxrcl 23631 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) ∈
ℝ*) |
37 | 6, 36 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℝ*) |
38 | 37, 34 | ifcld 4081 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈
ℝ*) |
39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) →
if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈
ℝ*) |
40 | | nn0ssre 11173 |
. . . . . . . . . . . . 13
⊢
ℕ0 ⊆ ℝ |
41 | | ressxr 9962 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
42 | 40, 41 | sstri 3577 |
. . . . . . . . . . . 12
⊢
ℕ0 ⊆ ℝ* |
43 | | mdegaddle.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
44 | 11, 30 | tdeglem1 23622 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ 𝑉 → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
46 | 45 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℕ0) |
47 | 42, 46 | sseldi 3566 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*) |
48 | 35, 39, 47 | 3jca 1235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐷‘𝐹) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*)) |
49 | 48 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐷‘𝐹) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*)) |
50 | | xrmax1 11880 |
. . . . . . . . . . . 12
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ (𝐷‘𝐺) ∈ ℝ*) → (𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
51 | 34, 37, 50 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
52 | 51 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
53 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) |
54 | 52, 53 | jca 553 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) |
55 | | xrlelttr 11863 |
. . . . . . . . 9
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈ ℝ*) → (((𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) → (𝐷‘𝐹) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) |
56 | 49, 54, 55 | sylc 63 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐷‘𝐹) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) |
57 | 28, 1, 2, 29, 11, 30, 31, 32, 56 | mdeglt 23629 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐹‘𝑐) = (0g‘𝑅)) |
58 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → 𝐺 ∈ 𝐵) |
59 | 37 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝐷‘𝐺) ∈
ℝ*) |
60 | 59, 39, 47 | 3jca 1235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐷‘𝐺) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*)) |
61 | 60 | adantrr 749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐷‘𝐺) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*)) |
62 | | xrmax2 11881 |
. . . . . . . . . . . 12
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ (𝐷‘𝐺) ∈ ℝ*) → (𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
63 | 34, 37, 62 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
64 | 63 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
65 | 64, 53 | jca 553 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) |
66 | | xrlelttr 11863 |
. . . . . . . . 9
⊢ (((𝐷‘𝐺) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈ ℝ*) → (((𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) → (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) |
67 | 61, 65, 66 | sylc 63 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) |
68 | 28, 1, 2, 29, 11, 30, 58, 32, 67 | mdeglt 23629 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐺‘𝑐) = (0g‘𝑅)) |
69 | 57, 68 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅))) |
70 | | mdegaddle.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
71 | | ringgrp 18375 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
72 | 70, 71 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Grp) |
73 | 10, 29 | ring0cl 18392 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
74 | 70, 73 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) |
75 | 10, 3, 29 | grplid 17275 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧
(0g‘𝑅)
∈ (Base‘𝑅))
→ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
76 | 72, 74, 75 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
77 | 76 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
78 | 69, 77 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐)) = (0g‘𝑅)) |
79 | 27, 78 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅)) |
80 | 79 | expr 641 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅))) |
81 | 80 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅))) |
82 | 1 | mplring 19273 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring) |
83 | 43, 70, 82 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ Ring) |
84 | 2, 4 | ringacl 18401 |
. . . 4
⊢ ((𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 + 𝐺) ∈ 𝐵) |
85 | 83, 5, 6, 84 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵) |
86 | 28, 1, 2, 29, 11, 30 | mdegleb 23628 |
. . 3
⊢ (((𝐹 + 𝐺) ∈ 𝐵 ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ*) →
((𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ↔ ∀𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅)))) |
87 | 85, 38, 86 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ↔ ∀𝑐 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} (if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅)))) |
88 | 81, 87 | mpbird 246 |
1
⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |