Metamath Proof Explorer


Theorem amgmwlem

Description: Weighted version of amgmlem . (Contributed by Kunhao Zheng, 19-Jun-2021)

Ref Expression
Hypotheses amgmwlem.0 𝑀 = ( mulGrp ‘ ℂfld )
amgmwlem.1 ( 𝜑𝐴 ∈ Fin )
amgmwlem.2 ( 𝜑𝐴 ≠ ∅ )
amgmwlem.3 ( 𝜑𝐹 : 𝐴 ⟶ ℝ+ )
amgmwlem.4 ( 𝜑𝑊 : 𝐴 ⟶ ℝ+ )
amgmwlem.5 ( 𝜑 → ( ℂfld Σg 𝑊 ) = 1 )
Assertion amgmwlem ( 𝜑 → ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ≤ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 amgmwlem.0 𝑀 = ( mulGrp ‘ ℂfld )
2 amgmwlem.1 ( 𝜑𝐴 ∈ Fin )
3 amgmwlem.2 ( 𝜑𝐴 ≠ ∅ )
4 amgmwlem.3 ( 𝜑𝐹 : 𝐴 ⟶ ℝ+ )
5 amgmwlem.4 ( 𝜑𝑊 : 𝐴 ⟶ ℝ+ )
6 amgmwlem.5 ( 𝜑 → ( ℂfld Σg 𝑊 ) = 1 )
7 4 ffvelrnda ( ( 𝜑𝑘𝐴 ) → ( 𝐹𝑘 ) ∈ ℝ+ )
8 5 ffvelrnda ( ( 𝜑𝑘𝐴 ) → ( 𝑊𝑘 ) ∈ ℝ+ )
9 8 rpred ( ( 𝜑𝑘𝐴 ) → ( 𝑊𝑘 ) ∈ ℝ )
10 7 9 rpcxpcld ( ( 𝜑𝑘𝐴 ) → ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ∈ ℝ+ )
11 10 relogcld ( ( 𝜑𝑘𝐴 ) → ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ∈ ℝ )
12 11 recnd ( ( 𝜑𝑘𝐴 ) → ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ∈ ℂ )
13 2 12 gsumfsum ( 𝜑 → ( ℂfld Σg ( 𝑘𝐴 ↦ ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ) ) = Σ 𝑘𝐴 ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) )
14 12 negnegd ( ( 𝜑𝑘𝐴 ) → - - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) = ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) )
15 14 sumeq2dv ( 𝜑 → Σ 𝑘𝐴 - - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) = Σ 𝑘𝐴 ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) )
16 11 renegcld ( ( 𝜑𝑘𝐴 ) → - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ∈ ℝ )
17 16 recnd ( ( 𝜑𝑘𝐴 ) → - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ∈ ℂ )
18 2 17 fsumneg ( 𝜑 → Σ 𝑘𝐴 - - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) = - Σ 𝑘𝐴 - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) )
19 7 9 logcxpd ( ( 𝜑𝑘𝐴 ) → ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) = ( ( 𝑊𝑘 ) · ( log ‘ ( 𝐹𝑘 ) ) ) )
20 19 negeqd ( ( 𝜑𝑘𝐴 ) → - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) = - ( ( 𝑊𝑘 ) · ( log ‘ ( 𝐹𝑘 ) ) ) )
21 20 sumeq2dv ( 𝜑 → Σ 𝑘𝐴 - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) = Σ 𝑘𝐴 - ( ( 𝑊𝑘 ) · ( log ‘ ( 𝐹𝑘 ) ) ) )
22 21 negeqd ( 𝜑 → - Σ 𝑘𝐴 - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) = - Σ 𝑘𝐴 - ( ( 𝑊𝑘 ) · ( log ‘ ( 𝐹𝑘 ) ) ) )
23 8 rpcnd ( ( 𝜑𝑘𝐴 ) → ( 𝑊𝑘 ) ∈ ℂ )
24 7 relogcld ( ( 𝜑𝑘𝐴 ) → ( log ‘ ( 𝐹𝑘 ) ) ∈ ℝ )
25 24 recnd ( ( 𝜑𝑘𝐴 ) → ( log ‘ ( 𝐹𝑘 ) ) ∈ ℂ )
26 23 25 mulneg2d ( ( 𝜑𝑘𝐴 ) → ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) = - ( ( 𝑊𝑘 ) · ( log ‘ ( 𝐹𝑘 ) ) ) )
27 26 eqcomd ( ( 𝜑𝑘𝐴 ) → - ( ( 𝑊𝑘 ) · ( log ‘ ( 𝐹𝑘 ) ) ) = ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) )
28 27 sumeq2dv ( 𝜑 → Σ 𝑘𝐴 - ( ( 𝑊𝑘 ) · ( log ‘ ( 𝐹𝑘 ) ) ) = Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) )
29 28 negeqd ( 𝜑 → - Σ 𝑘𝐴 - ( ( 𝑊𝑘 ) · ( log ‘ ( 𝐹𝑘 ) ) ) = - Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) )
30 18 22 29 3eqtrd ( 𝜑 → Σ 𝑘𝐴 - - ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) = - Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) )
31 13 15 30 3eqtr2rd ( 𝜑 → - Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) = ( ℂfld Σg ( 𝑘𝐴 ↦ ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ) ) )
32 negex - ( log ‘ ( 𝐹𝑘 ) ) ∈ V
33 32 a1i ( ( 𝜑𝑘𝐴 ) → - ( log ‘ ( 𝐹𝑘 ) ) ∈ V )
34 5 feqmptd ( 𝜑𝑊 = ( 𝑘𝐴 ↦ ( 𝑊𝑘 ) ) )
35 eqidd ( 𝜑 → ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) = ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) )
36 2 8 33 34 35 offval2 ( 𝜑 → ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) = ( 𝑘𝐴 ↦ ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) ) )
37 36 oveq2d ( 𝜑 → ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) = ( ℂfld Σg ( 𝑘𝐴 ↦ ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) )
38 25 negcld ( ( 𝜑𝑘𝐴 ) → - ( log ‘ ( 𝐹𝑘 ) ) ∈ ℂ )
39 23 38 mulcld ( ( 𝜑𝑘𝐴 ) → ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) ∈ ℂ )
40 2 39 gsumfsum ( 𝜑 → ( ℂfld Σg ( 𝑘𝐴 ↦ ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) = Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) )
41 37 40 eqtrd ( 𝜑 → ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) = Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) )
42 41 negeqd ( 𝜑 → - ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) = - Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · - ( log ‘ ( 𝐹𝑘 ) ) ) )
43 relogf1o ( log ↾ ℝ+ ) : ℝ+1-1-onto→ ℝ
44 f1of ( ( log ↾ ℝ+ ) : ℝ+1-1-onto→ ℝ → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
45 43 44 ax-mp ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ
46 rpre ( 𝑦 ∈ ℝ+𝑦 ∈ ℝ )
47 46 anim2i ( ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ ) )
48 47 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+ ) ) → ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ ) )
49 rpcxpcl ( ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ ) → ( 𝑥𝑐 𝑦 ) ∈ ℝ+ )
50 48 49 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+ ) ) → ( 𝑥𝑐 𝑦 ) ∈ ℝ+ )
51 inidm ( 𝐴𝐴 ) = 𝐴
52 50 4 5 2 2 51 off ( 𝜑 → ( 𝐹f𝑐 𝑊 ) : 𝐴 ⟶ ℝ+ )
53 fcompt ( ( ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ∧ ( 𝐹f𝑐 𝑊 ) : 𝐴 ⟶ ℝ+ ) → ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) = ( 𝑘𝐴 ↦ ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) ) )
54 45 52 53 sylancr ( 𝜑 → ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) = ( 𝑘𝐴 ↦ ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) ) )
55 52 ffvelrnda ( ( 𝜑𝑘𝐴 ) → ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ∈ ℝ+ )
56 fvres ( ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) = ( log ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) )
57 55 56 syl ( ( 𝜑𝑘𝐴 ) → ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) = ( log ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) )
58 4 ffnd ( 𝜑𝐹 Fn 𝐴 )
59 5 ffnd ( 𝜑𝑊 Fn 𝐴 )
60 eqidd ( ( 𝜑𝑘𝐴 ) → ( 𝐹𝑘 ) = ( 𝐹𝑘 ) )
61 eqidd ( ( 𝜑𝑘𝐴 ) → ( 𝑊𝑘 ) = ( 𝑊𝑘 ) )
62 58 59 2 2 51 60 61 ofval ( ( 𝜑𝑘𝐴 ) → ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) = ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) )
63 62 fveq2d ( ( 𝜑𝑘𝐴 ) → ( log ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) = ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) )
64 57 63 eqtrd ( ( 𝜑𝑘𝐴 ) → ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) = ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) )
65 64 mpteq2dva ( 𝜑 → ( 𝑘𝐴 ↦ ( ( log ↾ ℝ+ ) ‘ ( ( 𝐹f𝑐 𝑊 ) ‘ 𝑘 ) ) ) = ( 𝑘𝐴 ↦ ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ) )
66 54 65 eqtrd ( 𝜑 → ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) = ( 𝑘𝐴 ↦ ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ) )
67 66 oveq2d ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) ) = ( ℂfld Σg ( 𝑘𝐴 ↦ ( log ‘ ( ( 𝐹𝑘 ) ↑𝑐 ( 𝑊𝑘 ) ) ) ) ) )
68 31 42 67 3eqtr4d ( 𝜑 → - ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) = ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) ) )
69 1 oveq1i ( 𝑀s ( ℂ ∖ { 0 } ) ) = ( ( mulGrp ‘ ℂfld ) ↾s ( ℂ ∖ { 0 } ) )
70 69 rpmsubg + ∈ ( SubGrp ‘ ( 𝑀s ( ℂ ∖ { 0 } ) ) )
71 subgsubm ( ℝ+ ∈ ( SubGrp ‘ ( 𝑀s ( ℂ ∖ { 0 } ) ) ) → ℝ+ ∈ ( SubMnd ‘ ( 𝑀s ( ℂ ∖ { 0 } ) ) ) )
72 70 71 ax-mp + ∈ ( SubMnd ‘ ( 𝑀s ( ℂ ∖ { 0 } ) ) )
73 cnring fld ∈ Ring
74 cnfldbas ℂ = ( Base ‘ ℂfld )
75 cnfld0 0 = ( 0g ‘ ℂfld )
76 cndrng fld ∈ DivRing
77 74 75 76 drngui ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
78 77 1 unitsubm ( ℂfld ∈ Ring → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑀 ) )
79 eqid ( 𝑀s ( ℂ ∖ { 0 } ) ) = ( 𝑀s ( ℂ ∖ { 0 } ) )
80 79 subsubm ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ 𝑀 ) → ( ℝ+ ∈ ( SubMnd ‘ ( 𝑀s ( ℂ ∖ { 0 } ) ) ) ↔ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) ) )
81 73 78 80 mp2b ( ℝ+ ∈ ( SubMnd ‘ ( 𝑀s ( ℂ ∖ { 0 } ) ) ) ↔ ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) ) )
82 72 81 mpbi ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) ∧ ℝ+ ⊆ ( ℂ ∖ { 0 } ) )
83 82 simpli + ∈ ( SubMnd ‘ 𝑀 )
84 eqid ( 𝑀s+ ) = ( 𝑀s+ )
85 84 submbas ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → ℝ+ = ( Base ‘ ( 𝑀s+ ) ) )
86 83 85 ax-mp + = ( Base ‘ ( 𝑀s+ ) )
87 cnfld1 1 = ( 1r ‘ ℂfld )
88 1 87 ringidval 1 = ( 0g𝑀 )
89 eqid ( 0g𝑀 ) = ( 0g𝑀 )
90 84 89 subm0 ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → ( 0g𝑀 ) = ( 0g ‘ ( 𝑀s+ ) ) )
91 83 90 ax-mp ( 0g𝑀 ) = ( 0g ‘ ( 𝑀s+ ) )
92 88 91 eqtri 1 = ( 0g ‘ ( 𝑀s+ ) )
93 cncrng fld ∈ CRing
94 1 crngmgp ( ℂfld ∈ CRing → 𝑀 ∈ CMnd )
95 93 94 mp1i ( 𝜑𝑀 ∈ CMnd )
96 84 submmnd ( ℝ+ ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑀s+ ) ∈ Mnd )
97 83 96 mp1i ( 𝜑 → ( 𝑀s+ ) ∈ Mnd )
98 84 subcmn ( ( 𝑀 ∈ CMnd ∧ ( 𝑀s+ ) ∈ Mnd ) → ( 𝑀s+ ) ∈ CMnd )
99 95 97 98 syl2anc ( 𝜑 → ( 𝑀s+ ) ∈ CMnd )
100 resubdrg ( ℝ ∈ ( SubRing ‘ ℂfld ) ∧ ℝfld ∈ DivRing )
101 100 simpli ℝ ∈ ( SubRing ‘ ℂfld )
102 df-refld fld = ( ℂflds ℝ )
103 102 subrgring ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝfld ∈ Ring )
104 101 103 ax-mp fld ∈ Ring
105 ringmnd ( ℝfld ∈ Ring → ℝfld ∈ Mnd )
106 104 105 mp1i ( 𝜑 → ℝfld ∈ Mnd )
107 1 oveq1i ( 𝑀s+ ) = ( ( mulGrp ‘ ℂfld ) ↾s+ )
108 107 reloggim ( log ↾ ℝ+ ) ∈ ( ( 𝑀s+ ) GrpIso ℝfld )
109 gimghm ( ( log ↾ ℝ+ ) ∈ ( ( 𝑀s+ ) GrpIso ℝfld ) → ( log ↾ ℝ+ ) ∈ ( ( 𝑀s+ ) GrpHom ℝfld ) )
110 108 109 ax-mp ( log ↾ ℝ+ ) ∈ ( ( 𝑀s+ ) GrpHom ℝfld )
111 ghmmhm ( ( log ↾ ℝ+ ) ∈ ( ( 𝑀s+ ) GrpHom ℝfld ) → ( log ↾ ℝ+ ) ∈ ( ( 𝑀s+ ) MndHom ℝfld ) )
112 110 111 mp1i ( 𝜑 → ( log ↾ ℝ+ ) ∈ ( ( 𝑀s+ ) MndHom ℝfld ) )
113 1red ( 𝜑 → 1 ∈ ℝ )
114 52 2 113 fdmfifsupp ( 𝜑 → ( 𝐹f𝑐 𝑊 ) finSupp 1 )
115 86 92 99 106 2 112 52 114 gsummhm ( 𝜑 → ( ℝfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) ) = ( ( log ↾ ℝ+ ) ‘ ( ( 𝑀s+ ) Σg ( 𝐹f𝑐 𝑊 ) ) ) )
116 subrgsubg ( ℝ ∈ ( SubRing ‘ ℂfld ) → ℝ ∈ ( SubGrp ‘ ℂfld ) )
117 101 116 ax-mp ℝ ∈ ( SubGrp ‘ ℂfld )
118 subgsubm ( ℝ ∈ ( SubGrp ‘ ℂfld ) → ℝ ∈ ( SubMnd ‘ ℂfld ) )
119 117 118 ax-mp ℝ ∈ ( SubMnd ‘ ℂfld )
120 119 a1i ( 𝜑 → ℝ ∈ ( SubMnd ‘ ℂfld ) )
121 43 44 mp1i ( 𝜑 → ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ )
122 fco ( ( ( log ↾ ℝ+ ) : ℝ+ ⟶ ℝ ∧ ( 𝐹f𝑐 𝑊 ) : 𝐴 ⟶ ℝ+ ) → ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) : 𝐴 ⟶ ℝ )
123 121 52 122 syl2anc ( 𝜑 → ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) : 𝐴 ⟶ ℝ )
124 2 120 123 102 gsumsubm ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) ) = ( ℝfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) ) )
125 83 a1i ( 𝜑 → ℝ+ ∈ ( SubMnd ‘ 𝑀 ) )
126 2 125 52 84 gsumsubm ( 𝜑 → ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) = ( ( 𝑀s+ ) Σg ( 𝐹f𝑐 𝑊 ) ) )
127 126 fveq2d ( 𝜑 → ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) = ( ( log ↾ ℝ+ ) ‘ ( ( 𝑀s+ ) Σg ( 𝐹f𝑐 𝑊 ) ) ) )
128 115 124 127 3eqtr4d ( 𝜑 → ( ℂfld Σg ( ( log ↾ ℝ+ ) ∘ ( 𝐹f𝑐 𝑊 ) ) ) = ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) )
129 88 95 2 125 52 114 gsumsubmcl ( 𝜑 → ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ∈ ℝ+ )
130 fvres ( ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ∈ ℝ+ → ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) = ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) )
131 129 130 syl ( 𝜑 → ( ( log ↾ ℝ+ ) ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) = ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) )
132 68 128 131 3eqtrd ( 𝜑 → - ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) = ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) )
133 simprl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+ ) ) → 𝑥 ∈ ℝ+ )
134 133 rpcnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+ ) ) → 𝑥 ∈ ℂ )
135 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+ ) ) → 𝑦 ∈ ℝ+ )
136 135 rpcnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+ ) ) → 𝑦 ∈ ℂ )
137 134 136 mulcomd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
138 2 5 4 137 caofcom ( 𝜑 → ( 𝑊f · 𝐹 ) = ( 𝐹f · 𝑊 ) )
139 138 oveq2d ( 𝜑 → ( ℂfld Σg ( 𝑊f · 𝐹 ) ) = ( ℂfld Σg ( 𝐹f · 𝑊 ) ) )
140 4 feqmptd ( 𝜑𝐹 = ( 𝑘𝐴 ↦ ( 𝐹𝑘 ) ) )
141 2 8 7 34 140 offval2 ( 𝜑 → ( 𝑊f · 𝐹 ) = ( 𝑘𝐴 ↦ ( ( 𝑊𝑘 ) · ( 𝐹𝑘 ) ) ) )
142 141 oveq2d ( 𝜑 → ( ℂfld Σg ( 𝑊f · 𝐹 ) ) = ( ℂfld Σg ( 𝑘𝐴 ↦ ( ( 𝑊𝑘 ) · ( 𝐹𝑘 ) ) ) ) )
143 8 7 rpmulcld ( ( 𝜑𝑘𝐴 ) → ( ( 𝑊𝑘 ) · ( 𝐹𝑘 ) ) ∈ ℝ+ )
144 143 rpcnd ( ( 𝜑𝑘𝐴 ) → ( ( 𝑊𝑘 ) · ( 𝐹𝑘 ) ) ∈ ℂ )
145 2 144 gsumfsum ( 𝜑 → ( ℂfld Σg ( 𝑘𝐴 ↦ ( ( 𝑊𝑘 ) · ( 𝐹𝑘 ) ) ) ) = Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · ( 𝐹𝑘 ) ) )
146 142 145 eqtrd ( 𝜑 → ( ℂfld Σg ( 𝑊f · 𝐹 ) ) = Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · ( 𝐹𝑘 ) ) )
147 2 3 143 fsumrpcl ( 𝜑 → Σ 𝑘𝐴 ( ( 𝑊𝑘 ) · ( 𝐹𝑘 ) ) ∈ ℝ+ )
148 146 147 eqeltrd ( 𝜑 → ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ∈ ℝ+ )
149 139 148 eqeltrrd ( 𝜑 → ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ∈ ℝ+ )
150 149 relogcld ( 𝜑 → ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ∈ ℝ )
151 ringcmn ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
152 73 151 mp1i ( 𝜑 → ℂfld ∈ CMnd )
153 remulcl ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
154 153 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
155 rpssre + ⊆ ℝ
156 fss ( ( 𝑊 : 𝐴 ⟶ ℝ+ ∧ ℝ+ ⊆ ℝ ) → 𝑊 : 𝐴 ⟶ ℝ )
157 5 155 156 sylancl ( 𝜑𝑊 : 𝐴 ⟶ ℝ )
158 24 renegcld ( ( 𝜑𝑘𝐴 ) → - ( log ‘ ( 𝐹𝑘 ) ) ∈ ℝ )
159 158 fmpttd ( 𝜑 → ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) : 𝐴 ⟶ ℝ )
160 154 157 159 2 2 51 off ( 𝜑 → ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) : 𝐴 ⟶ ℝ )
161 0red ( 𝜑 → 0 ∈ ℝ )
162 160 2 161 fdmfifsupp ( 𝜑 → ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) finSupp 0 )
163 75 152 2 120 160 162 gsumsubmcl ( 𝜑 → ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) ∈ ℝ )
164 155 a1i ( 𝜑 → ℝ+ ⊆ ℝ )
165 simpr ( ( 𝜑𝑤 ∈ ℝ+ ) → 𝑤 ∈ ℝ+ )
166 165 relogcld ( ( 𝜑𝑤 ∈ ℝ+ ) → ( log ‘ 𝑤 ) ∈ ℝ )
167 166 renegcld ( ( 𝜑𝑤 ∈ ℝ+ ) → - ( log ‘ 𝑤 ) ∈ ℝ )
168 167 fmpttd ( 𝜑 → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) : ℝ+ ⟶ ℝ )
169 simpl ( ( 𝑎 ∈ ℝ+𝑏 ∈ ℝ+ ) → 𝑎 ∈ ℝ+ )
170 ioorp ( 0 (,) +∞ ) = ℝ+
171 169 170 eleqtrrdi ( ( 𝑎 ∈ ℝ+𝑏 ∈ ℝ+ ) → 𝑎 ∈ ( 0 (,) +∞ ) )
172 simpr ( ( 𝑎 ∈ ℝ+𝑏 ∈ ℝ+ ) → 𝑏 ∈ ℝ+ )
173 172 170 eleqtrrdi ( ( 𝑎 ∈ ℝ+𝑏 ∈ ℝ+ ) → 𝑏 ∈ ( 0 (,) +∞ ) )
174 iccssioo2 ( ( 𝑎 ∈ ( 0 (,) +∞ ) ∧ 𝑏 ∈ ( 0 (,) +∞ ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 0 (,) +∞ ) )
175 171 173 174 syl2anc ( ( 𝑎 ∈ ℝ+𝑏 ∈ ℝ+ ) → ( 𝑎 [,] 𝑏 ) ⊆ ( 0 (,) +∞ ) )
176 175 170 sseqtrdi ( ( 𝑎 ∈ ℝ+𝑏 ∈ ℝ+ ) → ( 𝑎 [,] 𝑏 ) ⊆ ℝ+ )
177 176 adantl ( ( 𝜑 ∧ ( 𝑎 ∈ ℝ+𝑏 ∈ ℝ+ ) ) → ( 𝑎 [,] 𝑏 ) ⊆ ℝ+ )
178 ioossico ( 0 (,) +∞ ) ⊆ ( 0 [,) +∞ )
179 170 178 eqsstrri + ⊆ ( 0 [,) +∞ )
180 fss ( ( 𝑊 : 𝐴 ⟶ ℝ+ ∧ ℝ+ ⊆ ( 0 [,) +∞ ) ) → 𝑊 : 𝐴 ⟶ ( 0 [,) +∞ ) )
181 5 179 180 sylancl ( 𝜑𝑊 : 𝐴 ⟶ ( 0 [,) +∞ ) )
182 0lt1 0 < 1
183 182 6 breqtrrid ( 𝜑 → 0 < ( ℂfld Σg 𝑊 ) )
184 logccv ( ( ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
185 184 3adant1 ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
186 elioore ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 ∈ ℝ )
187 186 3ad2ant3 ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℝ )
188 simp21 ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑥 ∈ ℝ+ )
189 188 relogcld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
190 187 189 remulcld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( log ‘ 𝑥 ) ) ∈ ℝ )
191 1red ( 𝑡 ∈ ( 0 (,) 1 ) → 1 ∈ ℝ )
192 191 186 resubcld ( 𝑡 ∈ ( 0 (,) 1 ) → ( 1 − 𝑡 ) ∈ ℝ )
193 192 3ad2ant3 ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℝ )
194 simp22 ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑦 ∈ ℝ+ )
195 194 relogcld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
196 193 195 remulcld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ∈ ℝ )
197 190 196 readdcld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ∈ ℝ )
198 eliooord ( 𝑡 ∈ ( 0 (,) 1 ) → ( 0 < 𝑡𝑡 < 1 ) )
199 198 simpld ( 𝑡 ∈ ( 0 (,) 1 ) → 0 < 𝑡 )
200 186 199 elrpd ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 ∈ ℝ+ )
201 200 3ad2ant3 ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℝ+ )
202 201 188 rpmulcld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · 𝑥 ) ∈ ℝ+ )
203 0red ( 𝑡 ∈ ( 0 (,) 1 ) → 0 ∈ ℝ )
204 198 simprd ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 < 1 )
205 1m0e1 ( 1 − 0 ) = 1
206 204 205 breqtrrdi ( 𝑡 ∈ ( 0 (,) 1 ) → 𝑡 < ( 1 − 0 ) )
207 186 191 203 206 ltsub13d ( 𝑡 ∈ ( 0 (,) 1 ) → 0 < ( 1 − 𝑡 ) )
208 192 207 elrpd ( 𝑡 ∈ ( 0 (,) 1 ) → ( 1 − 𝑡 ) ∈ ℝ+ )
209 208 3ad2ant3 ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℝ+ )
210 209 194 rpmulcld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · 𝑦 ) ∈ ℝ+ )
211 rpaddcl ( ( ( 𝑡 · 𝑥 ) ∈ ℝ+ ∧ ( ( 1 − 𝑡 ) · 𝑦 ) ∈ ℝ+ ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ+ )
212 202 210 211 syl2anc ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ+ )
213 212 relogcld ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ ℝ )
214 197 213 ltnegd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) < ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ↔ - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) ) )
215 185 214 mpbid ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) )
216 eqidd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) )
217 fveq2 ( 𝑤 = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) → ( log ‘ 𝑤 ) = ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
218 217 adantl ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) ∧ 𝑤 = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → ( log ‘ 𝑤 ) = ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
219 218 negeqd ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) ∧ 𝑤 = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
220 negex - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ V
221 220 a1i ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) ∈ V )
222 216 219 212 221 fvmptd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) = - ( log ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) )
223 fveq2 ( 𝑤 = 𝑥 → ( log ‘ 𝑤 ) = ( log ‘ 𝑥 ) )
224 223 negeqd ( 𝑤 = 𝑥 → - ( log ‘ 𝑤 ) = - ( log ‘ 𝑥 ) )
225 eqid ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) )
226 negex - ( log ‘ 𝑤 ) ∈ V
227 224 225 226 fvmpt3i ( 𝑥 ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) = - ( log ‘ 𝑥 ) )
228 188 227 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) = - ( log ‘ 𝑥 ) )
229 228 oveq2d ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) = ( 𝑡 · - ( log ‘ 𝑥 ) ) )
230 187 recnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → 𝑡 ∈ ℂ )
231 189 recnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
232 230 231 mulneg2d ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · - ( log ‘ 𝑥 ) ) = - ( 𝑡 · ( log ‘ 𝑥 ) ) )
233 229 232 eqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) = - ( 𝑡 · ( log ‘ 𝑥 ) ) )
234 fveq2 ( 𝑤 = 𝑦 → ( log ‘ 𝑤 ) = ( log ‘ 𝑦 ) )
235 234 negeqd ( 𝑤 = 𝑦 → - ( log ‘ 𝑤 ) = - ( log ‘ 𝑦 ) )
236 235 225 226 fvmpt3i ( 𝑦 ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) = - ( log ‘ 𝑦 ) )
237 194 236 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) = - ( log ‘ 𝑦 ) )
238 237 oveq2d ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) = ( ( 1 − 𝑡 ) · - ( log ‘ 𝑦 ) ) )
239 209 rpcnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 1 − 𝑡 ) ∈ ℂ )
240 195 recnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( log ‘ 𝑦 ) ∈ ℂ )
241 239 240 mulneg2d ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · - ( log ‘ 𝑦 ) ) = - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) )
242 238 241 eqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) = - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) )
243 233 242 oveq12d ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) = ( - ( 𝑡 · ( log ‘ 𝑥 ) ) + - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) )
244 190 recnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( 𝑡 · ( log ‘ 𝑥 ) ) ∈ ℂ )
245 196 recnd ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ∈ ℂ )
246 244 245 negdid ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) = ( - ( 𝑡 · ( log ‘ 𝑥 ) ) + - ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) )
247 243 246 eqtr4d ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) = - ( ( 𝑡 · ( log ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( log ‘ 𝑦 ) ) ) )
248 215 222 247 3brtr4d ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦 ) ∧ 𝑡 ∈ ( 0 (,) 1 ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ) < ( ( 𝑡 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑥 ) ) + ( ( 1 − 𝑡 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑦 ) ) ) )
249 164 168 177 248 scvxcvx ( ( 𝜑 ∧ ( 𝑢 ∈ ℝ+𝑣 ∈ ℝ+𝑠 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( 𝑠 · 𝑢 ) + ( ( 1 − 𝑠 ) · 𝑣 ) ) ) ≤ ( ( 𝑠 · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑢 ) ) + ( ( 1 − 𝑠 ) · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ 𝑣 ) ) ) )
250 164 168 177 2 181 4 183 249 jensen ( 𝜑 → ( ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ∈ ℝ+ ∧ ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ) ≤ ( ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg 𝑊 ) ) ) )
251 250 simprd ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ) ≤ ( ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg 𝑊 ) ) )
252 6 oveq2d ( 𝜑 → ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) = ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / 1 ) )
253 252 fveq2d ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ) = ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / 1 ) ) )
254 148 rpcnd ( 𝜑 → ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ∈ ℂ )
255 254 div1d ( 𝜑 → ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / 1 ) = ( ℂfld Σg ( 𝑊f · 𝐹 ) ) )
256 255 fveq2d ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / 1 ) ) = ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) )
257 fveq2 ( 𝑤 = ( ℂfld Σg ( 𝑊f · 𝐹 ) ) → ( log ‘ 𝑤 ) = ( log ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) )
258 257 negeqd ( 𝑤 = ( ℂfld Σg ( 𝑊f · 𝐹 ) ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) )
259 258 225 226 fvmpt3i ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ∈ ℝ+ → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) )
260 148 259 syl ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) )
261 139 fveq2d ( 𝜑 → ( log ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) = ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) )
262 261 negeqd ( 𝜑 → - ( log ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) )
263 260 262 eqtrd ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ℂfld Σg ( 𝑊f · 𝐹 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) )
264 253 256 263 3eqtrd ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ‘ ( ( ℂfld Σg ( 𝑊f · 𝐹 ) ) / ( ℂfld Σg 𝑊 ) ) ) = - ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) )
265 6 oveq2d ( 𝜑 → ( ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg 𝑊 ) ) = ( ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / 1 ) )
266 ringmnd ( ℂfld ∈ Ring → ℂfld ∈ Mnd )
267 73 266 ax-mp fld ∈ Mnd
268 74 submid ( ℂfld ∈ Mnd → ℂ ∈ ( SubMnd ‘ ℂfld ) )
269 267 268 mp1i ( 𝜑 → ℂ ∈ ( SubMnd ‘ ℂfld ) )
270 mulcl ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
271 270 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
272 rpcn ( 𝑥 ∈ ℝ+𝑥 ∈ ℂ )
273 272 ssriv + ⊆ ℂ
274 273 a1i ( 𝜑 → ℝ+ ⊆ ℂ )
275 5 274 fssd ( 𝜑𝑊 : 𝐴 ⟶ ℂ )
276 166 recnd ( ( 𝜑𝑤 ∈ ℝ+ ) → ( log ‘ 𝑤 ) ∈ ℂ )
277 276 negcld ( ( 𝜑𝑤 ∈ ℝ+ ) → - ( log ‘ 𝑤 ) ∈ ℂ )
278 277 fmpttd ( 𝜑 → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) : ℝ+ ⟶ ℂ )
279 fco ( ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) : ℝ+ ⟶ ℂ ∧ 𝐹 : 𝐴 ⟶ ℝ+ ) → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) : 𝐴 ⟶ ℂ )
280 278 4 279 syl2anc ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) : 𝐴 ⟶ ℂ )
281 271 275 280 2 2 51 off ( 𝜑 → ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) : 𝐴 ⟶ ℂ )
282 281 2 161 fdmfifsupp ( 𝜑 → ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) finSupp 0 )
283 75 152 2 269 281 282 gsumsubmcl ( 𝜑 → ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) ∈ ℂ )
284 283 div1d ( 𝜑 → ( ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / 1 ) = ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) )
285 eqidd ( 𝜑 → ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) = ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) )
286 fveq2 ( 𝑤 = ( 𝐹𝑘 ) → ( log ‘ 𝑤 ) = ( log ‘ ( 𝐹𝑘 ) ) )
287 286 negeqd ( 𝑤 = ( 𝐹𝑘 ) → - ( log ‘ 𝑤 ) = - ( log ‘ ( 𝐹𝑘 ) ) )
288 7 140 285 287 fmptco ( 𝜑 → ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) = ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) )
289 288 oveq2d ( 𝜑 → ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) = ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) )
290 289 oveq2d ( 𝜑 → ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) = ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) )
291 265 284 290 3eqtrd ( 𝜑 → ( ( ℂfld Σg ( 𝑊f · ( ( 𝑤 ∈ ℝ+ ↦ - ( log ‘ 𝑤 ) ) ∘ 𝐹 ) ) ) / ( ℂfld Σg 𝑊 ) ) = ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) )
292 251 264 291 3brtr3d ( 𝜑 → - ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ≤ ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) )
293 150 163 292 lenegcon1d ( 𝜑 → - ( ℂfld Σg ( 𝑊f · ( 𝑘𝐴 ↦ - ( log ‘ ( 𝐹𝑘 ) ) ) ) ) ≤ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) )
294 132 293 eqbrtrrd ( 𝜑 → ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ≤ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) )
295 129 relogcld ( 𝜑 → ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ∈ ℝ )
296 efle ( ( ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ∈ ℝ ∧ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ∈ ℝ ) → ( ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ≤ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ↔ ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ) ≤ ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ) ) )
297 295 150 296 syl2anc ( 𝜑 → ( ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ≤ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ↔ ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ) ≤ ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ) ) )
298 294 297 mpbid ( 𝜑 → ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ) ≤ ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ) )
299 129 reeflogd ( 𝜑 → ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ) = ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) )
300 299 eqcomd ( 𝜑 → ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) = ( exp ‘ ( log ‘ ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ) ) )
301 149 reeflogd ( 𝜑 → ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ) = ( ℂfld Σg ( 𝐹f · 𝑊 ) ) )
302 301 eqcomd ( 𝜑 → ( ℂfld Σg ( 𝐹f · 𝑊 ) ) = ( exp ‘ ( log ‘ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) ) ) )
303 298 300 302 3brtr4d ( 𝜑 → ( 𝑀 Σg ( 𝐹f𝑐 𝑊 ) ) ≤ ( ℂfld Σg ( 𝐹f · 𝑊 ) ) )