MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jensen Structured version   Visualization version   GIF version

Theorem jensen 25006
Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015.) (Proof shortened by AV, 27-Jul-2019.)
Hypotheses
Ref Expression
jensen.1 (𝜑𝐷 ⊆ ℝ)
jensen.2 (𝜑𝐹:𝐷⟶ℝ)
jensen.3 ((𝜑 ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
jensen.4 (𝜑𝐴 ∈ Fin)
jensen.5 (𝜑𝑇:𝐴⟶(0[,)+∞))
jensen.6 (𝜑𝑋:𝐴𝐷)
jensen.7 (𝜑 → 0 < (ℂfld Σg 𝑇))
jensen.8 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
Assertion
Ref Expression
jensen (𝜑 → (((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
Distinct variable groups:   𝑎,𝑏,𝑡,𝑥,𝑦,𝐴   𝐷,𝑎,𝑏,𝑡,𝑥,𝑦   𝜑,𝑎,𝑏,𝑡,𝑥,𝑦   𝐹,𝑎,𝑏,𝑡,𝑥,𝑦   𝑇,𝑎,𝑏,𝑡,𝑥,𝑦   𝑋,𝑎,𝑏,𝑡,𝑥,𝑦

Proof of Theorem jensen
Dummy variables 𝑐 𝑘 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 jensen.7 . . . . . 6 (𝜑 → 0 < (ℂfld Σg 𝑇))
2 jensen.5 . . . . . . . . 9 (𝜑𝑇:𝐴⟶(0[,)+∞))
32ffnd 6224 . . . . . . . 8 (𝜑𝑇 Fn 𝐴)
4 fnresdm 6178 . . . . . . . 8 (𝑇 Fn 𝐴 → (𝑇𝐴) = 𝑇)
53, 4syl 17 . . . . . . 7 (𝜑 → (𝑇𝐴) = 𝑇)
65oveq2d 6858 . . . . . 6 (𝜑 → (ℂfld Σg (𝑇𝐴)) = (ℂfld Σg 𝑇))
71, 6breqtrrd 4837 . . . . 5 (𝜑 → 0 < (ℂfld Σg (𝑇𝐴)))
8 ssid 3783 . . . . 5 𝐴𝐴
97, 8jctil 515 . . . 4 (𝜑 → (𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))))
10 jensen.4 . . . . 5 (𝜑𝐴 ∈ Fin)
11 sseq1 3786 . . . . . . . . 9 (𝑎 = ∅ → (𝑎𝐴 ↔ ∅ ⊆ 𝐴))
12 reseq2 5560 . . . . . . . . . . . . 13 (𝑎 = ∅ → (𝑇𝑎) = (𝑇 ↾ ∅))
13 res0 5569 . . . . . . . . . . . . 13 (𝑇 ↾ ∅) = ∅
1412, 13syl6eq 2815 . . . . . . . . . . . 12 (𝑎 = ∅ → (𝑇𝑎) = ∅)
1514oveq2d 6858 . . . . . . . . . . 11 (𝑎 = ∅ → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg ∅))
16 cnfld0 20043 . . . . . . . . . . . 12 0 = (0g‘ℂfld)
1716gsum0 17544 . . . . . . . . . . 11 (ℂfld Σg ∅) = 0
1815, 17syl6eq 2815 . . . . . . . . . 10 (𝑎 = ∅ → (ℂfld Σg (𝑇𝑎)) = 0)
1918breq2d 4821 . . . . . . . . 9 (𝑎 = ∅ → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < 0))
2011, 19anbi12d 624 . . . . . . . 8 (𝑎 = ∅ → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (∅ ⊆ 𝐴 ∧ 0 < 0)))
21 reseq2 5560 . . . . . . . . . . 11 (𝑎 = ∅ → ((𝑇𝑓 · 𝑋) ↾ 𝑎) = ((𝑇𝑓 · 𝑋) ↾ ∅))
2221oveq2d 6858 . . . . . . . . . 10 (𝑎 = ∅ → (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ ∅)))
2322, 18oveq12d 6860 . . . . . . . . 9 (𝑎 = ∅ → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ ∅)) / 0))
24 reseq2 5560 . . . . . . . . . . . . 13 (𝑎 = ∅ → ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎) = ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅))
2524oveq2d 6858 . . . . . . . . . . . 12 (𝑎 = ∅ → (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)))
2625, 18oveq12d 6860 . . . . . . . . . . 11 (𝑎 = ∅ → ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0))
2726breq2d 4821 . . . . . . . . . 10 (𝑎 = ∅ → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0)))
2827rabbidv 3338 . . . . . . . . 9 (𝑎 = ∅ → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0)})
2923, 28eleq12d 2838 . . . . . . . 8 (𝑎 = ∅ → (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0)}))
3020, 29imbi12d 335 . . . . . . 7 (𝑎 = ∅ → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0)})))
3130imbi2d 331 . . . . . 6 (𝑎 = ∅ → ((𝜑 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))})) ↔ (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0)}))))
32 sseq1 3786 . . . . . . . . 9 (𝑎 = 𝑘 → (𝑎𝐴𝑘𝐴))
33 reseq2 5560 . . . . . . . . . . 11 (𝑎 = 𝑘 → (𝑇𝑎) = (𝑇𝑘))
3433oveq2d 6858 . . . . . . . . . 10 (𝑎 = 𝑘 → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇𝑘)))
3534breq2d 4821 . . . . . . . . 9 (𝑎 = 𝑘 → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇𝑘))))
3632, 35anbi12d 624 . . . . . . . 8 (𝑎 = 𝑘 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘)))))
37 reseq2 5560 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((𝑇𝑓 · 𝑋) ↾ 𝑎) = ((𝑇𝑓 · 𝑋) ↾ 𝑘))
3837oveq2d 6858 . . . . . . . . . 10 (𝑎 = 𝑘 → (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)))
3938, 34oveq12d 6860 . . . . . . . . 9 (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
40 reseq2 5560 . . . . . . . . . . . . 13 (𝑎 = 𝑘 → ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎) = ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘))
4140oveq2d 6858 . . . . . . . . . . . 12 (𝑎 = 𝑘 → (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)))
4241, 34oveq12d 6860 . . . . . . . . . . 11 (𝑎 = 𝑘 → ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
4342breq2d 4821 . . . . . . . . . 10 (𝑎 = 𝑘 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
4443rabbidv 3338 . . . . . . . . 9 (𝑎 = 𝑘 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})
4539, 44eleq12d 2838 . . . . . . . 8 (𝑎 = 𝑘 → (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}))
4636, 45imbi12d 335 . . . . . . 7 (𝑎 = 𝑘 → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ ((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})))
4746imbi2d 331 . . . . . 6 (𝑎 = 𝑘 → ((𝜑 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))})) ↔ (𝜑 → ((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}))))
48 sseq1 3786 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → (𝑎𝐴 ↔ (𝑘 ∪ {𝑐}) ⊆ 𝐴))
49 reseq2 5560 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → (𝑇𝑎) = (𝑇 ↾ (𝑘 ∪ {𝑐})))
5049oveq2d 6858 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
5150breq2d 4821 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
5248, 51anbi12d 624 . . . . . . . 8 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
53 reseq2 5560 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇𝑓 · 𝑋) ↾ 𝑎) = ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})))
5453oveq2d 6858 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))))
5554, 50oveq12d 6860 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
56 reseq2 5560 . . . . . . . . . . . . 13 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎) = ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})))
5756oveq2d 6858 . . . . . . . . . . . 12 (𝑎 = (𝑘 ∪ {𝑐}) → (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))))
5857, 50oveq12d 6860 . . . . . . . . . . 11 (𝑎 = (𝑘 ∪ {𝑐}) → ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
5958breq2d 4821 . . . . . . . . . 10 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
6059rabbidv 3338 . . . . . . . . 9 (𝑎 = (𝑘 ∪ {𝑐}) → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
6155, 60eleq12d 2838 . . . . . . . 8 (𝑎 = (𝑘 ∪ {𝑐}) → (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
6252, 61imbi12d 335 . . . . . . 7 (𝑎 = (𝑘 ∪ {𝑐}) → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
6362imbi2d 331 . . . . . 6 (𝑎 = (𝑘 ∪ {𝑐}) → ((𝜑 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))})) ↔ (𝜑 → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
64 sseq1 3786 . . . . . . . . 9 (𝑎 = 𝐴 → (𝑎𝐴𝐴𝐴))
65 reseq2 5560 . . . . . . . . . . 11 (𝑎 = 𝐴 → (𝑇𝑎) = (𝑇𝐴))
6665oveq2d 6858 . . . . . . . . . 10 (𝑎 = 𝐴 → (ℂfld Σg (𝑇𝑎)) = (ℂfld Σg (𝑇𝐴)))
6766breq2d 4821 . . . . . . . . 9 (𝑎 = 𝐴 → (0 < (ℂfld Σg (𝑇𝑎)) ↔ 0 < (ℂfld Σg (𝑇𝐴))))
6864, 67anbi12d 624 . . . . . . . 8 (𝑎 = 𝐴 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) ↔ (𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴)))))
69 reseq2 5560 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((𝑇𝑓 · 𝑋) ↾ 𝑎) = ((𝑇𝑓 · 𝑋) ↾ 𝐴))
7069oveq2d 6858 . . . . . . . . . 10 (𝑎 = 𝐴 → (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) = (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)))
7170, 66oveq12d 6860 . . . . . . . . 9 (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))))
72 reseq2 5560 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎) = ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴))
7372oveq2d 6858 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) = (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)))
7473, 66oveq12d 6860 . . . . . . . . . . 11 (𝑎 = 𝐴 → ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) = ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))))
7574breq2d 4821 . . . . . . . . . 10 (𝑎 = 𝐴 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))))
7675rabbidv 3338 . . . . . . . . 9 (𝑎 = 𝐴 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})
7771, 76eleq12d 2838 . . . . . . . 8 (𝑎 = 𝐴 → (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))} ↔ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))
7868, 77imbi12d 335 . . . . . . 7 (𝑎 = 𝐴 → (((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))}) ↔ ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})))
7978imbi2d 331 . . . . . 6 (𝑎 = 𝐴 → ((𝜑 → ((𝑎𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑎))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑎)) / (ℂfld Σg (𝑇𝑎)))})) ↔ (𝜑 → ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))))
80 0re 10295 . . . . . . . . . 10 0 ∈ ℝ
8180ltnri 10400 . . . . . . . . 9 ¬ 0 < 0
8281pm2.21i 117 . . . . . . . 8 (0 < 0 → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0)})
8382adantl 473 . . . . . . 7 ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0)})
8483a1i 11 . . . . . 6 (𝜑 → ((∅ ⊆ 𝐴 ∧ 0 < 0) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ ∅)) / 0) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ ∅)) / 0)}))
85 impexp 441 . . . . . . . . . . . 12 (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) ↔ (𝑘𝐴 → (0 < (ℂfld Σg (𝑇𝑘)) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})))
86 simprl 787 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
8786unssad 3952 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘𝐴)
88 simpr 477 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇𝑘))) → 0 < (ℂfld Σg (𝑇𝑘)))
89 jensen.1 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐷 ⊆ ℝ)
9089ad3antrrr 721 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐷 ⊆ ℝ)
91 jensen.2 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹:𝐷⟶ℝ)
9291ad3antrrr 721 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐹:𝐷⟶ℝ)
93 simplll 791 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝜑)
94 jensen.3 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
9593, 94sylan 575 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) ∧ (𝑎𝐷𝑏𝐷)) → (𝑎[,]𝑏) ⊆ 𝐷)
9693, 10syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝐴 ∈ Fin)
9793, 2syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝑇:𝐴⟶(0[,)+∞))
98 jensen.6 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑋:𝐴𝐷)
9993, 98syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 𝑋:𝐴𝐷)
1001ad3antrrr 721 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 0 < (ℂfld Σg 𝑇))
101 jensen.8 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (𝑥𝐷𝑦𝐷𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
10293, 101sylan 575 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) ∧ (𝑥𝐷𝑦𝐷𝑡 ∈ (0[,]1))) → (𝐹‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ≤ ((𝑡 · (𝐹𝑥)) + ((1 − 𝑡) · (𝐹𝑦))))
103 simpllr 793 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ¬ 𝑐𝑘)
10486adantr 472 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
105 eqid 2765 . . . . . . . . . . . . . . . . . 18 (ℂfld Σg (𝑇𝑘)) = (ℂfld Σg (𝑇𝑘))
106 eqid 2765 . . . . . . . . . . . . . . . . . 18 (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))
107 cnring 20041 . . . . . . . . . . . . . . . . . . . . . . 23 fld ∈ Ring
108 ringcmn 18848 . . . . . . . . . . . . . . . . . . . . . . 23 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
109107, 108mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ℂfld ∈ CMnd)
11010ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝐴 ∈ Fin)
111 ssfi 8387 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ Fin ∧ 𝑘𝐴) → 𝑘 ∈ Fin)
112110, 87, 111syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑘 ∈ Fin)
113 rege0subm 20075 . . . . . . . . . . . . . . . . . . . . . . 23 (0[,)+∞) ∈ (SubMnd‘ℂfld)
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0[,)+∞) ∈ (SubMnd‘ℂfld))
1152ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 𝑇:𝐴⟶(0[,)+∞))
116115, 87fssresd 6253 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇𝑘):𝑘⟶(0[,)+∞))
117 c0ex 10287 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ V
118117a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ∈ V)
119116, 112, 118fdmfifsupp 8492 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑇𝑘) finSupp 0)
12016, 109, 112, 114, 116, 119gsumsubmcl 18585 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞))
121 elrege0 12482 . . . . . . . . . . . . . . . . . . . . . 22 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) ↔ ((ℂfld Σg (𝑇𝑘)) ∈ ℝ ∧ 0 ≤ (ℂfld Σg (𝑇𝑘))))
122121simplbi 491 . . . . . . . . . . . . . . . . . . . . 21 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
123120, 122syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
124123adantr 472 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ)
125 simprl 787 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → 0 < (ℂfld Σg (𝑇𝑘)))
126124, 125elrpd 12067 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (ℂfld Σg (𝑇𝑘)) ∈ ℝ+)
127 simprr 789 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})
128 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) → (𝐹𝑤) = (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
129128breq1d 4819 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ↔ (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
130129elrab 3519 . . . . . . . . . . . . . . . . . . . 20 (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))} ↔ (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))))
131127, 130sylib 209 . . . . . . . . . . . . . . . . . . 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 (𝑇𝑘)))))
132131simpld 488 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ 𝐷)
133131simprd 489 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))))
13490, 92, 95, 96, 97, 99, 100, 102, 103, 104, 105, 106, 126, 132, 133jensenlem2 25005 . . . . . . . . . . . . . . . . 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
135 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (𝐹𝑤) = (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
136135breq1d 4819 . . . . . . . . . . . . . . . . . 18 (𝑤 = ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ↔ (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
137136elrab 3519 . . . . . . . . . . . . . . . . 17 (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))} ↔ (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))))
138134, 137sylibr 225 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ (0 < (ℂfld Σg (𝑇𝑘)) ∧ ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
139138expr 448 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 < (ℂfld Σg (𝑇𝑘))) → (((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))} → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
14088, 139embantd 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
141 cnfldbas 20023 . . . . . . . . . . . . . . . . . . . . 21 ℂ = (Base‘ℂfld)
142 ringmnd 18823 . . . . . . . . . . . . . . . . . . . . . 22 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
143107, 142mp1i 13 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ℂfld ∈ Mnd)
144 ssfi 8387 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ Fin ∧ (𝑘 ∪ {𝑐}) ⊆ 𝐴) → (𝑘 ∪ {𝑐}) ∈ Fin)
145110, 86, 144syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (𝑘 ∪ {𝑐}) ∈ Fin)
146145adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑘 ∪ {𝑐}) ∈ Fin)
147 ssun2 3939 . . . . . . . . . . . . . . . . . . . . . . 23 {𝑐} ⊆ (𝑘 ∪ {𝑐})
148 vsnid 4367 . . . . . . . . . . . . . . . . . . . . . . 23 𝑐 ∈ {𝑐}
149147, 148sselii 3758 . . . . . . . . . . . . . . . . . . . . . 22 𝑐 ∈ (𝑘 ∪ {𝑐})
150149a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑐 ∈ (𝑘 ∪ {𝑐}))
151 remulcl 10274 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
152151adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
153 rge0ssre 12484 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℝ
154 fss 6236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝑇:𝐴⟶ℝ)
1552, 153, 154sylancl 580 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑇:𝐴⟶ℝ)
15698, 89fssd 6237 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝑋:𝐴⟶ℝ)
157 inidm 3982 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝐴) = 𝐴
158152, 155, 156, 10, 10, 157off 7110 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑇𝑓 · 𝑋):𝐴⟶ℝ)
159 ax-resscn 10246 . . . . . . . . . . . . . . . . . . . . . . . 24 ℝ ⊆ ℂ
160 fss 6236 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑇𝑓 · 𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇𝑓 · 𝑋):𝐴⟶ℂ)
161158, 159, 160sylancl 580 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑇𝑓 · 𝑋):𝐴⟶ℂ)
162161ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑓 · 𝑋):𝐴⟶ℂ)
16386adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑘 ∪ {𝑐}) ⊆ 𝐴)
164162, 163fssresd 6253 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
1652ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇:𝐴⟶(0[,)+∞))
166110adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐴 ∈ Fin)
167 fex 6682 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑇:𝐴⟶(0[,)+∞) ∧ 𝐴 ∈ Fin) → 𝑇 ∈ V)
168165, 166, 167syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇 ∈ V)
16998ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋:𝐴𝐷)
170 fex 6682 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋:𝐴𝐷𝐴 ∈ Fin) → 𝑋 ∈ V)
171169, 166, 170syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋 ∈ V)
172 offres 7361 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 ∈ V ∧ 𝑋 ∈ V) → ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
173168, 171, 172syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 · (𝑋 ↾ (𝑘 ∪ {𝑐}))))
174173oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0))
175153, 159sstri 3770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0[,)+∞) ⊆ ℂ
176 fss 6236 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑇:𝐴⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 𝑇:𝐴⟶ℂ)
177165, 175, 176sylancl 580 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇:𝐴⟶ℂ)
178177, 163fssresd 6253 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
179 eldifi 3894 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
180179adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → 𝑥 ∈ (𝑘 ∪ {𝑐}))
181 fvres 6394 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ (𝑘 ∪ {𝑐}) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇𝑥))
182180, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = (𝑇𝑥))
183 difun2 4208 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 ∪ {𝑐}) ∖ {𝑐}) = (𝑘 ∖ {𝑐})
184 difss 3899 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 ∖ {𝑐}) ⊆ 𝑘
185183, 184eqsstri 3795 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑘 ∪ {𝑐}) ∖ {𝑐}) ⊆ 𝑘
186185sseli 3757 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐}) → 𝑥𝑘)
187 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 = (ℂfld Σg (𝑇𝑘)))
18887adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑘𝐴)
189165, 188feqresmpt 6439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑘) = (𝑥𝑘 ↦ (𝑇𝑥)))
190189oveq2d 6858 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇𝑘)) = (ℂfld Σg (𝑥𝑘 ↦ (𝑇𝑥))))
191112adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑘 ∈ Fin)
192188sselda 3761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → 𝑥𝐴)
193165ffvelrnda 6549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝐴) → (𝑇𝑥) ∈ (0[,)+∞))
194192, 193syldan 585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ (0[,)+∞))
195175, 194sseldi 3759 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ ℂ)
196191, 195gsumfsum 20086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑥𝑘 ↦ (𝑇𝑥))) = Σ𝑥𝑘 (𝑇𝑥))
197187, 190, 1963eqtrrd 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → Σ𝑥𝑘 (𝑇𝑥) = 0)
198 elrege0 12482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑇𝑥) ∈ (0[,)+∞) ↔ ((𝑇𝑥) ∈ ℝ ∧ 0 ≤ (𝑇𝑥)))
199194, 198sylib 209 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → ((𝑇𝑥) ∈ ℝ ∧ 0 ≤ (𝑇𝑥)))
200199simpld 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) ∈ ℝ)
201199simprd 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → 0 ≤ (𝑇𝑥))
202191, 200, 201fsum00 14814 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (Σ𝑥𝑘 (𝑇𝑥) = 0 ↔ ∀𝑥𝑘 (𝑇𝑥) = 0))
203197, 202mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ∀𝑥𝑘 (𝑇𝑥) = 0)
204203r19.21bi 3079 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥𝑘) → (𝑇𝑥) = 0)
205186, 204sylan2 586 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → (𝑇𝑥) = 0)
206182, 205eqtrd 2799 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ((𝑘 ∪ {𝑐}) ∖ {𝑐})) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑥) = 0)
207178, 206suppss 7528 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
208 mul02 10468 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℂ → (0 · 𝑥) = 0)
209208adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) ∧ 𝑥 ∈ ℂ) → (0 · 𝑥) = 0)
21089ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐷 ⊆ ℝ)
211210, 159syl6ss 3773 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐷 ⊆ ℂ)
212169, 211fssd 6237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋:𝐴⟶ℂ)
213212, 163fssresd 6253 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋 ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
214117a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 ∈ V)
215207, 209, 178, 213, 146, 214suppssof1 7531 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 · (𝑋 ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
216174, 215eqsstrd 3799 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
217141, 16, 143, 146, 150, 164, 216gsumpt 18627 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
218 fvres 6394 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ (𝑘 ∪ {𝑐}) → (((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇𝑓 · 𝑋)‘𝑐))
219150, 218syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇𝑓 · 𝑋)‘𝑐))
220165ffnd 6224 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑇 Fn 𝐴)
221169ffnd 6224 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑋 Fn 𝐴)
222163, 150sseldd 3762 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝑐𝐴)
223 fnfvof 7109 . . . . . . . . . . . . . . . . . . . . 21 (((𝑇 Fn 𝐴𝑋 Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐𝐴)) → ((𝑇𝑓 · 𝑋)‘𝑐) = ((𝑇𝑐) · (𝑋𝑐)))
224220, 221, 166, 222, 223syl22anc 867 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑓 · 𝑋)‘𝑐) = ((𝑇𝑐) · (𝑋𝑐)))
225217, 219, 2243eqtrd 2803 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇𝑐) · (𝑋𝑐)))
226141, 16, 143, 146, 150, 178, 207gsumpt 18627 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐))
227 fvres 6394 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ (𝑘 ∪ {𝑐}) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇𝑐))
228150, 227syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇 ↾ (𝑘 ∪ {𝑐}))‘𝑐) = (𝑇𝑐))
229226, 228eqtrd 2799 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))) = (𝑇𝑐))
230225, 229oveq12d 6860 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇𝑐) · (𝑋𝑐)) / (𝑇𝑐)))
231212, 222ffvelrnd 6550 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋𝑐) ∈ ℂ)
232177, 222ffvelrnd 6550 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑐) ∈ ℂ)
233 simplrr 796 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))
234233, 229breqtrd 4835 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 0 < (𝑇𝑐))
235234gt0ne0d 10846 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑐) ≠ 0)
236231, 232, 235divcan3d 11060 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑐) · (𝑋𝑐)) / (𝑇𝑐)) = (𝑋𝑐))
237230, 236eqtrd 2799 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝑋𝑐))
238169, 222ffvelrnd 6550 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑋𝑐) ∈ 𝐷)
239237, 238eqeltrd 2844 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ 𝐷)
24091ad3antrrr 721 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → 𝐹:𝐷⟶ℝ)
241240, 238ffvelrnd 6550 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ∈ ℝ)
242241leidd 10848 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ≤ (𝐹‘(𝑋𝑐)))
243237fveq2d 6379 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) = (𝐹‘(𝑋𝑐)))
244 fco 6240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹:𝐷⟶ℝ ∧ 𝑋:𝐴𝐷) → (𝐹𝑋):𝐴⟶ℝ)
24591, 98, 244syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹𝑋):𝐴⟶ℝ)
246152, 155, 245, 10, 10, 157off 7110 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑇𝑓 · (𝐹𝑋)):𝐴⟶ℝ)
247 fss 6236 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑇𝑓 · (𝐹𝑋)):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝑇𝑓 · (𝐹𝑋)):𝐴⟶ℂ)
248246, 159, 247sylancl 580 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑇𝑓 · (𝐹𝑋)):𝐴⟶ℂ)
249248ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝑇𝑓 · (𝐹𝑋)):𝐴⟶ℂ)
250249, 163fssresd 6253 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
251245ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋):𝐴⟶ℝ)
252 fex 6682 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑋):𝐴⟶ℝ ∧ 𝐴 ∈ Fin) → (𝐹𝑋) ∈ V)
253251, 166, 252syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋) ∈ V)
254 offres 7361 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 ∈ V ∧ (𝐹𝑋) ∈ V) → ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))))
255168, 253, 254syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) = ((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))))
256255oveq1d 6857 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) = (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0))
257 fss 6236 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑋):𝐴⟶ℝ ∧ ℝ ⊆ ℂ) → (𝐹𝑋):𝐴⟶ℂ)
258251, 159, 257sylancl 580 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋):𝐴⟶ℂ)
259258, 163fssresd 6253 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐})):(𝑘 ∪ {𝑐})⟶ℂ)
260207, 209, 178, 259, 146, 214suppssof1 7531 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇 ↾ (𝑘 ∪ {𝑐})) ∘𝑓 · ((𝐹𝑋) ↾ (𝑘 ∪ {𝑐}))) supp 0) ⊆ {𝑐})
261256, 260eqsstrd 3799 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐})) supp 0) ⊆ {𝑐})
262141, 16, 143, 146, 150, 250, 261gsumpt 18627 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) = (((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐))
263 fvres 6394 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 ∈ (𝑘 ∪ {𝑐}) → (((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇𝑓 · (𝐹𝑋))‘𝑐))
264150, 263syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))‘𝑐) = ((𝑇𝑓 · (𝐹𝑋))‘𝑐))
26591ffnd 6224 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹 Fn 𝐷)
266 fnfco 6251 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 Fn 𝐷𝑋:𝐴𝐷) → (𝐹𝑋) Fn 𝐴)
267265, 98, 266syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐹𝑋) Fn 𝐴)
268267ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹𝑋) Fn 𝐴)
269 fnfvof 7109 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑇 Fn 𝐴 ∧ (𝐹𝑋) Fn 𝐴) ∧ (𝐴 ∈ Fin ∧ 𝑐𝐴)) → ((𝑇𝑓 · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)))
270220, 268, 166, 222, 269syl22anc 867 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑓 · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)))
271 fvco3 6464 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑋:𝐴𝐷𝑐𝐴) → ((𝐹𝑋)‘𝑐) = (𝐹‘(𝑋𝑐)))
272169, 222, 271syl2anc 579 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝐹𝑋)‘𝑐) = (𝐹‘(𝑋𝑐)))
273272oveq2d 6858 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑐) · ((𝐹𝑋)‘𝑐)) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
274270, 273eqtrd 2799 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((𝑇𝑓 · (𝐹𝑋))‘𝑐) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
275262, 264, 2743eqtrd 2803 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) = ((𝑇𝑐) · (𝐹‘(𝑋𝑐))))
276275, 229oveq12d 6860 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (((𝑇𝑐) · (𝐹‘(𝑋𝑐))) / (𝑇𝑐)))
277241recnd 10322 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘(𝑋𝑐)) ∈ ℂ)
278277, 232, 235divcan3d 11060 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (((𝑇𝑐) · (𝐹‘(𝑋𝑐))) / (𝑇𝑐)) = (𝐹‘(𝑋𝑐)))
279276, 278eqtrd 2799 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) = (𝐹‘(𝑋𝑐)))
280242, 243, 2793brtr4d 4841 . . . . . . . . . . . . . . . 16 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → (𝐹‘((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))))
281239, 280, 137sylanbrc 578 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) ∧ 0 = (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})
282281a1d 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
283121simprbi 490 . . . . . . . . . . . . . . . 16 ((ℂfld Σg (𝑇𝑘)) ∈ (0[,)+∞) → 0 ≤ (ℂfld Σg (𝑇𝑘)))
284120, 283syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → 0 ≤ (ℂfld Σg (𝑇𝑘)))
285 leloe 10378 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ (ℂfld Σg (𝑇𝑘)) ∈ ℝ) → (0 ≤ (ℂfld Σg (𝑇𝑘)) ↔ (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘)))))
28680, 123, 285sylancr 581 . . . . . . . . . . . . . . 15 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 ≤ (ℂfld Σg (𝑇𝑘)) ↔ (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘)))))
287284, 286mpbid 223 . . . . . . . . . . . . . 14 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (0 < (ℂfld Σg (𝑇𝑘)) ∨ 0 = (ℂfld Σg (𝑇𝑘))))
288140, 282, 287mpjaodan 981 . . . . . . . . . . . . 13 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ((0 < (ℂfld Σg (𝑇𝑘)) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
28987, 288embantd 59 . . . . . . . . . . . 12 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → ((𝑘𝐴 → (0 < (ℂfld Σg (𝑇𝑘)) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))})) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
29085, 289syl5bi 233 . . . . . . . . . . 11 (((𝜑 ∧ ¬ 𝑐𝑘) ∧ ((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))) → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))
291290ex 401 . . . . . . . . . 10 ((𝜑 ∧ ¬ 𝑐𝑘) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
292291com23 86 . . . . . . . . 9 ((𝜑 ∧ ¬ 𝑐𝑘) → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))})))
293292expcom 402 . . . . . . . 8 𝑐𝑘 → (𝜑 → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
294293adantl 473 . . . . . . 7 ((𝑘 ∈ Fin ∧ ¬ 𝑐𝑘) → (𝜑 → (((𝑘𝐴 ∧ 0 < (ℂfld Σg (𝑇𝑘))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝑘)) / (ℂfld Σg (𝑇𝑘)))}) → (((𝑘 ∪ {𝑐}) ⊆ 𝐴 ∧ 0 < (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐})))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ (𝑘 ∪ {𝑐}))) / (ℂfld Σg (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
295294a2d 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 (𝑇 ↾ (𝑘 ∪ {𝑐}))))}))))
29631, 47, 63, 79, 84, 295findcard2s 8408 . . . . 5 (𝐴 ∈ Fin → (𝜑 → ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})))
29710, 296mpcom 38 . . . 4 (𝜑 → ((𝐴𝐴 ∧ 0 < (ℂfld Σg (𝑇𝐴))) → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))}))
2989, 297mpd 15 . . 3 (𝜑 → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))})
299158ffnd 6224 . . . . . 6 (𝜑 → (𝑇𝑓 · 𝑋) Fn 𝐴)
300 fnresdm 6178 . . . . . 6 ((𝑇𝑓 · 𝑋) Fn 𝐴 → ((𝑇𝑓 · 𝑋) ↾ 𝐴) = (𝑇𝑓 · 𝑋))
301299, 300syl 17 . . . . 5 (𝜑 → ((𝑇𝑓 · 𝑋) ↾ 𝐴) = (𝑇𝑓 · 𝑋))
302301oveq2d 6858 . . . 4 (𝜑 → (ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) = (ℂfld Σg (𝑇𝑓 · 𝑋)))
303302, 6oveq12d 6860 . . 3 (𝜑 → ((ℂfld Σg ((𝑇𝑓 · 𝑋) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) = ((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇)))
3043, 267, 10, 10, 157offn 7106 . . . . . . . 8 (𝜑 → (𝑇𝑓 · (𝐹𝑋)) Fn 𝐴)
305 fnresdm 6178 . . . . . . . 8 ((𝑇𝑓 · (𝐹𝑋)) Fn 𝐴 → ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴) = (𝑇𝑓 · (𝐹𝑋)))
306304, 305syl 17 . . . . . . 7 (𝜑 → ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴) = (𝑇𝑓 · (𝐹𝑋)))
307306oveq2d 6858 . . . . . 6 (𝜑 → (ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) = (ℂfld Σg (𝑇𝑓 · (𝐹𝑋))))
308307, 6oveq12d 6860 . . . . 5 (𝜑 → ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) = ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇)))
309308breq2d 4821 . . . 4 (𝜑 → ((𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴))) ↔ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
310309rabbidv 3338 . . 3 (𝜑 → {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg ((𝑇𝑓 · (𝐹𝑋)) ↾ 𝐴)) / (ℂfld Σg (𝑇𝐴)))} = {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇))})
311298, 303, 3103eltr3d 2858 . 2 (𝜑 → ((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇)) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇))})
312 fveq2 6375 . . . 4 (𝑤 = ((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇)) → (𝐹𝑤) = (𝐹‘((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇))))
313312breq1d 4819 . . 3 (𝑤 = ((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇)) → ((𝐹𝑤) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇)) ↔ (𝐹‘((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
314313elrab 3519 . 2 (((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇)) ∈ {𝑤𝐷 ∣ (𝐹𝑤) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇))} ↔ (((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
315311, 314sylib 209 1 (𝜑 → (((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇)) ∈ 𝐷 ∧ (𝐹‘((ℂfld Σg (𝑇𝑓 · 𝑋)) / (ℂfld Σg 𝑇))) ≤ ((ℂfld Σg (𝑇𝑓 · (𝐹𝑋))) / (ℂfld Σg 𝑇))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wral 3055  {crab 3059  Vcvv 3350  cdif 3729  cun 3730  wss 3732  c0 4079  {csn 4334   class class class wbr 4809  cmpt 4888  cres 5279  ccom 5281   Fn wfn 6063  wf 6064  cfv 6068  (class class class)co 6842  𝑓 cof 7093   supp csupp 7497  Fincfn 8160  cc 10187  cr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194  +∞cpnf 10325   < clt 10328  cle 10329  cmin 10520   / cdiv 10938  [,)cico 12379  [,]cicc 12380  Σcsu 14701   Σg cgsu 16367  Mndcmnd 17560  SubMndcsubmnd 17600  CMndccmn 18459  Ringcrg 18814  fldccnfld 20019
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267  ax-addf 10268  ax-mulf 10269
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-iin 4679  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-supp 7498  df-tpos 7555  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fsupp 8483  df-sup 8555  df-oi 8622  df-card 9016  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-4 11337  df-5 11338  df-6 11339  df-7 11340  df-8 11341  df-9 11342  df-n0 11539  df-z 11625  df-dec 11741  df-uz 11887  df-rp 12029  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-sum 14702  df-struct 16132  df-ndx 16133  df-slot 16134  df-base 16136  df-sets 16137  df-ress 16138  df-plusg 16227  df-mulr 16228  df-starv 16229  df-tset 16233  df-ple 16234  df-ds 16236  df-unif 16237  df-0g 16368  df-gsum 16369  df-mre 16512  df-mrc 16513  df-acs 16515  df-mgm 17508  df-sgrp 17550  df-mnd 17561  df-submnd 17602  df-grp 17692  df-minusg 17693  df-mulg 17808  df-subg 17855  df-cntz 18013  df-cmn 18461  df-abl 18462  df-mgp 18757  df-ur 18769  df-ring 18816  df-cring 18817  df-oppr 18890  df-dvdsr 18908  df-unit 18909  df-invr 18939  df-dvr 18950  df-drng 19018  df-subrg 19047  df-cnfld 20020  df-refld 20225
This theorem is referenced by:  amgmlem  25007  amgmwlem  43220
  Copyright terms: Public domain W3C validator