Theorem jensenlem1

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

	Ref	Expression
Hypotheses	jensen.1	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
	jensen.2	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
	jensen.3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ 𝐷 )
	jensen.4	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	jensen.5	⊢ ( 𝜑 → 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) )
	jensen.6	⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐷 )
	jensen.7	⊢ ( 𝜑 → 0 < ( ℂfld Σg 𝑇 ) )
	jensen.8	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ≤ ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
	jensenlem.1	⊢ ( 𝜑 → ¬ 𝑧 ∈ 𝐵 )
	jensenlem.2	⊢ ( 𝜑 → ( 𝐵 ∪ { 𝑧 } ) ⊆ 𝐴 )
	jensenlem.s	⊢ 𝑆 = ( ℂfld Σg ( 𝑇 ↾ 𝐵 ) )
	jensenlem.l	⊢ 𝐿 = ( ℂfld Σg ( 𝑇 ↾ ( 𝐵 ∪ { 𝑧 } ) ) )
Assertion	jensenlem1	⊢ ( 𝜑 → 𝐿 = ( 𝑆 + ( 𝑇 ‘ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		jensen.1	⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
2		jensen.2	⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℝ )
3		jensen.3	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐷 ∧ 𝑏 ∈ 𝐷 ) ) → ( 𝑎 [,] 𝑏 ) ⊆ 𝐷 )
4		jensen.4	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		jensen.5	⊢ ( 𝜑 → 𝑇 : 𝐴 ⟶ ( 0 [,) +∞ ) )
6		jensen.6	⊢ ( 𝜑 → 𝑋 : 𝐴 ⟶ 𝐷 )
7		jensen.7	⊢ ( 𝜑 → 0 < ( ℂfld Σg 𝑇 ) )
8		jensen.8	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ≤ ( ( 𝑡 · ( 𝐹 ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( 𝐹 ‘ 𝑦 ) ) ) )
9		jensenlem.1	⊢ ( 𝜑 → ¬ 𝑧 ∈ 𝐵 )
10		jensenlem.2	⊢ ( 𝜑 → ( 𝐵 ∪ { 𝑧 } ) ⊆ 𝐴 )
11		jensenlem.s	⊢ 𝑆 = ( ℂfld Σg ( 𝑇 ↾ 𝐵 ) )
12		jensenlem.l	⊢ 𝐿 = ( ℂfld Σg ( 𝑇 ↾ ( 𝐵 ∪ { 𝑧 } ) ) )
13		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
14		cnfldadd	⊢ + = ( +g ‘ ℂfld )
15		cnring	⊢ ℂfld ∈ Ring
16		ringcmn	⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
17	15 16	mp1i	⊢ ( 𝜑 → ℂfld ∈ CMnd )
18	10	unssad	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
19	4 18	ssfid	⊢ ( 𝜑 → 𝐵 ∈ Fin )
20		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
21		ax-resscn	⊢ ℝ ⊆ ℂ
22	20 21	sstri	⊢ ( 0 [,) +∞ ) ⊆ ℂ
23	18	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
24	5	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
25	23 24	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
26	22 25	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑥 ) ∈ ℂ )
27	10	unssbd	⊢ ( 𝜑 → { 𝑧 } ⊆ 𝐴 )
28		vex	⊢ 𝑧 ∈ V
29	28	snss	⊢ ( 𝑧 ∈ 𝐴 ↔ { 𝑧 } ⊆ 𝐴 )
30	27 29	sylibr	⊢ ( 𝜑 → 𝑧 ∈ 𝐴 )
31	5 30	ffvelrnd	⊢ ( 𝜑 → ( 𝑇 ‘ 𝑧 ) ∈ ( 0 [,) +∞ ) )
32	22 31	sseldi	⊢ ( 𝜑 → ( 𝑇 ‘ 𝑧 ) ∈ ℂ )
33		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑧 ) )
34	13 14 17 19 26 30 9 32 33	gsumunsn	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑥 ∈ ( 𝐵 ∪ { 𝑧 } ) ↦ ( 𝑇 ‘ 𝑥 ) ) ) = ( ( ℂfld Σg ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 ‘ 𝑥 ) ) ) + ( 𝑇 ‘ 𝑧 ) ) )
35	5 10	feqresmpt	⊢ ( 𝜑 → ( 𝑇 ↾ ( 𝐵 ∪ { 𝑧 } ) ) = ( 𝑥 ∈ ( 𝐵 ∪ { 𝑧 } ) ↦ ( 𝑇 ‘ 𝑥 ) ) )
36	35	oveq2d	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑇 ↾ ( 𝐵 ∪ { 𝑧 } ) ) ) = ( ℂfld Σg ( 𝑥 ∈ ( 𝐵 ∪ { 𝑧 } ) ↦ ( 𝑇 ‘ 𝑥 ) ) ) )
37	5 18	feqresmpt	⊢ ( 𝜑 → ( 𝑇 ↾ 𝐵 ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 ‘ 𝑥 ) ) )
38	37	oveq2d	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑇 ↾ 𝐵 ) ) = ( ℂfld Σg ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 ‘ 𝑥 ) ) ) )
39	38	oveq1d	⊢ ( 𝜑 → ( ( ℂfld Σg ( 𝑇 ↾ 𝐵 ) ) + ( 𝑇 ‘ 𝑧 ) ) = ( ( ℂfld Σg ( 𝑥 ∈ 𝐵 ↦ ( 𝑇 ‘ 𝑥 ) ) ) + ( 𝑇 ‘ 𝑧 ) ) )
40	34 36 39	3eqtr4d	⊢ ( 𝜑 → ( ℂfld Σg ( 𝑇 ↾ ( 𝐵 ∪ { 𝑧 } ) ) ) = ( ( ℂfld Σg ( 𝑇 ↾ 𝐵 ) ) + ( 𝑇 ‘ 𝑧 ) ) )
41	11	oveq1i	⊢ ( 𝑆 + ( 𝑇 ‘ 𝑧 ) ) = ( ( ℂfld Σg ( 𝑇 ↾ 𝐵 ) ) + ( 𝑇 ‘ 𝑧 ) )
42	40 12 41	3eqtr4g	⊢ ( 𝜑 → 𝐿 = ( 𝑆 + ( 𝑇 ‘ 𝑧 ) ) )