Theorem jensenlem2

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

	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 ( 𝑇 ↾ ( 𝐵 ∪ { 𝑧 } ) ) )
	jensenlem.3	⊢ ( 𝜑 → 𝑆 ∈ ℝ+ )
	jensenlem.4	⊢ ( 𝜑 → ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐵 ) ) / 𝑆 ) ∈ 𝐷 )
	jensenlem.5	⊢ ( 𝜑 → ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐵 ) ) / 𝑆 ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ 𝐵 ) ) / 𝑆 ) )
Assertion	jensenlem2	⊢ ( 𝜑 → ( ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝐵 ∪ { 𝑧 } ) ) ) / 𝐿 ) ∈ 𝐷 ∧ ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ ( 𝐵 ∪ { 𝑧 } ) ) ) / 𝐿 ) ) ≤ ( ( ℂfld Σg ( ( 𝑇 ∘f · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝐵 ∪ { 𝑧 } ) ) ) / 𝐿 ) ) )

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