jensenlem2

	Ref	Expression
Hypotheses	jensen.1	$⊢ φ \to D \subseteq ℝ$
	jensen.2	$⊢ φ \to F : D ⟶ ℝ$
	jensen.3	$⊢ (φ \land (a \in D \land b \in D)) \to [a, b] \subseteq D$
	jensen.4	$⊢ φ \to A \in Fin$
	jensen.5	$⊢ φ \to T : A ⟶ [0, +∞)$
	jensen.6	$⊢ φ \to X : A ⟶ D$
	jensen.7	$⊢ φ \to 0 < \sum_{ℂ_{fld}} T$
	jensen.8	$⊢ (φ \land (x \in D \land y \in D \land t \in [0, 1])) \to F (t x + (1 - t) y) \leq t F (x) + (1 - t) F (y)$
	jensenlem.1	$⊢ φ \to \neg z \in B$
	jensenlem.2	$⊢ φ \to B \cup \{z\} \subseteq A$
	jensenlem.s	$⊢ S = \sum_{ℂ_{fld}} ({T ↾}_{B})$
	jensenlem.l	$⊢ L = \sum_{ℂ_{fld}} ({T ↾}_{(B \cup \{z\})})$
	jensenlem.3	$⊢ φ \to S \in ℝ^{+}$
	jensenlem.4	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{B})}{S} \in D$
	jensenlem.5	$⊢ φ \to F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{B})}{S}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{B})}{S}$
Assertion	jensenlem2	$⊢ φ \to (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(B \cup \{z\})})}{L} \in D \land F (\frac{\sum_{ℂ_{fld}} ({(T \times_{f} X) ↾}_{(B \cup \{z\})})}{L}) \leq \frac{\sum_{ℂ_{fld}} ({(T \times_{f} (F \circ X)) ↾}_{(B \cup \{z\})})}{L})$

Proof

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

Metamath Proof Explorer

Theorem jensenlem2

Proof