Metamath Proof Explorer

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 ffvelrnd ⊢ ( 𝜑 → ( 𝑇 ‘ 𝑧 ) ∈ ( 0 [,) +∞ ) )
47 41 46 sselid ⊢ ( 𝜑 → ( 𝑇 ‘ 𝑧 ) ∈ ℂ )
48 6 45 ffvelrnd ⊢ ( 𝜑 → ( 𝑋 ‘ 𝑧 ) ∈ 𝐷 )
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 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑇 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
76 74 75 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
77 41 76 sselid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑥 ) ∈ ℂ )
78 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ⊆ ℝ )
79 6 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑋 ‘ 𝑥 ) ∈ 𝐷 )
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 mulid1d ⊢ ( 𝜑 → ( 𝐿 · 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 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( ( 𝑆 / 𝐿 ) · ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐵 ) ) / 𝑆 ) ) + ( ( 1 − ( 𝑆 / 𝐿 ) ) · ( 𝑋 ‘ 𝑧 ) ) ) ) ∈ ℝ )
133 2 14 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐵 ) ) / 𝑆 ) ) ∈ ℝ )
134 116 133 remulcld ⊢ ( 𝜑 → ( ( 𝑆 / 𝐿 ) · ( 𝐹 ‘ ( ( ℂfld Σg ( ( 𝑇 ∘f · 𝑋 ) ↾ 𝐵 ) ) / 𝑆 ) ) ) ∈ ℝ )
135 2 48 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 ‘ 𝑧 ) ) ∈ ℝ )
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 ffvelrnda ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝑥 ) ∈ 𝐷 ) → ( 𝐹 ‘ ( 𝑋 ‘ 𝑥 ) ) ∈ ℝ )
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 · ( 𝐹 ∘ 𝑋 ) ) ↾ ( 𝐵 ∪ { 𝑧 } ) ) ) / 𝐿 ) ) )