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(tx+\left(1-t\right)y\right)\le tF\left(x\right)+\left(1-t\right)F\left(y\right)$$
	jensenlem.1	$$⊢\phi \to \neg z\in B$$
	jensenlem.2	$$⊢\phi \to B\cup \left\{z\right\}\subseteq A$$
	jensenlem.s	$$⊢S={\sum }_{{ℂ}_{\mathrm{fld}}}\left({T\upharpoonright }_B\right)$$
	jensenlem.l	$$⊢L={\sum }_{{ℂ}_{\mathrm{fld}}}\left({T\upharpoonright }_{\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(tx+\left(1-t\right)y\right)\le tF\left(x\right)+\left(1-t\right)F\left(y\right)$$
9		jensenlem.1	$$⊢\phi \to \neg z\in B$$
10		jensenlem.2	$$⊢\phi \to B\cup \left\{z\right\}\subseteq A$$
11		jensenlem.s	$$⊢S={\sum }_{{ℂ}_{\mathrm{fld}}}\left({T\upharpoonright }_B\right)$$
12		jensenlem.l	$$⊢L={\sum }_{{ℂ}_{\mathrm{fld}}}\left({T\upharpoonright }_{\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\leftrightarrow \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\upharpoonright }_{\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\upharpoonright }_{\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\upharpoonright }_B=\left(x\in B⟼T\left(x\right)\right)$$
38	37	oveq2d	$$⊢\phi \to {\sum }_{{ℂ}_{\mathrm{fld}}}\left({T\upharpoonright }_B\right)=\underset{x\in B}{{\sum }_{{ℂ}_{\mathrm{fld}}}}T\left(x\right)$$
39	38	oveq1d	$$⊢\phi \to \left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({T\upharpoonright }_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\upharpoonright }_{\left(B\cup \left\{z\right\}\right)}\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({T\upharpoonright }_B\right)\right)+T\left(z\right)$$
41	11	oveq1i	$$⊢S+T\left(z\right)=\left({\sum }_{{ℂ}_{\mathrm{fld}}},\left({T\upharpoonright }_B\right)\right)+T\left(z\right)$$
42	40 12 41	3eqtr4g	$$⊢\phi \to L=S+T\left(z\right)$$