Theorem jensenlem2

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

	Ref	Expression
Hypotheses	jensen.1	|- ( ph -> D C_ RR )
	jensen.2	|- ( ph -> F : D --> RR )
	jensen.3	|- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )
	jensen.4	|- ( ph -> A e. Fin )
	jensen.5	|- ( ph -> T : A --> ( 0 [,) +oo ) )
	jensen.6	|- ( ph -> X : A --> D )
	jensen.7	|- ( ph -> 0 < ( CCfld gsum T ) )
	jensen.8	|- ( ( ph /\ ( x e. D /\ y e. D /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) )
	jensenlem.1	|- ( ph -> -. z e. B )
	jensenlem.2	|- ( ph -> ( B u. { z } ) C_ A )
	jensenlem.s	|- S = ( CCfld gsum ( T |` B ) )
	jensenlem.l	|- L = ( CCfld gsum ( T |` ( B u. { z } ) ) )
	jensenlem.3	|- ( ph -> S e. RR+ )
	jensenlem.4	|- ( ph -> ( ( CCfld gsum ( ( T oF x. X ) |` B ) ) / S ) e. D )
	jensenlem.5	|- ( ph -> ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` B ) ) / S ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` B ) ) / S ) )
Assertion	jensenlem2	|- ( ph -> ( ( ( CCfld gsum ( ( T oF x. X ) |` ( B u. { z } ) ) ) / L ) e. D /\ ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` ( B u. { z } ) ) ) / L ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( B u. { z } ) ) ) / L ) ) )

Proof

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