# Metamath Proof Explorer

## Theorem jensen

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)

Ref Expression
Hypotheses jensen.1 ${⊢}{\phi }\to {D}\subseteq ℝ$
jensen.2 ${⊢}{\phi }\to {F}:{D}⟶ℝ$
jensen.3 ${⊢}\left({\phi }\wedge \left({a}\in {D}\wedge {b}\in {D}\right)\right)\to \left[{a},{b}\right]\subseteq {D}$
jensen.4 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
jensen.5 ${⊢}{\phi }\to {T}:{A}⟶\left[0,\mathrm{+\infty }\right)$
jensen.6 ${⊢}{\phi }\to {X}:{A}⟶{D}$
jensen.7 ${⊢}{\phi }\to 0<{\sum }_{{ℂ}_{\mathrm{fld}}}{T}$
jensen.8 ${⊢}\left({\phi }\wedge \left({x}\in {D}\wedge {y}\in {D}\wedge {t}\in \left[0,1\right]\right)\right)\to {F}\left({t}{x}+\left(1-{t}\right){y}\right)\le {t}{F}\left({x}\right)+\left(1-{t}\right){F}\left({y}\right)$
Assertion jensen ${⊢}{\phi }\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)$

### Proof

Step Hyp Ref Expression
1 jensen.1 ${⊢}{\phi }\to {D}\subseteq ℝ$
2 jensen.2 ${⊢}{\phi }\to {F}:{D}⟶ℝ$
3 jensen.3 ${⊢}\left({\phi }\wedge \left({a}\in {D}\wedge {b}\in {D}\right)\right)\to \left[{a},{b}\right]\subseteq {D}$
4 jensen.4 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
5 jensen.5 ${⊢}{\phi }\to {T}:{A}⟶\left[0,\mathrm{+\infty }\right)$
6 jensen.6 ${⊢}{\phi }\to {X}:{A}⟶{D}$
7 jensen.7 ${⊢}{\phi }\to 0<{\sum }_{{ℂ}_{\mathrm{fld}}}{T}$
8 jensen.8 ${⊢}\left({\phi }\wedge \left({x}\in {D}\wedge {y}\in {D}\wedge {t}\in \left[0,1\right]\right)\right)\to {F}\left({t}{x}+\left(1-{t}\right){y}\right)\le {t}{F}\left({x}\right)+\left(1-{t}\right){F}\left({y}\right)$
9 5 ffnd ${⊢}{\phi }\to {T}Fn{A}$
10 fnresdm ${⊢}{T}Fn{A}\to {{T}↾}_{{A}}={T}$
11 9 10 syl ${⊢}{\phi }\to {{T}↾}_{{A}}={T}$
12 11 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}{T}$
13 7 12 breqtrrd ${⊢}{\phi }\to 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)$
14 ssid ${⊢}{A}\subseteq {A}$
15 13 14 jctil ${⊢}{\phi }\to \left({A}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)\right)$
16 sseq1 ${⊢}{a}=\varnothing \to \left({a}\subseteq {A}↔\varnothing \subseteq {A}\right)$
17 reseq2 ${⊢}{a}=\varnothing \to {{T}↾}_{{a}}={{T}↾}_{\varnothing }$
18 res0 ${⊢}{{T}↾}_{\varnothing }=\varnothing$
19 17 18 eqtrdi ${⊢}{a}=\varnothing \to {{T}↾}_{{a}}=\varnothing$
20 19 oveq2d ${⊢}{a}=\varnothing \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\varnothing$
21 cnfld0 ${⊢}0={0}_{{ℂ}_{\mathrm{fld}}}$
22 21 gsum0 ${⊢}{\sum }_{{ℂ}_{\mathrm{fld}}}\varnothing =0$
23 20 22 eqtrdi ${⊢}{a}=\varnothing \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)=0$
24 23 breq2d ${⊢}{a}=\varnothing \to \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)↔0<0\right)$
25 16 24 anbi12d ${⊢}{a}=\varnothing \to \left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)↔\left(\varnothing \subseteq {A}\wedge 0<0\right)\right)$
26 reseq2 ${⊢}{a}=\varnothing \to {\left({T}{×}_{f}{X}\right)↾}_{{a}}={\left({T}{×}_{f}{X}\right)↾}_{\varnothing }$
27 26 oveq2d ${⊢}{a}=\varnothing \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\varnothing }\right)$
28 27 23 oveq12d ${⊢}{a}=\varnothing \to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\varnothing }\right)}{0}$
29 reseq2 ${⊢}{a}=\varnothing \to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}={\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }$
30 29 oveq2d ${⊢}{a}=\varnothing \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)$
31 30 23 oveq12d ${⊢}{a}=\varnothing \to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}$
32 31 breq2d ${⊢}{a}=\varnothing \to \left({F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}↔{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}\right)$
33 32 rabbidv ${⊢}{a}=\varnothing \to \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}=\left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}\right\}$
34 28 33 eleq12d ${⊢}{a}=\varnothing \to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}↔\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\varnothing }\right)}{0}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}\right\}\right)$
35 25 34 imbi12d ${⊢}{a}=\varnothing \to \left(\left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}\right)↔\left(\left(\varnothing \subseteq {A}\wedge 0<0\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\varnothing }\right)}{0}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}\right\}\right)\right)$
36 35 imbi2d ${⊢}{a}=\varnothing \to \left(\left({\phi }\to \left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}\right)\right)↔\left({\phi }\to \left(\left(\varnothing \subseteq {A}\wedge 0<0\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\varnothing }\right)}{0}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}\right\}\right)\right)\right)$
37 sseq1 ${⊢}{a}={k}\to \left({a}\subseteq {A}↔{k}\subseteq {A}\right)$
38 reseq2 ${⊢}{a}={k}\to {{T}↾}_{{a}}={{T}↾}_{{k}}$
39 38 oveq2d ${⊢}{a}={k}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)$
40 39 breq2d ${⊢}{a}={k}\to \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)↔0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)$
41 37 40 anbi12d ${⊢}{a}={k}\to \left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)↔\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\right)$
42 reseq2 ${⊢}{a}={k}\to {\left({T}{×}_{f}{X}\right)↾}_{{a}}={\left({T}{×}_{f}{X}\right)↾}_{{k}}$
43 42 oveq2d ${⊢}{a}={k}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)$
44 43 39 oveq12d ${⊢}{a}={k}\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}$
45 reseq2 ${⊢}{a}={k}\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}={\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}$
46 45 oveq2d ${⊢}{a}={k}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)$
47 46 39 oveq12d ${⊢}{a}={k}\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}$
48 47 breq2d ${⊢}{a}={k}\to \left({F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}↔{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)$
49 48 rabbidv ${⊢}{a}={k}\to \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}=\left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}$
50 44 49 eleq12d ${⊢}{a}={k}\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}↔\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)$
51 41 50 imbi12d ${⊢}{a}={k}\to \left(\left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}\right)↔\left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)$
52 51 imbi2d ${⊢}{a}={k}\to \left(\left({\phi }\to \left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}\right)\right)↔\left({\phi }\to \left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\right)$
53 sseq1 ${⊢}{a}={k}\cup \left\{{c}\right\}\to \left({a}\subseteq {A}↔{k}\cup \left\{{c}\right\}\subseteq {A}\right)$
54 reseq2 ${⊢}{a}={k}\cup \left\{{c}\right\}\to {{T}↾}_{{a}}={{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}$
55 54 oveq2d ${⊢}{a}={k}\cup \left\{{c}\right\}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
56 55 breq2d ${⊢}{a}={k}\cup \left\{{c}\right\}\to \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)↔0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)$
57 53 56 anbi12d ${⊢}{a}={k}\cup \left\{{c}\right\}\to \left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)↔\left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)$
58 reseq2 ${⊢}{a}={k}\cup \left\{{c}\right\}\to {\left({T}{×}_{f}{X}\right)↾}_{{a}}={\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}$
59 58 oveq2d ${⊢}{a}={k}\cup \left\{{c}\right\}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
60 59 55 oveq12d ${⊢}{a}={k}\cup \left\{{c}\right\}\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}$
61 reseq2 ${⊢}{a}={k}\cup \left\{{c}\right\}\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}={\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}$
62 61 oveq2d ${⊢}{a}={k}\cup \left\{{c}\right\}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
63 62 55 oveq12d ${⊢}{a}={k}\cup \left\{{c}\right\}\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}$
64 63 breq2d ${⊢}{a}={k}\cup \left\{{c}\right\}\to \left({F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}↔{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)$
65 64 rabbidv ${⊢}{a}={k}\cup \left\{{c}\right\}\to \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}=\left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}$
66 60 65 eleq12d ${⊢}{a}={k}\cup \left\{{c}\right\}\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}↔\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)$
67 57 66 imbi12d ${⊢}{a}={k}\cup \left\{{c}\right\}\to \left(\left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}\right)↔\left(\left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)\right)$
68 67 imbi2d ${⊢}{a}={k}\cup \left\{{c}\right\}\to \left(\left({\phi }\to \left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}\right)\right)↔\left({\phi }\to \left(\left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)\right)\right)$
69 sseq1 ${⊢}{a}={A}\to \left({a}\subseteq {A}↔{A}\subseteq {A}\right)$
70 reseq2 ${⊢}{a}={A}\to {{T}↾}_{{a}}={{T}↾}_{{A}}$
71 70 oveq2d ${⊢}{a}={A}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)$
72 71 breq2d ${⊢}{a}={A}\to \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)↔0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)\right)$
73 69 72 anbi12d ${⊢}{a}={A}\to \left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)↔\left({A}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)\right)\right)$
74 reseq2 ${⊢}{a}={A}\to {\left({T}{×}_{f}{X}\right)↾}_{{a}}={\left({T}{×}_{f}{X}\right)↾}_{{A}}$
75 74 oveq2d ${⊢}{a}={A}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)$
76 75 71 oveq12d ${⊢}{a}={A}\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}$
77 reseq2 ${⊢}{a}={A}\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}={\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}$
78 77 oveq2d ${⊢}{a}={A}\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)$
79 78 71 oveq12d ${⊢}{a}={A}\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}$
80 79 breq2d ${⊢}{a}={A}\to \left({F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}↔{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right)$
81 80 rabbidv ${⊢}{a}={A}\to \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}=\left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right\}$
82 76 81 eleq12d ${⊢}{a}={A}\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}↔\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right\}\right)$
83 73 82 imbi12d ${⊢}{a}={A}\to \left(\left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}\right)↔\left(\left({A}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right\}\right)\right)$
84 83 imbi2d ${⊢}{a}={A}\to \left(\left({\phi }\to \left(\left({a}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{a}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{a}}\right)}\right\}\right)\right)↔\left({\phi }\to \left(\left({A}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right\}\right)\right)\right)$
85 0re ${⊢}0\in ℝ$
86 85 ltnri ${⊢}¬0<0$
87 86 pm2.21i ${⊢}0<0\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\varnothing }\right)}{0}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}\right\}$
88 87 adantl ${⊢}\left(\varnothing \subseteq {A}\wedge 0<0\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\varnothing }\right)}{0}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}\right\}$
89 88 a1i ${⊢}{\phi }\to \left(\left(\varnothing \subseteq {A}\wedge 0<0\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\varnothing }\right)}{0}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\varnothing }\right)}{0}\right\}\right)$
90 impexp ${⊢}\left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)↔\left({k}\subseteq {A}\to \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)$
91 simprl ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {k}\cup \left\{{c}\right\}\subseteq {A}$
92 91 unssad ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {k}\subseteq {A}$
93 simpr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)$
94 1 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {D}\subseteq ℝ$
95 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {F}:{D}⟶ℝ$
96 simplll ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {\phi }$
97 96 3 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\wedge \left({a}\in {D}\wedge {b}\in {D}\right)\right)\to \left[{a},{b}\right]\subseteq {D}$
98 96 4 syl ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {A}\in \mathrm{Fin}$
99 96 5 syl ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {T}:{A}⟶\left[0,\mathrm{+\infty }\right)$
100 96 6 syl ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {X}:{A}⟶{D}$
101 7 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to 0<{\sum }_{{ℂ}_{\mathrm{fld}}}{T}$
102 96 8 sylan ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\wedge \left({x}\in {D}\wedge {y}\in {D}\wedge {t}\in \left[0,1\right]\right)\right)\to {F}\left({t}{x}+\left(1-{t}\right){y}\right)\le {t}{F}\left({x}\right)+\left(1-{t}\right){F}\left({y}\right)$
103 simpllr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to ¬{c}\in {k}$
104 91 adantr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {k}\cup \left\{{c}\right\}\subseteq {A}$
105 eqid ${⊢}{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)$
106 eqid ${⊢}{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
107 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
108 ringcmn ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
109 107 108 mp1i ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
110 4 ad2antrr ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {A}\in \mathrm{Fin}$
111 110 92 ssfid ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {k}\in \mathrm{Fin}$
112 rege0subm ${⊢}\left[0,\mathrm{+\infty }\right)\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$
113 112 a1i ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to \left[0,\mathrm{+\infty }\right)\in \mathrm{SubMnd}\left({ℂ}_{\mathrm{fld}}\right)$
114 5 ad2antrr ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {T}:{A}⟶\left[0,\mathrm{+\infty }\right)$
115 114 92 fssresd ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to \left({{T}↾}_{{k}}\right):{k}⟶\left[0,\mathrm{+\infty }\right)$
116 c0ex ${⊢}0\in \mathrm{V}$
117 116 a1i ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to 0\in \mathrm{V}$
118 115 111 117 fdmfifsupp ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {finSupp}_{0}\left(\left({{T}↾}_{{k}}\right)\right)$
119 21 109 111 113 115 118 gsumsubmcl ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in \left[0,\mathrm{+\infty }\right)$
120 elrege0 ${⊢}{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in ℝ\wedge 0\le {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)$
121 120 simplbi ${⊢}{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in \left[0,\mathrm{+\infty }\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in ℝ$
122 119 121 syl ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in ℝ$
123 122 adantr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in ℝ$
124 simprl ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)$
125 123 124 elrpd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in {ℝ}^{+}$
126 simprr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}$
127 fveq2 ${⊢}{w}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\to {F}\left({w}\right)={F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)$
128 127 breq1d ${⊢}{w}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\to \left({F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}↔{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)$
129 128 elrab ${⊢}\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}↔\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)$
130 126 129 sylib ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)$
131 130 simpld ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in {D}$
132 130 simprd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}$
133 94 95 97 98 99 100 101 102 103 104 105 106 125 131 132 jensenlem2 ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)$
134 fveq2 ${⊢}{w}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\to {F}\left({w}\right)={F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)$
135 134 breq1d ${⊢}{w}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\to \left({F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}↔{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)$
136 135 elrab ${⊢}\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}↔\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)$
137 133 136 sylibr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}$
138 137 expr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)$
139 93 138 embantd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left(\left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)$
140 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
141 ringmnd ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$
142 107 141 mp1i ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {ℂ}_{\mathrm{fld}}\in \mathrm{Mnd}$
143 110 91 ssfid ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to {k}\cup \left\{{c}\right\}\in \mathrm{Fin}$
144 143 adantr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {k}\cup \left\{{c}\right\}\in \mathrm{Fin}$
145 ssun2 ${⊢}\left\{{c}\right\}\subseteq {k}\cup \left\{{c}\right\}$
146 vsnid ${⊢}{c}\in \left\{{c}\right\}$
147 145 146 sselii ${⊢}{c}\in \left({k}\cup \left\{{c}\right\}\right)$
148 147 a1i ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {c}\in \left({k}\cup \left\{{c}\right\}\right)$
149 remulcl ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {x}{y}\in ℝ$
150 149 adantl ${⊢}\left({\phi }\wedge \left({x}\in ℝ\wedge {y}\in ℝ\right)\right)\to {x}{y}\in ℝ$
151 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
152 fss ${⊢}\left({T}:{A}⟶\left[0,\mathrm{+\infty }\right)\wedge \left[0,\mathrm{+\infty }\right)\subseteq ℝ\right)\to {T}:{A}⟶ℝ$
153 5 151 152 sylancl ${⊢}{\phi }\to {T}:{A}⟶ℝ$
154 6 1 fssd ${⊢}{\phi }\to {X}:{A}⟶ℝ$
155 inidm ${⊢}{A}\cap {A}={A}$
156 150 153 154 4 4 155 off ${⊢}{\phi }\to \left({T}{×}_{f}{X}\right):{A}⟶ℝ$
157 ax-resscn ${⊢}ℝ\subseteq ℂ$
158 fss ${⊢}\left(\left({T}{×}_{f}{X}\right):{A}⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \left({T}{×}_{f}{X}\right):{A}⟶ℂ$
159 156 157 158 sylancl ${⊢}{\phi }\to \left({T}{×}_{f}{X}\right):{A}⟶ℂ$
160 159 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({T}{×}_{f}{X}\right):{A}⟶ℂ$
161 91 adantr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {k}\cup \left\{{c}\right\}\subseteq {A}$
162 160 161 fssresd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right):{k}\cup \left\{{c}\right\}⟶ℂ$
163 5 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {T}:{A}⟶\left[0,\mathrm{+\infty }\right)$
164 110 adantr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {A}\in \mathrm{Fin}$
165 fex ${⊢}\left({T}:{A}⟶\left[0,\mathrm{+\infty }\right)\wedge {A}\in \mathrm{Fin}\right)\to {T}\in \mathrm{V}$
166 163 164 165 syl2anc ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {T}\in \mathrm{V}$
167 6 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {X}:{A}⟶{D}$
168 fex ${⊢}\left({X}:{A}⟶{D}\wedge {A}\in \mathrm{Fin}\right)\to {X}\in \mathrm{V}$
169 167 164 168 syl2anc ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {X}\in \mathrm{V}$
170 offres ${⊢}\left({T}\in \mathrm{V}\wedge {X}\in \mathrm{V}\right)\to {\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}=\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right){×}_{f}\left({{X}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
171 166 169 170 syl2anc ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}=\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right){×}_{f}\left({{X}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
172 171 oveq1d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\mathrm{supp}0=\left(\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right){×}_{f}\left({{X}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\mathrm{supp}0$
173 151 157 sstri ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℂ$
174 fss ${⊢}\left({T}:{A}⟶\left[0,\mathrm{+\infty }\right)\wedge \left[0,\mathrm{+\infty }\right)\subseteq ℂ\right)\to {T}:{A}⟶ℂ$
175 163 173 174 sylancl ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {T}:{A}⟶ℂ$
176 175 161 fssresd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right):{k}\cup \left\{{c}\right\}⟶ℂ$
177 eldifi ${⊢}{x}\in \left(\left({k}\cup \left\{{c}\right\}\right)\setminus \left\{{c}\right\}\right)\to {x}\in \left({k}\cup \left\{{c}\right\}\right)$
178 177 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in \left(\left({k}\cup \left\{{c}\right\}\right)\setminus \left\{{c}\right\}\right)\right)\to {x}\in \left({k}\cup \left\{{c}\right\}\right)$
179 178 fvresd ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in \left(\left({k}\cup \left\{{c}\right\}\right)\setminus \left\{{c}\right\}\right)\right)\to \left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\left({x}\right)={T}\left({x}\right)$
180 difun2 ${⊢}\left({k}\cup \left\{{c}\right\}\right)\setminus \left\{{c}\right\}={k}\setminus \left\{{c}\right\}$
181 difss ${⊢}{k}\setminus \left\{{c}\right\}\subseteq {k}$
182 180 181 eqsstri ${⊢}\left({k}\cup \left\{{c}\right\}\right)\setminus \left\{{c}\right\}\subseteq {k}$
183 182 sseli ${⊢}{x}\in \left(\left({k}\cup \left\{{c}\right\}\right)\setminus \left\{{c}\right\}\right)\to {x}\in {k}$
184 simpr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)$
185 92 adantr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {k}\subseteq {A}$
186 163 185 feqresmpt ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {{T}↾}_{{k}}=\left({x}\in {k}⟼{T}\left({x}\right)\right)$
187 186 oveq2d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)=\underset{{x}\in {k}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right)$
188 111 adantr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {k}\in \mathrm{Fin}$
189 185 sselda ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in {k}\right)\to {x}\in {A}$
190 163 ffvelrnda ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in {A}\right)\to {T}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
191 189 190 syldan ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in {k}\right)\to {T}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
192 173 191 sseldi ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in {k}\right)\to {T}\left({x}\right)\in ℂ$
193 188 192 gsumfsum ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \underset{{x}\in {k}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right)=\sum _{{x}\in {k}}{T}\left({x}\right)$
194 184 187 193 3eqtrrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \sum _{{x}\in {k}}{T}\left({x}\right)=0$
195 elrege0 ${⊢}{T}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({T}\left({x}\right)\in ℝ\wedge 0\le {T}\left({x}\right)\right)$
196 191 195 sylib ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in {k}\right)\to \left({T}\left({x}\right)\in ℝ\wedge 0\le {T}\left({x}\right)\right)$
197 196 simpld ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in {k}\right)\to {T}\left({x}\right)\in ℝ$
198 196 simprd ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in {k}\right)\to 0\le {T}\left({x}\right)$
199 188 197 198 fsum00 ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left(\sum _{{x}\in {k}}{T}\left({x}\right)=0↔\forall {x}\in {k}\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)=0\right)$
200 194 199 mpbid ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \forall {x}\in {k}\phantom{\rule{.4em}{0ex}}{T}\left({x}\right)=0$
201 200 r19.21bi ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in {k}\right)\to {T}\left({x}\right)=0$
202 183 201 sylan2 ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in \left(\left({k}\cup \left\{{c}\right\}\right)\setminus \left\{{c}\right\}\right)\right)\to {T}\left({x}\right)=0$
203 179 202 eqtrd ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in \left(\left({k}\cup \left\{{c}\right\}\right)\setminus \left\{{c}\right\}\right)\right)\to \left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\left({x}\right)=0$
204 176 203 suppss ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\mathrm{supp}0\subseteq \left\{{c}\right\}$
205 mul02 ${⊢}{x}\in ℂ\to 0\cdot {x}=0$
206 205 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\wedge {x}\in ℂ\right)\to 0\cdot {x}=0$
207 1 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {D}\subseteq ℝ$
208 207 157 sstrdi ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {D}\subseteq ℂ$
209 167 208 fssd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {X}:{A}⟶ℂ$
210 209 161 fssresd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({{X}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right):{k}\cup \left\{{c}\right\}⟶ℂ$
211 116 a1i ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to 0\in \mathrm{V}$
212 204 206 176 210 144 211 suppssof1 ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left(\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right){×}_{f}\left({{X}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\mathrm{supp}0\subseteq \left\{{c}\right\}$
213 172 212 eqsstrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\mathrm{supp}0\subseteq \left\{{c}\right\}$
214 140 21 142 144 148 162 213 gsumpt ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)=\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\left({c}\right)$
215 148 fvresd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\left({c}\right)=\left({T}{×}_{f}{X}\right)\left({c}\right)$
216 163 ffnd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {T}Fn{A}$
217 167 ffnd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {X}Fn{A}$
218 161 148 sseldd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {c}\in {A}$
219 fnfvof ${⊢}\left(\left({T}Fn{A}\wedge {X}Fn{A}\right)\wedge \left({A}\in \mathrm{Fin}\wedge {c}\in {A}\right)\right)\to \left({T}{×}_{f}{X}\right)\left({c}\right)={T}\left({c}\right){X}\left({c}\right)$
220 216 217 164 218 219 syl22anc ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({T}{×}_{f}{X}\right)\left({c}\right)={T}\left({c}\right){X}\left({c}\right)$
221 214 215 220 3eqtrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)={T}\left({c}\right){X}\left({c}\right)$
222 140 21 142 144 148 176 204 gsumpt ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)=\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\left({c}\right)$
223 148 fvresd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\left({c}\right)={T}\left({c}\right)$
224 222 223 eqtrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)={T}\left({c}\right)$
225 221 224 oveq12d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}=\frac{{T}\left({c}\right){X}\left({c}\right)}{{T}\left({c}\right)}$
226 209 218 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {X}\left({c}\right)\in ℂ$
227 175 218 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {T}\left({c}\right)\in ℂ$
228 simplrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
229 228 224 breqtrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to 0<{T}\left({c}\right)$
230 229 gt0ne0d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {T}\left({c}\right)\ne 0$
231 226 227 230 divcan3d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{T}\left({c}\right){X}\left({c}\right)}{{T}\left({c}\right)}={X}\left({c}\right)$
232 225 231 eqtrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}={X}\left({c}\right)$
233 167 218 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {X}\left({c}\right)\in {D}$
234 232 233 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in {D}$
235 2 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {F}:{D}⟶ℝ$
236 235 233 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {F}\left({X}\left({c}\right)\right)\in ℝ$
237 236 leidd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {F}\left({X}\left({c}\right)\right)\le {F}\left({X}\left({c}\right)\right)$
238 232 fveq2d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)={F}\left({X}\left({c}\right)\right)$
239 fco ${⊢}\left({F}:{D}⟶ℝ\wedge {X}:{A}⟶{D}\right)\to \left({F}\circ {X}\right):{A}⟶ℝ$
240 2 6 239 syl2anc ${⊢}{\phi }\to \left({F}\circ {X}\right):{A}⟶ℝ$
241 150 153 240 4 4 155 off ${⊢}{\phi }\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right):{A}⟶ℝ$
242 fss ${⊢}\left(\left({T}{×}_{f}\left({F}\circ {X}\right)\right):{A}⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right):{A}⟶ℂ$
243 241 157 242 sylancl ${⊢}{\phi }\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right):{A}⟶ℂ$
244 243 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right):{A}⟶ℂ$
245 244 161 fssresd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right):{k}\cup \left\{{c}\right\}⟶ℂ$
246 240 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({F}\circ {X}\right):{A}⟶ℝ$
247 fex ${⊢}\left(\left({F}\circ {X}\right):{A}⟶ℝ\wedge {A}\in \mathrm{Fin}\right)\to {F}\circ {X}\in \mathrm{V}$
248 246 164 247 syl2anc ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {F}\circ {X}\in \mathrm{V}$
249 offres ${⊢}\left({T}\in \mathrm{V}\wedge {F}\circ {X}\in \mathrm{V}\right)\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}=\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right){×}_{f}\left({\left({F}\circ {X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
250 166 248 249 syl2anc ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}=\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right){×}_{f}\left({\left({F}\circ {X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)$
251 250 oveq1d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\mathrm{supp}0=\left(\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right){×}_{f}\left({\left({F}\circ {X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\mathrm{supp}0$
252 fss ${⊢}\left(\left({F}\circ {X}\right):{A}⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \left({F}\circ {X}\right):{A}⟶ℂ$
253 246 157 252 sylancl ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({F}\circ {X}\right):{A}⟶ℂ$
254 253 161 fssresd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({F}\circ {X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right):{k}\cup \left\{{c}\right\}⟶ℂ$
255 204 206 176 254 144 211 suppssof1 ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left(\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right){×}_{f}\left({\left({F}\circ {X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\mathrm{supp}0\subseteq \left\{{c}\right\}$
256 251 255 eqsstrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\mathrm{supp}0\subseteq \left\{{c}\right\}$
257 140 21 142 144 148 245 256 gsumpt ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)=\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\left({c}\right)$
258 148 fvresd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\left({c}\right)=\left({T}{×}_{f}\left({F}\circ {X}\right)\right)\left({c}\right)$
259 2 ffnd ${⊢}{\phi }\to {F}Fn{D}$
260 fnfco ${⊢}\left({F}Fn{D}\wedge {X}:{A}⟶{D}\right)\to \left({F}\circ {X}\right)Fn{A}$
261 259 6 260 syl2anc ${⊢}{\phi }\to \left({F}\circ {X}\right)Fn{A}$
262 261 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({F}\circ {X}\right)Fn{A}$
263 fnfvof ${⊢}\left(\left({T}Fn{A}\wedge \left({F}\circ {X}\right)Fn{A}\right)\wedge \left({A}\in \mathrm{Fin}\wedge {c}\in {A}\right)\right)\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right)\left({c}\right)={T}\left({c}\right)\left({F}\circ {X}\right)\left({c}\right)$
264 216 262 164 218 263 syl22anc ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right)\left({c}\right)={T}\left({c}\right)\left({F}\circ {X}\right)\left({c}\right)$
265 fvco3 ${⊢}\left({X}:{A}⟶{D}\wedge {c}\in {A}\right)\to \left({F}\circ {X}\right)\left({c}\right)={F}\left({X}\left({c}\right)\right)$
266 167 218 265 syl2anc ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({F}\circ {X}\right)\left({c}\right)={F}\left({X}\left({c}\right)\right)$
267 266 oveq2d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {T}\left({c}\right)\left({F}\circ {X}\right)\left({c}\right)={T}\left({c}\right){F}\left({X}\left({c}\right)\right)$
268 264 267 eqtrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right)\left({c}\right)={T}\left({c}\right){F}\left({X}\left({c}\right)\right)$
269 257 258 268 3eqtrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)={T}\left({c}\right){F}\left({X}\left({c}\right)\right)$
270 269 224 oveq12d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}=\frac{{T}\left({c}\right){F}\left({X}\left({c}\right)\right)}{{T}\left({c}\right)}$
271 236 recnd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {F}\left({X}\left({c}\right)\right)\in ℂ$
272 271 227 230 divcan3d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{T}\left({c}\right){F}\left({X}\left({c}\right)\right)}{{T}\left({c}\right)}={F}\left({X}\left({c}\right)\right)$
273 270 272 eqtrd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}={F}\left({X}\left({c}\right)\right)$
274 237 238 273 3brtr4d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}$
275 135 234 274 elrabd ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}$
276 275 a1d ${⊢}\left(\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\wedge 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \left(\left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)$
277 120 simprbi ${⊢}{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in \left[0,\mathrm{+\infty }\right)\to 0\le {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)$
278 119 277 syl ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to 0\le {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)$
279 leloe ${⊢}\left(0\in ℝ\wedge {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\in ℝ\right)\to \left(0\le {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)↔\left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\vee 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\right)$
280 85 122 279 sylancr ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to \left(0\le {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)↔\left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\vee 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\right)$
281 278 280 mpbid ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\vee 0={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)$
282 139 276 281 mpjaodan ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to \left(\left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)$
283 92 282 embantd ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to \left(\left({k}\subseteq {A}\to \left(0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)$
284 90 283 syl5bi ${⊢}\left(\left({\phi }\wedge ¬{c}\in {k}\right)\wedge \left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\right)\to \left(\left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)$
285 284 ex ${⊢}\left({\phi }\wedge ¬{c}\in {k}\right)\to \left(\left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\to \left(\left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)\right)$
286 285 com23 ${⊢}\left({\phi }\wedge ¬{c}\in {k}\right)\to \left(\left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\to \left(\left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)\right)$
287 286 expcom ${⊢}¬{c}\in {k}\to \left({\phi }\to \left(\left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\to \left(\left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)\right)\right)$
288 287 adantl ${⊢}\left({k}\in \mathrm{Fin}\wedge ¬{c}\in {k}\right)\to \left({\phi }\to \left(\left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\to \left(\left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)\right)\right)$
289 288 a2d ${⊢}\left({k}\in \mathrm{Fin}\wedge ¬{c}\in {k}\right)\to \left(\left({\phi }\to \left(\left({k}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{k}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{k}}\right)}\right\}\right)\right)\to \left({\phi }\to \left(\left({k}\cup \left\{{c}\right\}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({k}\cup \left\{{c}\right\}\right)}\right)}\right\}\right)\right)\right)$
290 36 52 68 84 89 289 findcard2s ${⊢}{A}\in \mathrm{Fin}\to \left({\phi }\to \left(\left({A}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right\}\right)\right)$
291 4 290 mpcom ${⊢}{\phi }\to \left(\left({A}\subseteq {A}\wedge 0<{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)\right)\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right\}\right)$
292 15 291 mpd ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right\}$
293 156 ffnd ${⊢}{\phi }\to \left({T}{×}_{f}{X}\right)Fn{A}$
294 fnresdm ${⊢}\left({T}{×}_{f}{X}\right)Fn{A}\to {\left({T}{×}_{f}{X}\right)↾}_{{A}}={T}{×}_{f}{X}$
295 293 294 syl ${⊢}{\phi }\to {\left({T}{×}_{f}{X}\right)↾}_{{A}}={T}{×}_{f}{X}$
296 295 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)$
297 296 12 oveq12d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}$
298 9 261 4 4 155 offn ${⊢}{\phi }\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right)Fn{A}$
299 fnresdm ${⊢}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)Fn{A}\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}={T}{×}_{f}\left({F}\circ {X}\right)$
300 298 299 syl ${⊢}{\phi }\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}={T}{×}_{f}\left({F}\circ {X}\right)$
301 300 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)={\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)$
302 301 12 oveq12d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}$
303 302 breq2d ${⊢}{\phi }\to \left({F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}↔{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)$
304 303 rabbidv ${⊢}{\phi }\to \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{A}}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{A}}\right)}\right\}=\left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right\}$
305 292 297 304 3eltr3d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right\}$
306 fveq2 ${⊢}{w}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\to {F}\left({w}\right)={F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)$
307 306 breq1d ${⊢}{w}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\to \left({F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}↔{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)$
308 307 elrab ${⊢}\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\in \left\{{w}\in {D}|{F}\left({w}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right\}↔\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)$
309 305 308 sylib ${⊢}{\phi }\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}{X}\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({T}{×}_{f}\left({F}\circ {X}\right)\right)}{{\sum }_{{ℂ}_{\mathrm{fld}}}{T}}\right)$