# Metamath Proof Explorer

## Theorem jensenlem1

Description: Lemma for jensen . (Contributed by Mario Carneiro, 4-Jun-2016)

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)$
Assertion jensenlem1 ${⊢}{\phi }\to {L}={S}+{T}\left({z}\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 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
14 cnfldadd ${⊢}+={+}_{{ℂ}_{\mathrm{fld}}}$
15 cnring ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}$
16 ringcmn ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{Ring}\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
17 15 16 mp1i ${⊢}{\phi }\to {ℂ}_{\mathrm{fld}}\in \mathrm{CMnd}$
18 10 unssad ${⊢}{\phi }\to {B}\subseteq {A}$
19 4 18 ssfid ${⊢}{\phi }\to {B}\in \mathrm{Fin}$
20 rge0ssre ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℝ$
21 ax-resscn ${⊢}ℝ\subseteq ℂ$
22 20 21 sstri ${⊢}\left[0,\mathrm{+\infty }\right)\subseteq ℂ$
23 18 sselda ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {x}\in {A}$
24 5 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {T}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
25 23 24 syldan ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {T}\left({x}\right)\in \left[0,\mathrm{+\infty }\right)$
26 22 25 sseldi ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {T}\left({x}\right)\in ℂ$
27 10 unssbd ${⊢}{\phi }\to \left\{{z}\right\}\subseteq {A}$
28 vex ${⊢}{z}\in \mathrm{V}$
29 28 snss ${⊢}{z}\in {A}↔\left\{{z}\right\}\subseteq {A}$
30 27 29 sylibr ${⊢}{\phi }\to {z}\in {A}$
31 5 30 ffvelrnd ${⊢}{\phi }\to {T}\left({z}\right)\in \left[0,\mathrm{+\infty }\right)$
32 22 31 sseldi ${⊢}{\phi }\to {T}\left({z}\right)\in ℂ$
33 fveq2 ${⊢}{x}={z}\to {T}\left({x}\right)={T}\left({z}\right)$
34 13 14 17 19 26 30 9 32 33 gsumunsn ${⊢}{\phi }\to \underset{{x}\in {B}\cup \left\{{z}\right\}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right)=\left(\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}},{T}\left({x}\right)\right)+{T}\left({z}\right)$
35 5 10 feqresmpt ${⊢}{\phi }\to {{T}↾}_{\left({B}\cup \left\{{z}\right\}\right)}=\left({x}\in \left({B}\cup \left\{{z}\right\}\right)⟼{T}\left({x}\right)\right)$
36 35 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)=\underset{{x}\in {B}\cup \left\{{z}\right\}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right)$
37 5 18 feqresmpt ${⊢}{\phi }\to {{T}↾}_{{B}}=\left({x}\in {B}⟼{T}\left({x}\right)\right)$
38 37 oveq2d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{{B}}\right)=\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}}{T}\left({x}\right)$
39 38 oveq1d ${⊢}{\phi }\to \left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({{T}↾}_{{B}}\right)\right)+{T}\left({z}\right)=\left(\underset{{x}\in {B}}{{\sum }_{{ℂ}_{\mathrm{fld}}}},{T}\left({x}\right)\right)+{T}\left({z}\right)$
40 34 36 39 3eqtr4d ${⊢}{\phi }\to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({{T}↾}_{\left({B}\cup \left\{{z}\right\}\right)}\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({{T}↾}_{{B}}\right)\right)+{T}\left({z}\right)$
41 11 oveq1i ${⊢}{S}+{T}\left({z}\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({{T}↾}_{{B}}\right)\right)+{T}\left({z}\right)$
42 40 12 41 3eqtr4g ${⊢}{\phi }\to {L}={S}+{T}\left({z}\right)$