Step | Hyp | Ref
| Expression |
1 | | mdegaddle.y |
. . . . . . . . . 10
⊢ 𝑌 = (𝐼 mPoly 𝑅) |
2 | | mdegaddle.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑌) |
3 | | eqid 2821 |
. . . . . . . . . 10
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | mdegaddle.p |
. . . . . . . . . 10
⊢ + =
(+g‘𝑌) |
5 | | mdegaddle.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
6 | | mdegaddle.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
7 | 1, 2, 3, 4, 5, 6 | mpladd 20216 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 + 𝐺) = (𝐹 ∘f
(+g‘𝑅)𝐺)) |
8 | 7 | fveq1d 6667 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 + 𝐺)‘𝑐) = ((𝐹 ∘f
(+g‘𝑅)𝐺)‘𝑐)) |
9 | 8 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹 + 𝐺)‘𝑐) = ((𝐹 ∘f
(+g‘𝑅)𝐺)‘𝑐)) |
10 | | eqid 2821 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
11 | | eqid 2821 |
. . . . . . . . . . 11
⊢ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} = {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin} |
12 | 1, 10, 2, 11, 5 | mplelf 20207 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
13 | 12 | ffnd 6510 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
14 | 13 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐹 Fn {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
15 | 1, 10, 2, 11, 6 | mplelf 20207 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶(Base‘𝑅)) |
16 | 15 | ffnd 6510 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 Fn {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
17 | 16 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝐺 Fn {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
18 | | ovex 7183 |
. . . . . . . . . 10
⊢
(ℕ0 ↑m 𝐼) ∈ V |
19 | 18 | rabex 5228 |
. . . . . . . . 9
⊢ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∈
V |
20 | 19 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∈
V) |
21 | | simpr 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
22 | | fnfvof 7417 |
. . . . . . . 8
⊢ (((𝐹 Fn {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ 𝐺 Fn {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) ∧ ({𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∈ V ∧
𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin})) →
((𝐹 ∘f
(+g‘𝑅)𝐺)‘𝑐) = ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐))) |
23 | 14, 17, 20, 21, 22 | syl22anc 836 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹 ∘f
(+g‘𝑅)𝐺)‘𝑐) = ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐))) |
24 | 9, 23 | eqtrd 2856 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐹 + 𝐺)‘𝑐) = ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐))) |
25 | 24 | adantrr 715 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐹 + 𝐺)‘𝑐) = ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐))) |
26 | | mdegaddle.d |
. . . . . . . 8
⊢ 𝐷 = (𝐼 mDeg 𝑅) |
27 | | eqid 2821 |
. . . . . . . 8
⊢
(0g‘𝑅) = (0g‘𝑅) |
28 | | eqid 2821 |
. . . . . . . 8
⊢ (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) = (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)) |
29 | 5 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → 𝐹 ∈ 𝐵) |
30 | | simprl 769 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}) |
31 | 26, 1, 2 | mdegxrcl 24655 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ 𝐵 → (𝐷‘𝐹) ∈
ℝ*) |
32 | 5, 31 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘𝐹) ∈
ℝ*) |
33 | 32 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝐷‘𝐹) ∈
ℝ*) |
34 | 26, 1, 2 | mdegxrcl 24655 |
. . . . . . . . . . . . . 14
⊢ (𝐺 ∈ 𝐵 → (𝐷‘𝐺) ∈
ℝ*) |
35 | 6, 34 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷‘𝐺) ∈
ℝ*) |
36 | 35, 32 | ifcld 4512 |
. . . . . . . . . . . 12
⊢ (𝜑 → if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈
ℝ*) |
37 | 36 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) →
if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈
ℝ*) |
38 | | nn0ssre 11895 |
. . . . . . . . . . . . 13
⊢
ℕ0 ⊆ ℝ |
39 | | ressxr 10679 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
40 | 38, 39 | sstri 3976 |
. . . . . . . . . . . 12
⊢
ℕ0 ⊆ ℝ* |
41 | | mdegaddle.i |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
42 | 11, 28 | tdeglem1 24646 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ 𝑉 → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏)):{𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈
Fin}⟶ℕ0) |
44 | 43 | ffvelrnda 6846 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℕ0) |
45 | 40, 44 | sseldi 3965 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*) |
46 | 33, 37, 45 | 3jca 1124 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐷‘𝐹) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*)) |
47 | 46 | adantrr 715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐷‘𝐹) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*)) |
48 | | xrmax1 12562 |
. . . . . . . . . . . 12
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ (𝐷‘𝐺) ∈ ℝ*) → (𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
49 | 32, 35, 48 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
50 | 49 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
51 | | simprr 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) |
52 | 50, 51 | jca 514 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) |
53 | | xrlelttr 12543 |
. . . . . . . . 9
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈ ℝ*) → (((𝐷‘𝐹) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) → (𝐷‘𝐹) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) |
54 | 47, 52, 53 | sylc 65 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐷‘𝐹) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) |
55 | 26, 1, 2, 27, 11, 28, 29, 30, 54 | mdeglt 24653 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐹‘𝑐) = (0g‘𝑅)) |
56 | 6 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → 𝐺 ∈ 𝐵) |
57 | 35 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → (𝐷‘𝐺) ∈
ℝ*) |
58 | 57, 37, 45 | 3jca 1124 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) → ((𝐷‘𝐺) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*)) |
59 | 58 | adantrr 715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐷‘𝐺) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈
ℝ*)) |
60 | | xrmax2 12563 |
. . . . . . . . . . . 12
⊢ (((𝐷‘𝐹) ∈ ℝ* ∧ (𝐷‘𝐺) ∈ ℝ*) → (𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
61 | 32, 35, 60 | syl2anc 586 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
62 | 61 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |
63 | 62, 51 | jca 514 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) |
64 | | xrlelttr 12543 |
. . . . . . . . 9
⊢ (((𝐷‘𝐺) ∈ ℝ* ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ* ∧ ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) ∈ ℝ*) → (((𝐷‘𝐺) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) → (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) |
65 | 59, 63, 64 | sylc 65 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐷‘𝐺) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐)) |
66 | 26, 1, 2, 27, 11, 28, 56, 30, 65 | mdeglt 24653 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → (𝐺‘𝑐) = (0g‘𝑅)) |
67 | 55, 66 | oveq12d 7168 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐)) = ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅))) |
68 | | mdegaddle.r |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
69 | | ringgrp 19296 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
70 | 68, 69 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Grp) |
71 | 10, 27 | ring0cl 19313 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
72 | 68, 71 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) |
73 | 10, 3, 27 | grplid 18127 |
. . . . . . . 8
⊢ ((𝑅 ∈ Grp ∧
(0g‘𝑅)
∈ (Base‘𝑅))
→ ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
74 | 70, 72, 73 | syl2anc 586 |
. . . . . . 7
⊢ (𝜑 →
((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
75 | 74 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((0g‘𝑅)(+g‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
76 | 67, 75 | eqtrd 2856 |
. . . . 5
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐹‘𝑐)(+g‘𝑅)(𝐺‘𝑐)) = (0g‘𝑅)) |
77 | 25, 76 | eqtrd 2856 |
. . . 4
⊢ ((𝜑 ∧ (𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐))) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅)) |
78 | 77 | expr 459 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin}) →
(if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅))) |
79 | 78 | ralrimiva 3182 |
. 2
⊢ (𝜑 → ∀𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅))) |
80 | 1 | mplring 20226 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring) |
81 | 41, 68, 80 | syl2anc 586 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ Ring) |
82 | 2, 4 | ringacl 19322 |
. . . 4
⊢ ((𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵) → (𝐹 + 𝐺) ∈ 𝐵) |
83 | 81, 5, 6, 82 | syl3anc 1367 |
. . 3
⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵) |
84 | 26, 1, 2, 27, 11, 28 | mdegleb 24652 |
. . 3
⊢ (((𝐹 + 𝐺) ∈ 𝐵 ∧ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ∈ ℝ*) →
((𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ↔ ∀𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅)))) |
85 | 83, 36, 84 | syl2anc 586 |
. 2
⊢ (𝜑 → ((𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) ↔ ∀𝑐 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} (if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹)) < ((𝑏 ∈ {𝑎 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑎 “ ℕ) ∈ Fin} ↦
(ℂfld Σg 𝑏))‘𝑐) → ((𝐹 + 𝐺)‘𝑐) = (0g‘𝑅)))) |
86 | 79, 85 | mpbird 259 |
1
⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) ≤ if((𝐷‘𝐹) ≤ (𝐷‘𝐺), (𝐷‘𝐺), (𝐷‘𝐹))) |