# Metamath Proof Explorer

## Theorem jensenlem2

Description: Lemma for jensen . (Contributed by Mario Carneiro, 21-Jun-2015)

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)$
jensenlem.1 ${⊢}{\phi }\to ¬{z}\in {B}$
jensenlem.2 ${⊢}{\phi }\to {B}\cup \left\{{z}\right\}\subseteq {A}$
jensenlem.s ${⊢}{S}={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{B}}\right)$
jensenlem.l ${⊢}{L}={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)$
jensenlem.3 ${⊢}{\phi }\to {S}\in {ℝ}^{+}$
jensenlem.4 ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\in {D}$
jensenlem.5 ${⊢}{\phi }\to {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}$
Assertion jensenlem2 ${⊢}{\phi }\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\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 jensenlem.1 ${⊢}{\phi }\to ¬{z}\in {B}$
10 jensenlem.2 ${⊢}{\phi }\to {B}\cup \left\{{z}\right\}\subseteq {A}$
11 jensenlem.s ${⊢}{S}={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{B}}\right)$
12 jensenlem.l ${⊢}{L}={\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)$
13 jensenlem.3 ${⊢}{\phi }\to {S}\in {ℝ}^{+}$
14 jensenlem.4 ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\in {D}$
15 jensenlem.5 ${⊢}{\phi }\to {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}$
16 cnfld0 ${⊢}0={0}_{{ℂ}_{\mathrm{fld}}}$
17 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
18 ringabl ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{Abel}$
19 17 18 mp1i ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}\in \mathrm{Abel}$
20 10 unssad ${⊢}{\phi }\to {B}\subseteq {A}$
21 4 20 ssfid ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
22 resubdrg ${⊢}\left(ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℝ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$
23 22 simpli ${⊢}ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$
24 subrgsubg ${⊢}ℝ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
25 23 24 mp1i ${⊢}{\phi }\to ℝ\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$
26 remulcl ${⊢}\left({x}\in ℝ\wedge {y}\in ℝ\right)\to {x}{y}\in ℝ$
27 26 adantl ${⊢}\left({\phi }\wedge \left({x}\in ℝ\wedge {y}\in ℝ\right)\right)\to {x}{y}\in ℝ$
28 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
29 fss ${⊢}\left({T}:{A}⟶\left[0,\mathrm{+\infty }\right)\wedge \left[0,\mathrm{+\infty }\right)\subseteq ℝ\right)\to {T}:{A}⟶ℝ$
30 5 28 29 sylancl ${⊢}{\phi }\to {T}:{A}⟶ℝ$
31 6 1 fssd ${⊢}{\phi }\to {X}:{A}⟶ℝ$
32 inidm ${⊢}{A}\cap {A}={A}$
33 27 30 31 4 4 32 off ${⊢}{\phi }\to \left({T}{×}_{f}{X}\right):{A}⟶ℝ$
34 33 20 fssresd ${⊢}{\phi }\to \left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right):{B}⟶ℝ$
35 c0ex ${⊢}0\in \mathrm{V}$
36 35 a1i ${⊢}{\phi }\to 0\in \mathrm{V}$
37 34 21 36 fdmfifsupp ${⊢}{\phi }\to {finSupp}_{0}\left(\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)\right)$
38 16 19 21 25 34 37 gsumsubgcl ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)\in ℝ$
39 38 recnd ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)\in ℂ$
40 ax-resscn ${⊢}ℝ\subseteq ℂ$
41 28 40 sstri ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℂ$
42 10 unssbd ${⊢}{\phi }\to \left\{{z}\right\}\subseteq {A}$
43 vex ${⊢}{z}\in \mathrm{V}$
44 43 snss ${⊢}{z}\in {A}↔\left\{{z}\right\}\subseteq {A}$
45 42 44 sylibr ${⊢}{\phi }\to {z}\in {A}$
46 5 45 ffvelrnd ${⊢}{\phi }\to {T}\left({z}\right)\in \left[0,\mathrm{+\infty }\right)$
47 41 46 sseldi ${⊢}{\phi }\to {T}\left({z}\right)\in ℂ$
48 6 45 ffvelrnd ${⊢}{\phi }\to {X}\left({z}\right)\in {D}$
49 1 48 sseldd ${⊢}{\phi }\to {X}\left({z}\right)\in ℝ$
50 49 recnd ${⊢}{\phi }\to {X}\left({z}\right)\in ℂ$
51 47 50 mulcld ${⊢}{\phi }\to {T}\left({z}\right){X}\left({z}\right)\in ℂ$
52 1 2 3 4 5 6 7 8 9 10 11 12 jensenlem1 ${⊢}{\phi }\to {L}={S}+{T}\left({z}\right)$
53 13 rpred ${⊢}{\phi }\to {S}\in ℝ$
54 elrege0 ${⊢}{T}\left({z}\right)\in \left[0,\mathrm{+\infty }\right)↔\left({T}\left({z}\right)\in ℝ\wedge 0\le {T}\left({z}\right)\right)$
55 54 simplbi ${⊢}{T}\left({z}\right)\in \left[0,\mathrm{+\infty }\right)\to {T}\left({z}\right)\in ℝ$
56 46 55 syl ${⊢}{\phi }\to {T}\left({z}\right)\in ℝ$
57 53 56 readdcld ${⊢}{\phi }\to {S}+{T}\left({z}\right)\in ℝ$
58 52 57 eqeltrd ${⊢}{\phi }\to {L}\in ℝ$
59 58 recnd ${⊢}{\phi }\to {L}\in ℂ$
60 0red ${⊢}{\phi }\to 0\in ℝ$
61 13 rpgt0d ${⊢}{\phi }\to 0<{S}$
62 54 simprbi ${⊢}{T}\left({z}\right)\in \left[0,\mathrm{+\infty }\right)\to 0\le {T}\left({z}\right)$
63 46 62 syl ${⊢}{\phi }\to 0\le {T}\left({z}\right)$
64 53 56 addge01d ${⊢}{\phi }\to \left(0\le {T}\left({z}\right)↔{S}\le {S}+{T}\left({z}\right)\right)$
65 63 64 mpbid ${⊢}{\phi }\to {S}\le {S}+{T}\left({z}\right)$
66 65 52 breqtrrd ${⊢}{\phi }\to {S}\le {L}$
67 60 53 58 61 66 ltletrd ${⊢}{\phi }\to 0<{L}$
68 67 gt0ne0d ${⊢}{\phi }\to {L}\ne 0$
69 39 51 59 68 divdird ${⊢}{\phi }\to \frac{\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)\right)+{T}\left({z}\right){X}\left({z}\right)}{{L}}=\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{L}}\right)+\left(\frac{{T}\left({z}\right){X}\left({z}\right)}{{L}}\right)$
70 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
71 cnfldadd ${⊢}+={+}_{{ℂ}_{\mathrm{fld}}}$
72 ringcmn ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
73 17 72 mp1i ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
74 20 sselda ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\in {A}$
75 5 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {T}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
76 74 75 syldan ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {T}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
77 41 76 sseldi ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {T}\left({x}\right)\in ℂ$
78 1 adantr ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {D}\subseteq ℝ$
79 6 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {X}\left({x}\right)\in {D}$
80 74 79 syldan ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {X}\left({x}\right)\in {D}$
81 78 80 sseldd ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {X}\left({x}\right)\in ℝ$
82 81 recnd ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {X}\left({x}\right)\in ℂ$
83 77 82 mulcld ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {T}\left({x}\right){X}\left({x}\right)\in ℂ$
84 fveq2 ${⊢}{x}={z}\to {T}\left({x}\right)={T}\left({z}\right)$
85 fveq2 ${⊢}{x}={z}\to {X}\left({x}\right)={X}\left({z}\right)$
86 84 85 oveq12d ${⊢}{x}={z}\to {T}\left({x}\right){X}\left({x}\right)={T}\left({z}\right){X}\left({z}\right)$
87 70 71 73 21 83 45 9 51 86 gsumunsn ${⊢}{\phi }\to \underset{{x}\in {B}\cup \left\{{z}\right\}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right){X}\left({x}\right)=\left(\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}},{T}\left({x}\right){X}\left({x}\right)\right)+{T}\left({z}\right){X}\left({z}\right)$
88 5 feqmptd ${⊢}{\phi }\to {T}=\left({x}\in {A}⟼{T}\left({x}\right)\right)$
89 6 feqmptd ${⊢}{\phi }\to {X}=\left({x}\in {A}⟼{X}\left({x}\right)\right)$
90 4 75 79 88 89 offval2 ${⊢}{\phi }\to {T}{×}_{f}{X}=\left({x}\in {A}⟼{T}\left({x}\right){X}\left({x}\right)\right)$
91 90 reseq1d ${⊢}{\phi }\to {\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}={\left({x}\in {A}⟼{T}\left({x}\right){X}\left({x}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}$
92 10 resmptd ${⊢}{\phi }\to {\left({x}\in {A}⟼{T}\left({x}\right){X}\left({x}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}=\left({x}\in \left({B}\cup \left\{{z}\right\}\right)⟼{T}\left({x}\right){X}\left({x}\right)\right)$
93 91 92 eqtrd ${⊢}{\phi }\to {\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}=\left({x}\in \left({B}\cup \left\{{z}\right\}\right)⟼{T}\left({x}\right){X}\left({x}\right)\right)$
94 93 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)=\underset{{x}\in {B}\cup \left\{{z}\right\}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right){X}\left({x}\right)$
95 90 reseq1d ${⊢}{\phi }\to {\left({T}{×}_{f}{X}\right)↾}_{{B}}={\left({x}\in {A}⟼{T}\left({x}\right){X}\left({x}\right)\right)↾}_{{B}}$
96 20 resmptd ${⊢}{\phi }\to {\left({x}\in {A}⟼{T}\left({x}\right){X}\left({x}\right)\right)↾}_{{B}}=\left({x}\in {B}⟼{T}\left({x}\right){X}\left({x}\right)\right)$
97 95 96 eqtrd ${⊢}{\phi }\to {\left({T}{×}_{f}{X}\right)↾}_{{B}}=\left({x}\in {B}⟼{T}\left({x}\right){X}\left({x}\right)\right)$
98 97 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)=\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right){X}\left({x}\right)$
99 98 oveq1d ${⊢}{\phi }\to \left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)\right)+{T}\left({z}\right){X}\left({z}\right)=\left(\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}},{T}\left({x}\right){X}\left({x}\right)\right)+{T}\left({z}\right){X}\left({z}\right)$
100 87 94 99 3eqtr4d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)\right)+{T}\left({z}\right){X}\left({z}\right)$
101 100 oveq1d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}=\frac{\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)\right)+{T}\left({z}\right){X}\left({z}\right)}{{L}}$
102 53 recnd ${⊢}{\phi }\to {S}\in ℂ$
103 13 rpne0d ${⊢}{\phi }\to {S}\ne 0$
104 39 102 59 103 68 dmdcand ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{L}}$
105 59 102 59 68 divsubdird ${⊢}{\phi }\to \frac{{L}-{S}}{{L}}=\left(\frac{{L}}{{L}}\right)-\left(\frac{{S}}{{L}}\right)$
106 102 47 52 mvrladdd ${⊢}{\phi }\to {L}-{S}={T}\left({z}\right)$
107 106 oveq1d ${⊢}{\phi }\to \frac{{L}-{S}}{{L}}=\frac{{T}\left({z}\right)}{{L}}$
108 59 68 dividd ${⊢}{\phi }\to \frac{{L}}{{L}}=1$
109 108 oveq1d ${⊢}{\phi }\to \left(\frac{{L}}{{L}}\right)-\left(\frac{{S}}{{L}}\right)=1-\left(\frac{{S}}{{L}}\right)$
110 105 107 109 3eqtr3rd ${⊢}{\phi }\to 1-\left(\frac{{S}}{{L}}\right)=\frac{{T}\left({z}\right)}{{L}}$
111 110 oveq1d ${⊢}{\phi }\to \left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)=\left(\frac{{T}\left({z}\right)}{{L}}\right){X}\left({z}\right)$
112 47 50 59 68 div23d ${⊢}{\phi }\to \frac{{T}\left({z}\right){X}\left({z}\right)}{{L}}=\left(\frac{{T}\left({z}\right)}{{L}}\right){X}\left({z}\right)$
113 111 112 eqtr4d ${⊢}{\phi }\to \left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)=\frac{{T}\left({z}\right){X}\left({z}\right)}{{L}}$
114 104 113 oveq12d ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)=\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{L}}\right)+\left(\frac{{T}\left({z}\right){X}\left({z}\right)}{{L}}\right)$
115 69 101 114 3eqtr4d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}=\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)$
116 53 58 68 redivcld ${⊢}{\phi }\to \frac{{S}}{{L}}\in ℝ$
117 13 rpge0d ${⊢}{\phi }\to 0\le {S}$
118 divge0 ${⊢}\left(\left({S}\in ℝ\wedge 0\le {S}\right)\wedge \left({L}\in ℝ\wedge 0<{L}\right)\right)\to 0\le \frac{{S}}{{L}}$
119 53 117 58 67 118 syl22anc ${⊢}{\phi }\to 0\le \frac{{S}}{{L}}$
120 59 mulid1d ${⊢}{\phi }\to {L}\cdot 1={L}$
121 66 120 breqtrrd ${⊢}{\phi }\to {S}\le {L}\cdot 1$
122 1red ${⊢}{\phi }\to 1\in ℝ$
123 ledivmul ${⊢}\left({S}\in ℝ\wedge 1\in ℝ\wedge \left({L}\in ℝ\wedge 0<{L}\right)\right)\to \left(\frac{{S}}{{L}}\le 1↔{S}\le {L}\cdot 1\right)$
124 53 122 58 67 123 syl112anc ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\le 1↔{S}\le {L}\cdot 1\right)$
125 121 124 mpbird ${⊢}{\phi }\to \frac{{S}}{{L}}\le 1$
126 elicc01 ${⊢}\frac{{S}}{{L}}\in \left[0,1\right]↔\left(\frac{{S}}{{L}}\in ℝ\wedge 0\le \frac{{S}}{{L}}\wedge \frac{{S}}{{L}}\le 1\right)$
127 116 119 125 126 syl3anbrc ${⊢}{\phi }\to \frac{{S}}{{L}}\in \left[0,1\right]$
128 14 48 127 3jca ${⊢}{\phi }\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\in {D}\wedge {X}\left({z}\right)\in {D}\wedge \frac{{S}}{{L}}\in \left[0,1\right]\right)$
129 1 3 cvxcl ${⊢}\left({\phi }\wedge \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\in {D}\wedge {X}\left({z}\right)\in {D}\wedge \frac{{S}}{{L}}\in \left[0,1\right]\right)\right)\to \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\in {D}$
130 128 129 mpdan ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\in {D}$
131 115 130 eqeltrd ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\in {D}$
132 2 130 ffvelrnd ${⊢}{\phi }\to {F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)\in ℝ$
133 2 14 ffvelrnd ${⊢}{\phi }\to {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\in ℝ$
134 116 133 remulcld ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\in ℝ$
135 2 48 ffvelrnd ${⊢}{\phi }\to {F}\left({X}\left({z}\right)\right)\in ℝ$
136 56 135 remulcld ${⊢}{\phi }\to {T}\left({z}\right){F}\left({X}\left({z}\right)\right)\in ℝ$
137 136 58 68 redivcld ${⊢}{\phi }\to \frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}\in ℝ$
138 134 137 readdcld ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(\frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}\right)\in ℝ$
139 fco ${⊢}\left({F}:{D}⟶ℝ\wedge {X}:{A}⟶{D}\right)\to \left({F}\circ {X}\right):{A}⟶ℝ$
140 2 6 139 syl2anc ${⊢}{\phi }\to \left({F}\circ {X}\right):{A}⟶ℝ$
141 27 30 140 4 4 32 off ${⊢}{\phi }\to \left({T}{×}_{f}\left({F}\circ {X}\right)\right):{A}⟶ℝ$
142 141 20 fssresd ${⊢}{\phi }\to \left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right):{B}⟶ℝ$
143 142 21 36 fdmfifsupp ${⊢}{\phi }\to {finSupp}_{0}\left(\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)\right)$
144 16 19 21 25 142 143 gsumsubgcl ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)\in ℝ$
145 144 53 103 redivcld ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\in ℝ$
146 116 145 remulcld ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)\in ℝ$
147 1re ${⊢}1\in ℝ$
148 resubcl ${⊢}\left(1\in ℝ\wedge \frac{{S}}{{L}}\in ℝ\right)\to 1-\left(\frac{{S}}{{L}}\right)\in ℝ$
149 147 116 148 sylancr ${⊢}{\phi }\to 1-\left(\frac{{S}}{{L}}\right)\in ℝ$
150 149 135 remulcld ${⊢}{\phi }\to \left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)\in ℝ$
151 146 150 readdcld ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)\in ℝ$
152 oveq2 ${⊢}{x}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\to {t}{x}={t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)$
153 152 fvoveq1d ${⊢}{x}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\to {F}\left({t}{x}+\left(1-{t}\right){y}\right)={F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){y}\right)$
154 fveq2 ${⊢}{x}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\to {F}\left({x}\right)={F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)$
155 154 oveq2d ${⊢}{x}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\to {t}{F}\left({x}\right)={t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)$
156 155 oveq1d ${⊢}{x}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\to {t}{F}\left({x}\right)+\left(1-{t}\right){F}\left({y}\right)={t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({y}\right)$
157 153 156 breq12d ${⊢}{x}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\to \left({F}\left({t}{x}+\left(1-{t}\right){y}\right)\le {t}{F}\left({x}\right)+\left(1-{t}\right){F}\left({y}\right)↔{F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){y}\right)\le {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({y}\right)\right)$
158 157 imbi2d ${⊢}{x}=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\to \left(\left({\phi }\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)\right)↔\left({\phi }\to {F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){y}\right)\le {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({y}\right)\right)\right)$
159 oveq2 ${⊢}{y}={X}\left({z}\right)\to \left(1-{t}\right){y}=\left(1-{t}\right){X}\left({z}\right)$
160 159 oveq2d ${⊢}{y}={X}\left({z}\right)\to {t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){y}={t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){X}\left({z}\right)$
161 160 fveq2d ${⊢}{y}={X}\left({z}\right)\to {F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){y}\right)={F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){X}\left({z}\right)\right)$
162 fveq2 ${⊢}{y}={X}\left({z}\right)\to {F}\left({y}\right)={F}\left({X}\left({z}\right)\right)$
163 162 oveq2d ${⊢}{y}={X}\left({z}\right)\to \left(1-{t}\right){F}\left({y}\right)=\left(1-{t}\right){F}\left({X}\left({z}\right)\right)$
164 163 oveq2d ${⊢}{y}={X}\left({z}\right)\to {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({y}\right)={t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({X}\left({z}\right)\right)$
165 161 164 breq12d ${⊢}{y}={X}\left({z}\right)\to \left({F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){y}\right)\le {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({y}\right)↔{F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){X}\left({z}\right)\right)\le {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({X}\left({z}\right)\right)\right)$
166 165 imbi2d ${⊢}{y}={X}\left({z}\right)\to \left(\left({\phi }\to {F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){y}\right)\le {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({y}\right)\right)↔\left({\phi }\to {F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){X}\left({z}\right)\right)\le {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({X}\left({z}\right)\right)\right)\right)$
167 oveq1 ${⊢}{t}=\frac{{S}}{{L}}\to {t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)=\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)$
168 oveq2 ${⊢}{t}=\frac{{S}}{{L}}\to 1-{t}=1-\left(\frac{{S}}{{L}}\right)$
169 168 oveq1d ${⊢}{t}=\frac{{S}}{{L}}\to \left(1-{t}\right){X}\left({z}\right)=\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)$
170 167 169 oveq12d ${⊢}{t}=\frac{{S}}{{L}}\to {t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){X}\left({z}\right)=\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)$
171 170 fveq2d ${⊢}{t}=\frac{{S}}{{L}}\to {F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){X}\left({z}\right)\right)={F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)$
172 oveq1 ${⊢}{t}=\frac{{S}}{{L}}\to {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)=\left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)$
173 168 oveq1d ${⊢}{t}=\frac{{S}}{{L}}\to \left(1-{t}\right){F}\left({X}\left({z}\right)\right)=\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
174 172 173 oveq12d ${⊢}{t}=\frac{{S}}{{L}}\to {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({X}\left({z}\right)\right)=\left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
175 171 174 breq12d ${⊢}{t}=\frac{{S}}{{L}}\to \left({F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){X}\left({z}\right)\right)\le {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({X}\left({z}\right)\right)↔{F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)\le \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)\right)$
176 175 imbi2d ${⊢}{t}=\frac{{S}}{{L}}\to \left(\left({\phi }\to {F}\left({t}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){X}\left({z}\right)\right)\le {t}{F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-{t}\right){F}\left({X}\left({z}\right)\right)\right)↔\left({\phi }\to {F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)\le \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)\right)\right)$
177 8 expcom ${⊢}\left({x}\in {D}\wedge {y}\in {D}\wedge {t}\in \left[0,1\right]\right)\to \left({\phi }\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)\right)$
178 158 166 176 177 vtocl3ga ${⊢}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\in {D}\wedge {X}\left({z}\right)\in {D}\wedge \frac{{S}}{{L}}\in \left[0,1\right]\right)\to \left({\phi }\to {F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)\le \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)\right)$
179 14 48 127 178 syl3anc ${⊢}{\phi }\to \left({\phi }\to {F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)\le \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)\right)$
180 179 pm2.43i ${⊢}{\phi }\to {F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)\le \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
181 110 oveq1d ${⊢}{\phi }\to \left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)=\left(\frac{{T}\left({z}\right)}{{L}}\right){F}\left({X}\left({z}\right)\right)$
182 135 recnd ${⊢}{\phi }\to {F}\left({X}\left({z}\right)\right)\in ℂ$
183 47 182 59 68 div23d ${⊢}{\phi }\to \frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}=\left(\frac{{T}\left({z}\right)}{{L}}\right){F}\left({X}\left({z}\right)\right)$
184 181 183 eqtr4d ${⊢}{\phi }\to \left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)=\frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}$
185 184 oveq2d ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)=\left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(\frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}\right)$
186 180 185 breqtrd ${⊢}{\phi }\to {F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)\le \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(\frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}\right)$
187 183 181 eqtr4d ${⊢}{\phi }\to \frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}=\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
188 187 oveq2d ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(\frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}\right)=\left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
189 53 58 61 67 divgt0d ${⊢}{\phi }\to 0<\frac{{S}}{{L}}$
190 lemul2 ${⊢}\left({F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\in ℝ\wedge \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\in ℝ\wedge \left(\frac{{S}}{{L}}\in ℝ\wedge 0<\frac{{S}}{{L}}\right)\right)\to \left({F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}↔\left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\le \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)\right)$
191 133 145 116 189 190 syl112anc ${⊢}{\phi }\to \left({F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}↔\left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\le \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)\right)$
192 15 191 mpbid ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)\le \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)$
193 134 146 150 192 leadd1dd ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)\le \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
194 188 193 eqbrtrd ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right){F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(\frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}\right)\le \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
195 132 138 151 186 194 letrd ${⊢}{\phi }\to {F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)\le \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
196 115 fveq2d ${⊢}{\phi }\to {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\right)={F}\left(\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){X}\left({z}\right)\right)$
197 144 recnd ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)\in ℂ$
198 136 recnd ${⊢}{\phi }\to {T}\left({z}\right){F}\left({X}\left({z}\right)\right)\in ℂ$
199 197 198 59 68 divdird ${⊢}{\phi }\to \frac{\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)\right)+{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}=\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{L}}\right)+\left(\frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}\right)$
200 28 75 sseldi ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {T}\left({x}\right)\in ℝ$
201 2 ffvelrnda ${⊢}\left({\phi }\wedge {X}\left({x}\right)\in {D}\right)\to {F}\left({X}\left({x}\right)\right)\in ℝ$
202 79 201 syldan ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({X}\left({x}\right)\right)\in ℝ$
203 200 202 remulcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {T}\left({x}\right){F}\left({X}\left({x}\right)\right)\in ℝ$
204 203 recnd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {T}\left({x}\right){F}\left({X}\left({x}\right)\right)\in ℂ$
205 74 204 syldan ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {T}\left({x}\right){F}\left({X}\left({x}\right)\right)\in ℂ$
206 85 fveq2d ${⊢}{x}={z}\to {F}\left({X}\left({x}\right)\right)={F}\left({X}\left({z}\right)\right)$
207 84 206 oveq12d ${⊢}{x}={z}\to {T}\left({x}\right){F}\left({X}\left({x}\right)\right)={T}\left({z}\right){F}\left({X}\left({z}\right)\right)$
208 70 71 73 21 205 45 9 198 207 gsumunsn ${⊢}{\phi }\to \underset{{x}\in {B}\cup \left\{{z}\right\}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right){F}\left({X}\left({x}\right)\right)=\left(\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}},{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)+{T}\left({z}\right){F}\left({X}\left({z}\right)\right)$
209 2 feqmptd ${⊢}{\phi }\to {F}=\left({y}\in {D}⟼{F}\left({y}\right)\right)$
210 fveq2 ${⊢}{y}={X}\left({x}\right)\to {F}\left({y}\right)={F}\left({X}\left({x}\right)\right)$
211 79 89 209 210 fmptco ${⊢}{\phi }\to {F}\circ {X}=\left({x}\in {A}⟼{F}\left({X}\left({x}\right)\right)\right)$
212 4 75 202 88 211 offval2 ${⊢}{\phi }\to {T}{×}_{f}\left({F}\circ {X}\right)=\left({x}\in {A}⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)$
213 212 reseq1d ${⊢}{\phi }\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}={\left({x}\in {A}⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}$
214 10 resmptd ${⊢}{\phi }\to {\left({x}\in {A}⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}=\left({x}\in \left({B}\cup \left\{{z}\right\}\right)⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)$
215 213 214 eqtrd ${⊢}{\phi }\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}=\left({x}\in \left({B}\cup \left\{{z}\right\}\right)⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)$
216 215 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)=\underset{{x}\in {B}\cup \left\{{z}\right\}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right){F}\left({X}\left({x}\right)\right)$
217 212 reseq1d ${⊢}{\phi }\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}={\left({x}\in {A}⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)↾}_{{B}}$
218 20 resmptd ${⊢}{\phi }\to {\left({x}\in {A}⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)↾}_{{B}}=\left({x}\in {B}⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)$
219 217 218 eqtrd ${⊢}{\phi }\to {\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}=\left({x}\in {B}⟼{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)$
220 219 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)=\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right){F}\left({X}\left({x}\right)\right)$
221 220 oveq1d ${⊢}{\phi }\to \left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)\right)+{T}\left({z}\right){F}\left({X}\left({z}\right)\right)=\left(\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}},{T}\left({x}\right){F}\left({X}\left({x}\right)\right)\right)+{T}\left({z}\right){F}\left({X}\left({z}\right)\right)$
222 208 216 221 3eqtr4d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)\right)+{T}\left({z}\right){F}\left({X}\left({z}\right)\right)$
223 222 oveq1d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}=\frac{\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)\right)+{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}$
224 197 102 59 103 68 dmdcand ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)=\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{L}}$
225 224 184 oveq12d ${⊢}{\phi }\to \left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)=\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{L}}\right)+\left(\frac{{T}\left({z}\right){F}\left({X}\left({z}\right)\right)}{{L}}\right)$
226 199 223 225 3eqtr4d ${⊢}{\phi }\to \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}=\left(\frac{{S}}{{L}}\right)\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{{B}}\right)}{{S}}\right)+\left(1-\left(\frac{{S}}{{L}}\right)\right){F}\left({X}\left({z}\right)\right)$
227 195 196 226 3brtr4d ${⊢}{\phi }\to {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}$
228 131 227 jca ${⊢}{\phi }\to \left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\in {D}\wedge {F}\left(\frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}{X}\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\right)\le \frac{{\sum }_{{ℂ}_{\mathrm{fld}}}\left({\left({T}{×}_{f}\left({F}\circ {X}\right)\right)↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)}{{L}}\right)$