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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
8 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑊 ‘ 𝑘 ) ∈ ℝ+ )
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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ∘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 = ( ℂfld ↾s ℝ )
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 · 𝑊 ) ) )