Step | Hyp | Ref
| Expression |
1 | | jensen.7 |
. . . . . 6
⊢ (𝜑 → 0 <
(ℂfld Σg 𝑇)) |
2 | | jensen.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇:𝐴⟶(0[,)+∞)) |
3 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝑇:𝐴⟶(0[,)+∞) → 𝑇 Fn 𝐴) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 Fn 𝐴) |
5 | | fnresdm 6000 |
. . . . . . . 8
⊢ (𝑇 Fn 𝐴 → (𝑇 ↾ 𝐴) = 𝑇) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑇 ↾ 𝐴) = 𝑇) |
7 | 6 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑇 ↾ 𝐴)) = (ℂfld
Σg 𝑇)) |
8 | 1, 7 | breqtrrd 4681 |
. . . . 5
⊢ (𝜑 → 0 <
(ℂfld Σg (𝑇 ↾ 𝐴))) |
9 | | ssid 3624 |
. . . . 5
⊢ 𝐴 ⊆ 𝐴 |
10 | 8, 9 | jctil 560 |
. . . 4
⊢ (𝜑 → (𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝐴)))) |
11 | | jensen.4 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ Fin) |
12 | | sseq1 3626 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → (𝑎 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
13 | | reseq2 5391 |
. . . . . . . . . . . . 13
⊢ (𝑎 = ∅ → (𝑇 ↾ 𝑎) = (𝑇 ↾ ∅)) |
14 | | res0 5400 |
. . . . . . . . . . . . 13
⊢ (𝑇 ↾ ∅) =
∅ |
15 | 13, 14 | syl6eq 2672 |
. . . . . . . . . . . 12
⊢ (𝑎 = ∅ → (𝑇 ↾ 𝑎) = ∅) |
16 | 15 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑎 = ∅ →
(ℂfld Σg (𝑇 ↾ 𝑎)) = (ℂfld
Σg ∅)) |
17 | | cnfld0 19770 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) |
18 | 17 | gsum0 17278 |
. . . . . . . . . . 11
⊢
(ℂfld Σg ∅) =
0 |
19 | 16, 18 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑎 = ∅ →
(ℂfld Σg (𝑇 ↾ 𝑎)) = 0) |
20 | 19 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → (0 <
(ℂfld Σg (𝑇 ↾ 𝑎)) ↔ 0 < 0)) |
21 | 12, 20 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑎 = ∅ → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) ↔ (∅ ⊆ 𝐴 ∧ 0 < 0))) |
22 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (𝑎 = ∅ → ((𝑇 ∘𝑓
· 𝑋) ↾ 𝑎) = ((𝑇 ∘𝑓 · 𝑋) ↾
∅)) |
23 | 22 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = ∅ →
(ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) = (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾
∅))) |
24 | 23, 19 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑎 = ∅ →
((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ ∅)) /
0)) |
25 | | reseq2 5391 |
. . . . . . . . . . . . 13
⊢ (𝑎 = ∅ → ((𝑇 ∘𝑓
· (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) |
26 | 25 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑎 = ∅ →
(ℂfld Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅))) |
27 | 26, 19 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑎 = ∅ →
((ℂfld Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)) |
28 | 27 | breq2d 4665 |
. . . . . . . . . 10
⊢ (𝑎 = ∅ → ((𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0))) |
29 | 28 | rabbidv 3189 |
. . . . . . . . 9
⊢ (𝑎 = ∅ → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}) |
30 | 24, 29 | eleq12d 2695 |
. . . . . . . 8
⊢ (𝑎 = ∅ →
(((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ ∅)) / 0) ∈
{𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) /
0)})) |
31 | 21, 30 | imbi12d 334 |
. . . . . . 7
⊢ (𝑎 = ∅ → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))}) ↔ ((∅ ⊆ 𝐴 ∧ 0 < 0) →
((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ ∅)) / 0) ∈
{𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) /
0)}))) |
32 | 31 | imbi2d 330 |
. . . . . 6
⊢ (𝑎 = ∅ → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) →
((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ ∅)) / 0) ∈
{𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) /
0)})))) |
33 | | sseq1 3626 |
. . . . . . . . 9
⊢ (𝑎 = 𝑘 → (𝑎 ⊆ 𝐴 ↔ 𝑘 ⊆ 𝐴)) |
34 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑘 → (𝑇 ↾ 𝑎) = (𝑇 ↾ 𝑘)) |
35 | 34 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑘 → (ℂfld
Σg (𝑇 ↾ 𝑎)) = (ℂfld
Σg (𝑇 ↾ 𝑘))) |
36 | 35 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑎 = 𝑘 → (0 < (ℂfld
Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘)))) |
37 | 33, 36 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑎 = 𝑘 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) ↔ (𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))))) |
38 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑘 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎) = ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) |
39 | 38 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑘 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) = (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘))) |
40 | 39, 35 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑎 = 𝑘 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))) |
41 | | reseq2 5391 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑘 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) |
42 | 41 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑘 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘))) |
43 | 42, 35 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑘 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))) |
44 | 43 | breq2d 4665 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑘 → ((𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))))) |
45 | 44 | rabbidv 3189 |
. . . . . . . . 9
⊢ (𝑎 = 𝑘 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) |
46 | 40, 45 | eleq12d 2695 |
. . . . . . . 8
⊢ (𝑎 = 𝑘 → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) |
47 | 37, 46 | imbi12d 334 |
. . . . . . 7
⊢ (𝑎 = 𝑘 → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))}) ↔ ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}))) |
48 | 47 | imbi2d 330 |
. . . . . 6
⊢ (𝑎 = 𝑘 → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})))) |
49 | | sseq1 3626 |
. . . . . . . . 9
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (𝑎 ⊆ 𝐴 ↔ (𝑘 ∪ {𝑐}) ⊆ 𝐴)) |
50 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (𝑇 ↾ 𝑎) = (𝑇 ↾ (𝑘 ∪ {𝑐}))) |
51 | 50 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld
Σg (𝑇 ↾ 𝑎)) = (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) |
52 | 51 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (0 < (ℂfld
Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) |
53 | 49, 52 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) ↔ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))) |
54 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎) = ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) |
55 | 54 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) = (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})))) |
56 | 55, 51 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) |
57 | | reseq2 5391 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) |
58 | 57 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})))) |
59 | 58, 51 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) |
60 | 59 | breq2d 4665 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))) |
61 | 60 | rabbidv 3189 |
. . . . . . . . 9
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}) |
62 | 56, 61 | eleq12d 2695 |
. . . . . . . 8
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})) |
63 | 53, 62 | imbi12d 334 |
. . . . . . 7
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))}) ↔ (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))) |
64 | 63 | imbi2d 330 |
. . . . . 6
⊢ (𝑎 = (𝑘 ∪ {𝑐}) → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))) |
65 | | sseq1 3626 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (𝑎 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
66 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (𝑇 ↾ 𝑎) = (𝑇 ↾ 𝐴)) |
67 | 66 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (ℂfld
Σg (𝑇 ↾ 𝑎)) = (ℂfld
Σg (𝑇 ↾ 𝐴))) |
68 | 67 | breq2d 4665 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (0 < (ℂfld
Σg (𝑇 ↾ 𝑎)) ↔ 0 < (ℂfld
Σg (𝑇 ↾ 𝐴)))) |
69 | 65, 68 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) ↔ (𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝐴))))) |
70 | | reseq2 5391 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎) = ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) |
71 | 70 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) = (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴))) |
72 | 71, 67 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))) |
73 | | reseq2 5391 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎) = ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) |
74 | 73 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) = (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴))) |
75 | 74, 67 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) = ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))) |
76 | 75 | breq2d 4665 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → ((𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ↔ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))))) |
77 | 76 | rabbidv 3189 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))}) |
78 | 72, 77 | eleq12d 2695 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))} ↔ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))})) |
79 | 69, 78 | imbi12d 334 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))}) ↔ ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝐴))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))}))) |
80 | 79 | imbi2d 330 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ((𝜑 → ((𝑎 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑎))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑎)) / (ℂfld
Σg (𝑇 ↾ 𝑎)))})) ↔ (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝐴))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))})))) |
81 | | 0re 10040 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
82 | 81 | ltnri 10146 |
. . . . . . . . 9
⊢ ¬ 0
< 0 |
83 | 82 | pm2.21i 116 |
. . . . . . . 8
⊢ (0 < 0
→ ((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ ∅)) / 0) ∈
{𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}) |
84 | 83 | adantl 482 |
. . . . . . 7
⊢ ((∅
⊆ 𝐴 ∧ 0 < 0)
→ ((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ ∅)) / 0) ∈
{𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) / 0)}) |
85 | 84 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) →
((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ ∅)) / 0) ∈
{𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ ∅)) /
0)})) |
86 | | impexp 462 |
. . . . . . . . . . . 12
⊢ (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) ↔ (𝑘 ⊆ 𝐴 → (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}))) |
87 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴) |
88 | 87 | unssad 3790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ⊆ 𝐴) |
89 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) |
90 | | jensen.1 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐷 ⊆ ℝ) |
91 | 90 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → 𝐷 ⊆ ℝ) |
92 | | jensen.2 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐹:𝐷⟶ℝ) |
93 | 92 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → 𝐹:𝐷⟶ℝ) |
94 | | simplll 798 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → 𝜑) |
95 | | jensen.3 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) |
96 | 94, 95 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) ∧ (𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷) |
97 | 94, 11 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → 𝐴 ∈ Fin) |
98 | 94, 2 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → 𝑇:𝐴⟶(0[,)+∞)) |
99 | | jensen.6 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋:𝐴⟶𝐷) |
100 | 94, 99 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → 𝑋:𝐴⟶𝐷) |
101 | 1 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → 0 < (ℂfld
Σg 𝑇)) |
102 | | jensen.8 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
103 | 94, 102 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) ∧ (𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹‘𝑥)) + ((1 − 𝑡) · (𝐹‘𝑦)))) |
104 | | simpllr 799 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → ¬ 𝑐 ∈ 𝑘) |
105 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → (𝑘 ∪ {𝑐}) ⊆ 𝐴) |
106 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(ℂfld Σg (𝑇 ↾ 𝑘)) = (ℂfld
Σg (𝑇 ↾ 𝑘)) |
107 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) |
108 | | cnring 19768 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
ℂfld ∈ Ring |
109 | | ringcmn 18581 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
110 | 108, 109 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ℂfld ∈
CMnd) |
111 | 11 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝐴 ∈ Fin) |
112 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ∈ Fin) |
113 | 111, 88, 112 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ∈ Fin) |
114 | | rege0subm 19802 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(0[,)+∞) ∈
(SubMnd‘ℂfld) |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0[,)+∞) ∈
(SubMnd‘ℂfld)) |
116 | 2 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑇:𝐴⟶(0[,)+∞)) |
117 | 116, 88 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇 ↾ 𝑘):𝑘⟶(0[,)+∞)) |
118 | | c0ex 10034 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
V |
119 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ∈ V) |
120 | 117, 113,
119 | fdmfifsupp 8285 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇 ↾ 𝑘) finSupp 0) |
121 | 17, 110, 113, 115, 117, 120 | gsumsubmcl 18319 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld
Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞)) |
122 | | elrege0 12278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) ↔
((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ ∧ 0 ≤
(ℂfld Σg (𝑇 ↾ 𝑘)))) |
123 | 122 | simplbi 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) →
(ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ) |
124 | 121, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld
Σg (𝑇 ↾ 𝑘)) ∈ ℝ) |
125 | 124 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → (ℂfld
Σg (𝑇 ↾ 𝑘)) ∈ ℝ) |
126 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) |
127 | 125, 126 | elrpd 11869 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → (ℂfld
Σg (𝑇 ↾ 𝑘)) ∈
ℝ+) |
128 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) |
129 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹‘𝑤) = (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))))) |
130 | 129 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ↔ (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))))) |
131 | 130 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))} ↔ (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))))) |
132 | 128, 131 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))))) |
133 | 132 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ 𝐷) |
134 | 132 | simprd 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))) |
135 | 91, 93, 96, 97, 98, 100, 101, 103, 104, 105, 106, 107, 127, 133, 134 | jensenlem2 24714 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))) |
136 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (𝐹‘𝑤) = (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))) |
137 | 136 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ↔ (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))) |
138 | 137 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
⊢
(((ℂfld Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))} ↔ (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))) |
139 | 135, 138 | sylibr 224 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∧ ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}) |
140 | 139 | expr 643 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))} → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})) |
141 | 89, 140 | embantd 59 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})) |
142 | | cnfldbas 19750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℂ =
(Base‘ℂfld) |
143 | | ringmnd 18556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
144 | 108, 143 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ℂfld ∈
Mnd) |
145 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ∈ Fin ∧ (𝑘 ∪ {𝑐}) ⊆ 𝐴) → (𝑘 ∪ {𝑐}) ∈ Fin) |
146 | 111, 87, 145 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ∈ Fin) |
147 | 146 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑘 ∪ {𝑐}) ∈ Fin) |
148 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑐} ⊆ (𝑘 ∪ {𝑐}) |
149 | | vsnid 4209 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑐 ∈ {𝑐} |
150 | 148, 149 | sselii 3600 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑐 ∈ (𝑘 ∪ {𝑐}) |
151 | 150 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑐 ∈ (𝑘 ∪ {𝑐})) |
152 | | remulcl 10021 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ) |
153 | 152 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ) |
154 | | rge0ssre 12280 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(0[,)+∞) ⊆ ℝ |
155 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℝ) → 𝑇:𝐴⟶ℝ) |
156 | 2, 154, 155 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑇:𝐴⟶ℝ) |
157 | 99, 90 | fssd 6057 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑋:𝐴⟶ℝ) |
158 | | inidm 3822 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
159 | 153, 156,
157, 11, 11, 158 | off 6912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑇 ∘𝑓 · 𝑋):𝐴⟶ℝ) |
160 | | ax-resscn 9993 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ℝ
⊆ ℂ |
161 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑇 ∘𝑓
· 𝑋):𝐴⟶ℝ ∧ ℝ
⊆ ℂ) → (𝑇
∘𝑓 · 𝑋):𝐴⟶ℂ) |
162 | 159, 160,
161 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑇 ∘𝑓 · 𝑋):𝐴⟶ℂ) |
163 | 162 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑇 ∘𝑓 · 𝑋):𝐴⟶ℂ) |
164 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴) |
165 | 163, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ) |
166 | 2 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑇:𝐴⟶(0[,)+∞)) |
167 | 111 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝐴 ∈ Fin) |
168 | | fex 6490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ Fin) → 𝑇 ∈ V) |
169 | 166, 167,
168 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑇 ∈ V) |
170 | 99 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑋:𝐴⟶𝐷) |
171 | | fex 6490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑋:𝐴⟶𝐷 ∧ 𝐴 ∈ Fin) → 𝑋 ∈ V) |
172 | 170, 167,
171 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑋 ∈ V) |
173 | | offres 7163 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑇 ∈ V ∧ 𝑋 ∈ V) → ((𝑇 ∘𝑓
· 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 ·
(𝑋 ↾ (𝑘 ∪ {𝑐})))) |
174 | 169, 172,
173 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 ·
(𝑋 ↾ (𝑘 ∪ {𝑐})))) |
175 | 174 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 ·
(𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0)) |
176 | 154, 160 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(0[,)+∞) ⊆ ℂ |
177 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞)
⊆ ℂ) → 𝑇:𝐴⟶ℂ) |
178 | 166, 176,
177 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑇:𝐴⟶ℂ) |
179 | 178, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑇 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ) |
180 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ (𝑘 ∪ {𝑐})) |
181 | 180 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → 𝑥 ∈ (𝑘 ∪ {𝑐})) |
182 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ (𝑘 ∪ {𝑐}) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇‘𝑥)) |
183 | 181, 182 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇‘𝑥)) |
184 | | difun2 4048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) = (𝑘 ∖ {𝑐}) |
185 | | difss 3737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∖ {𝑐}) ⊆ 𝑘 |
186 | 184, 185 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) ⊆ 𝑘 |
187 | 186 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ 𝑘) |
188 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) |
189 | 88 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑘 ⊆ 𝐴) |
190 | 166, 189 | feqresmpt 6250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑇 ↾ 𝑘) = (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥))) |
191 | 190 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (ℂfld
Σg (𝑇 ↾ 𝑘)) = (ℂfld
Σg (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥)))) |
192 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑘 ∈ Fin) |
193 | 189 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴) |
194 | 166 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝐴) → (𝑇‘𝑥) ∈ (0[,)+∞)) |
195 | 193, 194 | syldan 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ (0[,)+∞)) |
196 | 176, 195 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ ℂ) |
197 | 192, 196 | gsumfsum 19813 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (ℂfld
Σg (𝑥 ∈ 𝑘 ↦ (𝑇‘𝑥))) = Σ𝑥 ∈ 𝑘 (𝑇‘𝑥)) |
198 | 188, 191,
197 | 3eqtrrd 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → Σ𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0) |
199 | | elrege0 12278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑇‘𝑥) ∈ (0[,)+∞) ↔ ((𝑇‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑥))) |
200 | 195, 199 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → ((𝑇‘𝑥) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑥))) |
201 | 200 | simpld 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) ∈ ℝ) |
202 | 200 | simprd 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → 0 ≤ (𝑇‘𝑥)) |
203 | 192, 201,
202 | fsum00 14530 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (Σ𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0 ↔ ∀𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0)) |
204 | 198, 203 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ∀𝑥 ∈ 𝑘 (𝑇‘𝑥) = 0) |
205 | 204 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ 𝑘) → (𝑇‘𝑥) = 0) |
206 | 187, 205 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → (𝑇‘𝑥) = 0) |
207 | 183, 206 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = 0) |
208 | 179, 207 | suppss 7325 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐}) |
209 | | mul02 10214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℂ → (0
· 𝑥) =
0) |
210 | 209 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ ¬
𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0) |
211 | 90 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝐷 ⊆ ℝ) |
212 | 211, 160 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝐷 ⊆ ℂ) |
213 | 170, 212 | fssd 6057 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑋:𝐴⟶ℂ) |
214 | 213, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑋 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ) |
215 | 118 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 0 ∈ V) |
216 | 208, 210,
179, 214, 147, 215 | suppssof1 7328 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 ·
(𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐}) |
217 | 175, 216 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐}) |
218 | 142, 17, 144, 147, 151, 165, 217 | gsumpt 18361 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐)) |
219 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 ∈ (𝑘 ∪ {𝑐}) → (((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘𝑓 · 𝑋)‘𝑐)) |
220 | 151, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘𝑓 · 𝑋)‘𝑐)) |
221 | 166, 3 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑇 Fn 𝐴) |
222 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑋:𝐴⟶𝐷 → 𝑋 Fn 𝐴) |
223 | 170, 222 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑋 Fn 𝐴) |
224 | 164, 151 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝑐 ∈ 𝐴) |
225 | | fnfvof 6911 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑇 Fn 𝐴 ∧ 𝑋 Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴)) → ((𝑇 ∘𝑓 · 𝑋)‘𝑐) = ((𝑇‘𝑐) · (𝑋‘𝑐))) |
226 | 221, 223,
167, 224, 225 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘𝑓 · 𝑋)‘𝑐) = ((𝑇‘𝑐) · (𝑋‘𝑐))) |
227 | 218, 220,
226 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇‘𝑐) · (𝑋‘𝑐))) |
228 | 142, 17, 144, 147, 151, 179, 208 | gsumpt 18361 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐)) |
229 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 ∈ (𝑘 ∪ {𝑐}) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇‘𝑐)) |
230 | 151, 229 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇‘𝑐)) |
231 | 228, 230 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (𝑇‘𝑐)) |
232 | 227, 231 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇‘𝑐) · (𝑋‘𝑐)) / (𝑇‘𝑐))) |
233 | 213, 224 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑋‘𝑐) ∈ ℂ) |
234 | 178, 224 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑇‘𝑐) ∈ ℂ) |
235 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) |
236 | 235, 231 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 0 < (𝑇‘𝑐)) |
237 | 236 | gt0ne0d 10592 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑇‘𝑐) ≠ 0) |
238 | 233, 234,
237 | divcan3d 10806 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇‘𝑐) · (𝑋‘𝑐)) / (𝑇‘𝑐)) = (𝑋‘𝑐)) |
239 | 232, 238 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝑋‘𝑐)) |
240 | 170, 224 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑋‘𝑐) ∈ 𝐷) |
241 | 239, 240 | eqeltrd 2701 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷) |
242 | 92 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → 𝐹:𝐷⟶ℝ) |
243 | 242, 240 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ∈ ℝ) |
244 | 243 | leidd 10594 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ≤ (𝐹‘(𝑋‘𝑐))) |
245 | 239 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) = (𝐹‘(𝑋‘𝑐))) |
246 | | fco 6058 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
247 | 92, 99, 246 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
248 | 153, 156,
247, 11, 11, 158 | off 6912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℝ) |
249 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑇 ∘𝑓
· (𝐹 ∘ 𝑋)):𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → (𝑇
∘𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℂ) |
250 | 248, 160,
249 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℂ) |
251 | 250 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)):𝐴⟶ℂ) |
252 | 251, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ) |
253 | 247 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋):𝐴⟶ℝ) |
254 | | fex 6490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹 ∘ 𝑋):𝐴⟶ℝ ∧ 𝐴 ∈ Fin) → (𝐹 ∘ 𝑋) ∈ V) |
255 | 253, 167,
254 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋) ∈ V) |
256 | | offres 7163 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑇 ∈ V ∧ (𝐹 ∘ 𝑋) ∈ V) → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 ·
((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐})))) |
257 | 169, 255,
256 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 ·
((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐})))) |
258 | 257 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 ·
((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0)) |
259 | | fss 6056 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐹 ∘ 𝑋):𝐴⟶ℝ ∧ ℝ ⊆
ℂ) → (𝐹 ∘
𝑋):𝐴⟶ℂ) |
260 | 253, 160,
259 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋):𝐴⟶ℂ) |
261 | 260, 164 | fssresd 6071 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ) |
262 | 208, 210,
179, 261, 147, 215 | suppssof1 7328 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 ·
((𝐹 ∘ 𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐}) |
263 | 258, 262 | eqsstrd 3639 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐}) |
264 | 142, 17, 144, 147, 151, 252, 263 | gsumpt 18361 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐)) |
265 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 ∈ (𝑘 ∪ {𝑐}) → (((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))‘𝑐)) |
266 | 151, 265 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))‘𝑐)) |
267 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹:𝐷⟶ℝ → 𝐹 Fn 𝐷) |
268 | 92, 267 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐹 Fn 𝐷) |
269 | | fnfco 6069 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐹 Fn 𝐷 ∧ 𝑋:𝐴⟶𝐷) → (𝐹 ∘ 𝑋) Fn 𝐴) |
270 | 268, 99, 269 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐹 ∘ 𝑋) Fn 𝐴) |
271 | 270 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹 ∘ 𝑋) Fn 𝐴) |
272 | | fnfvof 6911 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑇 Fn 𝐴 ∧ (𝐹 ∘ 𝑋) Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐 ∈ 𝐴)) → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐))) |
273 | 221, 271,
167, 224, 272 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐))) |
274 | | fvco3 6275 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋:𝐴⟶𝐷 ∧ 𝑐 ∈ 𝐴) → ((𝐹 ∘ 𝑋)‘𝑐) = (𝐹‘(𝑋‘𝑐))) |
275 | 170, 224,
274 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝐹 ∘ 𝑋)‘𝑐) = (𝐹‘(𝑋‘𝑐))) |
276 | 275 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇‘𝑐) · ((𝐹 ∘ 𝑋)‘𝑐)) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐)))) |
277 | 273, 276 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))‘𝑐) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐)))) |
278 | 264, 266,
277 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐)))) |
279 | 278, 231 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))) / (𝑇‘𝑐))) |
280 | 243 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹‘(𝑋‘𝑐)) ∈ ℂ) |
281 | 280, 234,
237 | divcan3d 10806 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (((𝑇‘𝑐) · (𝐹‘(𝑋‘𝑐))) / (𝑇‘𝑐)) = (𝐹‘(𝑋‘𝑐))) |
282 | 279, 281 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝐹‘(𝑋‘𝑐))) |
283 | 244, 245,
282 | 3brtr4d 4685 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → (𝐹‘((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) |
284 | 241, 283,
138 | sylanbrc 698 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}) |
285 | 284 | a1d 25 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})) |
286 | 122 | simprbi 480 |
. . . . . . . . . . . . . . . 16
⊢
((ℂfld Σg (𝑇 ↾ 𝑘)) ∈ (0[,)+∞) → 0 ≤
(ℂfld Σg (𝑇 ↾ 𝑘))) |
287 | 121, 286 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ≤ (ℂfld
Σg (𝑇 ↾ 𝑘))) |
288 | | leloe 10124 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ (ℂfld Σg (𝑇 ↾ 𝑘)) ∈ ℝ) → (0 ≤
(ℂfld Σg (𝑇 ↾ 𝑘)) ↔ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))))) |
289 | 81, 124, 288 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 ≤ (ℂfld
Σg (𝑇 ↾ 𝑘)) ↔ (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘))))) |
290 | 287, 289 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) ∨ 0 = (ℂfld
Σg (𝑇 ↾ 𝑘)))) |
291 | 141, 285,
290 | mpjaodan 827 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ((0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})) |
292 | 88, 291 | embantd 59 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ((𝑘 ⊆ 𝐴 → (0 < (ℂfld
Σg (𝑇 ↾ 𝑘)) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})) |
293 | 86, 292 | syl5bi 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})) |
294 | 293 | ex 450 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))) |
295 | 294 | com23 86 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑐 ∈ 𝑘) → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))) |
296 | 295 | expcom 451 |
. . . . . . . 8
⊢ (¬
𝑐 ∈ 𝑘 → (𝜑 → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))) |
297 | 296 | adantl 482 |
. . . . . . 7
⊢ ((𝑘 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑘) → (𝜑 → (((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))) |
298 | 297 | a2d 29 |
. . . . . 6
⊢ ((𝑘 ∈ Fin ∧ ¬ 𝑐 ∈ 𝑘) → ((𝜑 → ((𝑘 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝑘))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝑘)) / (ℂfld
Σg (𝑇 ↾ 𝑘)))})) → (𝜑 → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld
Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))) |
299 | 32, 48, 64, 80, 85, 298 | findcard2s 8201 |
. . . . 5
⊢ (𝐴 ∈ Fin → (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝐴))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))}))) |
300 | 11, 299 | mpcom 38 |
. . . 4
⊢ (𝜑 → ((𝐴 ⊆ 𝐴 ∧ 0 < (ℂfld
Σg (𝑇 ↾ 𝐴))) → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))})) |
301 | 10, 300 | mpd 15 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))}) |
302 | | ffn 6045 |
. . . . . . 7
⊢ ((𝑇 ∘𝑓
· 𝑋):𝐴⟶ℝ → (𝑇 ∘𝑓
· 𝑋) Fn 𝐴) |
303 | 159, 302 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑇 ∘𝑓 · 𝑋) Fn 𝐴) |
304 | | fnresdm 6000 |
. . . . . 6
⊢ ((𝑇 ∘𝑓
· 𝑋) Fn 𝐴 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴) = (𝑇 ∘𝑓 · 𝑋)) |
305 | 303, 304 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴) = (𝑇 ∘𝑓 · 𝑋)) |
306 | 305 | oveq2d 6666 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) = (ℂfld
Σg (𝑇 ∘𝑓 · 𝑋))) |
307 | 306, 7 | oveq12d 6668 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) = ((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇))) |
308 | 4, 270, 11, 11, 158 | offn 6908 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) Fn 𝐴) |
309 | | fnresdm 6000 |
. . . . . . . 8
⊢ ((𝑇 ∘𝑓
· (𝐹 ∘ 𝑋)) Fn 𝐴 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴) = (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) |
310 | 308, 309 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴) = (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) |
311 | 310 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) = (ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)))) |
312 | 311, 7 | oveq12d 6668 |
. . . . 5
⊢ (𝜑 → ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) = ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇))) |
313 | 312 | breq2d 4665 |
. . . 4
⊢ (𝜑 → ((𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴))) ↔ (𝐹‘𝑤) ≤ ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇)))) |
314 | 313 | rabbidv 3189 |
. . 3
⊢ (𝜑 → {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg ((𝑇 ∘𝑓 · (𝐹 ∘ 𝑋)) ↾ 𝐴)) / (ℂfld
Σg (𝑇 ↾ 𝐴)))} = {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇))}) |
315 | 301, 307,
314 | 3eltr3d 2715 |
. 2
⊢ (𝜑 → ((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇)) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇))}) |
316 | | fveq2 6191 |
. . . 4
⊢ (𝑤 = ((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇)) → (𝐹‘𝑤) = (𝐹‘((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇)))) |
317 | 316 | breq1d 4663 |
. . 3
⊢ (𝑤 = ((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇)) → ((𝐹‘𝑤) ≤ ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇)) ↔ (𝐹‘((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇))) ≤ ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇)))) |
318 | 317 | elrab 3363 |
. 2
⊢
(((ℂfld Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇)) ∈ {𝑤 ∈ 𝐷 ∣ (𝐹‘𝑤) ≤ ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇))} ↔ (((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇))) ≤ ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇)))) |
319 | 315, 318 | sylib 208 |
1
⊢ (𝜑 → (((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld
Σg (𝑇 ∘𝑓 · 𝑋)) / (ℂfld
Σg 𝑇))) ≤ ((ℂfld
Σg (𝑇 ∘𝑓 · (𝐹 ∘ 𝑋))) / (ℂfld
Σg 𝑇)))) |