amgmwlem - Mathbox for Kunhao Zheng

	Mathbox for Kunhao Zheng		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > amgmwlem		Structured version Visualization version GIF version

Theorem amgmwlem 47803

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

**Hypotheses**
Ref	Expression
amgmwlem.0	⊢ 𝑀 = (mulGrp‘ℂ_fld)
amgmwlem.1	⊢ (𝜑 → 𝐴 ∈ Fin)
amgmwlem.2	⊢ (𝜑 → 𝐴 ≠ ∅)
amgmwlem.3	⊢ (𝜑 → 𝐹:𝐴⟶ℝ⁺)
amgmwlem.4	⊢ (𝜑 → 𝑊:𝐴⟶ℝ⁺)
amgmwlem.5	⊢ (𝜑 → (ℂ_fld Σ_g 𝑊) = 1)

**Assertion**
Ref	Expression
amgmwlem	⊢ (𝜑 → (𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)) ≤ (ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)))

Proof of Theorem amgmwlem Dummy variables 𝑎 𝑏 𝑠 𝑢 𝑣 𝑘 𝑦 𝑤 𝑥 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		amgmwlem.1	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ Fin)
2		amgmwlem.3	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ⁺)
3	2	ffvelcdmda 7084	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℝ⁺)
4		amgmwlem.4	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑊:𝐴⟶ℝ⁺)
5	4	ffvelcdmda 7084	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ⁺)
6	5	rpred 13013	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℝ)
7	3, 6	rpcxpcld 26232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘)) ∈ ℝ⁺)
8	7	relogcld 26123	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) ∈ ℝ)
9	8	recnd 11239	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) ∈ ℂ)
10	1, 9	gsumfsum 21005	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))) = Σ𝑘 ∈ 𝐴 (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))
11	9	negnegd 11559	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → --(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) = (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))
12	11	sumeq2dv 15646	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) = Σ𝑘 ∈ 𝐴 (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))
13	8	renegcld 11638	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) ∈ ℝ)
14	13	recnd 11239	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) ∈ ℂ)
15	1, 14	fsumneg 15730	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))
16	3, 6	logcxpd 26233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) = ((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
17	16	negeqd 11451	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) = -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
18	17	sumeq2dv 15646	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) = Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
19	18	negeqd 11451	. . . . . . . 8 ⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
20	5	rpcnd 13015	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) ∈ ℂ)
21	3	relogcld 26123	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℝ)
22	21	recnd 11239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘(𝐹‘𝑘)) ∈ ℂ)
23	20, 22	mulneg2d 11665	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) = -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))))
24	23	eqcomd 2739	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
25	24	sumeq2dv 15646	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
26	25	negeqd 11451	. . . . . . . 8 ⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 -((𝑊‘𝑘) · (log‘(𝐹‘𝑘))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
27	15, 19, 26	3eqtrd 2777	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 --(log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
28	10, 12, 27	3eqtr2rd 2780	. . . . . 6 ⊢ (𝜑 → -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))))
29		negex 11455	. . . . . . . . . . 11 ⊢ -(log‘(𝐹‘𝑘)) ∈ V
30	29	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ V)
31	4	feqmptd 6958	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊 = (𝑘 ∈ 𝐴 ↦ (𝑊‘𝑘)))
32		eqidd 2734	. . . . . . . . . 10 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))
33	1, 5, 30, 31, 32	offval2 7687	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘)))))
34	33	oveq2d 7422	. . . . . . . 8 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))))
35	22	negcld 11555	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℂ)
36	20, 35	mulcld 11231	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))) ∈ ℂ)
37	1, 36	gsumfsum 21005	. . . . . . . 8 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
38	34, 37	eqtrd 2773	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
39	38	negeqd 11451	. . . . . 6 ⊢ (𝜑 → -(ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = -Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · -(log‘(𝐹‘𝑘))))
40		relogf1o 26067	. . . . . . . . . 10 ⊢ (log ↾ ℝ⁺):ℝ⁺–1-1-onto→ℝ
41		f1of 6831	. . . . . . . . . 10 ⊢ ((log ↾ ℝ⁺):ℝ⁺–1-1-onto→ℝ → (log ↾ ℝ⁺):ℝ⁺⟶ℝ)
42	40, 41	ax-mp 5	. . . . . . . . 9 ⊢ (log ↾ ℝ⁺):ℝ⁺⟶ℝ
43		rpre 12979	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ⁺ → 𝑦 ∈ ℝ)
44	43	anim2i 618	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺) → (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ))
45	44	adantl 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ))
46		rpcxpcl 26176	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ) → (𝑥↑_𝑐𝑦) ∈ ℝ⁺)
47	45, 46	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → (𝑥↑_𝑐𝑦) ∈ ℝ⁺)
48		inidm 4218	. . . . . . . . . 10 ⊢ (𝐴 ∩ 𝐴) = 𝐴
49	47, 2, 4, 1, 1, 48	off 7685	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∘_f ↑_𝑐𝑊):𝐴⟶ℝ⁺)
50		fcompt 7128	. . . . . . . . 9 ⊢ (((log ↾ ℝ⁺):ℝ⁺⟶ℝ ∧ (𝐹 ∘_f ↑_𝑐𝑊):𝐴⟶ℝ⁺) → ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ ((log ↾ ℝ⁺)‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘))))
51	42, 49, 50	sylancr 588	. . . . . . . 8 ⊢ (𝜑 → ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ ((log ↾ ℝ⁺)‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘))))
52	49	ffvelcdmda 7084	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘) ∈ ℝ⁺)
53		fvres 6908	. . . . . . . . . . 11 ⊢ (((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘) ∈ ℝ⁺ → ((log ↾ ℝ⁺)‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘)) = (log‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘)))
54	52, 53	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((log ↾ ℝ⁺)‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘)) = (log‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘)))
55	2	ffnd 6716	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 Fn 𝐴)
56	4	ffnd 6716	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑊 Fn 𝐴)
57		eqidd 2734	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) = (𝐹‘𝑘))
58		eqidd 2734	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑊‘𝑘) = (𝑊‘𝑘))
59	55, 56, 1, 1, 48, 57, 58	ofval 7678	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘) = ((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘)))
60	59	fveq2d 6893	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (log‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘)) = (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))
61	54, 60	eqtrd 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((log ↾ ℝ⁺)‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘)) = (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))
62	61	mpteq2dva 5248	. . . . . . . 8 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((log ↾ ℝ⁺)‘((𝐹 ∘_f ↑_𝑐𝑊)‘𝑘))) = (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘)))))
63	51, 62	eqtrd 2773	. . . . . . 7 ⊢ (𝜑 → ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊)) = (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘)))))
64	63	oveq2d 7422	. . . . . 6 ⊢ (𝜑 → (ℂ_fld Σ_g ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊))) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ (log‘((𝐹‘𝑘)↑_𝑐(𝑊‘𝑘))))))
65	28, 39, 64	3eqtr4d 2783	. . . . 5 ⊢ (𝜑 → -(ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (ℂ_fld Σ_g ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊))))
66		amgmwlem.0	. . . . . . . . . . . . 13 ⊢ 𝑀 = (mulGrp‘ℂ_fld)
67	66	oveq1i 7416	. . . . . . . . . . . 12 ⊢ (𝑀 ↾_s (ℂ ∖ {0})) = ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))
68	67	rpmsubg 21002	. . . . . . . . . . 11 ⊢ ℝ⁺ ∈ (SubGrp‘(𝑀 ↾_s (ℂ ∖ {0})))
69		subgsubm 19023	. . . . . . . . . . 11 ⊢ (ℝ⁺ ∈ (SubGrp‘(𝑀 ↾_s (ℂ ∖ {0}))) → ℝ⁺ ∈ (SubMnd‘(𝑀 ↾_s (ℂ ∖ {0}))))
70	68, 69	ax-mp 5	. . . . . . . . . 10 ⊢ ℝ⁺ ∈ (SubMnd‘(𝑀 ↾_s (ℂ ∖ {0})))
71		cnring 20960	. . . . . . . . . . 11 ⊢ ℂ_fld ∈ Ring
72		cnfldbas 20941	. . . . . . . . . . . . 13 ⊢ ℂ = (Base‘ℂ_fld)
73		cnfld0 20962	. . . . . . . . . . . . 13 ⊢ 0 = (0_g‘ℂ_fld)
74		cndrng 20967	. . . . . . . . . . . . 13 ⊢ ℂ_fld ∈ DivRing
75	72, 73, 74	drngui 20314	. . . . . . . . . . . 12 ⊢ (ℂ ∖ {0}) = (Unit‘ℂ_fld)
76	75, 66	unitsubm 20193	. . . . . . . . . . 11 ⊢ (ℂ_fld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
77		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑀 ↾_s (ℂ ∖ {0})) = (𝑀 ↾_s (ℂ ∖ {0}))
78	77	subsubm 18694	. . . . . . . . . . 11 ⊢ ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ⁺ ∈ (SubMnd‘(𝑀 ↾_s (ℂ ∖ {0}))) ↔ (ℝ⁺ ∈ (SubMnd‘𝑀) ∧ ℝ⁺ ⊆ (ℂ ∖ {0}))))
79	71, 76, 78	mp2b 10	. . . . . . . . . 10 ⊢ (ℝ⁺ ∈ (SubMnd‘(𝑀 ↾_s (ℂ ∖ {0}))) ↔ (ℝ⁺ ∈ (SubMnd‘𝑀) ∧ ℝ⁺ ⊆ (ℂ ∖ {0})))
80	70, 79	mpbi 229	. . . . . . . . 9 ⊢ (ℝ⁺ ∈ (SubMnd‘𝑀) ∧ ℝ⁺ ⊆ (ℂ ∖ {0}))
81	80	simpli 485	. . . . . . . 8 ⊢ ℝ⁺ ∈ (SubMnd‘𝑀)
82		eqid 2733	. . . . . . . . 9 ⊢ (𝑀 ↾_s ℝ⁺) = (𝑀 ↾_s ℝ⁺)
83	82	submbas 18692	. . . . . . . 8 ⊢ (ℝ⁺ ∈ (SubMnd‘𝑀) → ℝ⁺ = (Base‘(𝑀 ↾_s ℝ⁺)))
84	81, 83	ax-mp 5	. . . . . . 7 ⊢ ℝ⁺ = (Base‘(𝑀 ↾_s ℝ⁺))
85		cnfld1 20963	. . . . . . . . 9 ⊢ 1 = (1_r‘ℂ_fld)
86	66, 85	ringidval 20001	. . . . . . . 8 ⊢ 1 = (0_g‘𝑀)
87		eqid 2733	. . . . . . . . . 10 ⊢ (0_g‘𝑀) = (0_g‘𝑀)
88	82, 87	subm0 18693	. . . . . . . . 9 ⊢ (ℝ⁺ ∈ (SubMnd‘𝑀) → (0_g‘𝑀) = (0_g‘(𝑀 ↾_s ℝ⁺)))
89	81, 88	ax-mp 5	. . . . . . . 8 ⊢ (0_g‘𝑀) = (0_g‘(𝑀 ↾_s ℝ⁺))
90	86, 89	eqtri 2761	. . . . . . 7 ⊢ 1 = (0_g‘(𝑀 ↾_s ℝ⁺))
91		cncrng 20959	. . . . . . . . 9 ⊢ ℂ_fld ∈ CRing
92	66	crngmgp 20058	. . . . . . . . 9 ⊢ (ℂ_fld ∈ CRing → 𝑀 ∈ CMnd)
93	91, 92	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ CMnd)
94	82	submmnd 18691	. . . . . . . . 9 ⊢ (ℝ⁺ ∈ (SubMnd‘𝑀) → (𝑀 ↾_s ℝ⁺) ∈ Mnd)
95	81, 94	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → (𝑀 ↾_s ℝ⁺) ∈ Mnd)
96	82	subcmn 19700	. . . . . . . 8 ⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾_s ℝ⁺) ∈ Mnd) → (𝑀 ↾_s ℝ⁺) ∈ CMnd)
97	93, 95, 96	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑀 ↾_s ℝ⁺) ∈ CMnd)
98		resubdrg 21153	. . . . . . . . . 10 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) ∧ ℝ_fld ∈ DivRing)
99	98	simpli 485	. . . . . . . . 9 ⊢ ℝ ∈ (SubRing‘ℂ_fld)
100		df-refld 21150	. . . . . . . . . 10 ⊢ ℝ_fld = (ℂ_fld ↾_s ℝ)
101	100	subrgring 20359	. . . . . . . . 9 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) → ℝ_fld ∈ Ring)
102	99, 101	ax-mp 5	. . . . . . . 8 ⊢ ℝ_fld ∈ Ring
103		ringmnd 20060	. . . . . . . 8 ⊢ (ℝ_fld ∈ Ring → ℝ_fld ∈ Mnd)
104	102, 103	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ℝ_fld ∈ Mnd)
105	66	oveq1i 7416	. . . . . . . . . 10 ⊢ (𝑀 ↾_s ℝ⁺) = ((mulGrp‘ℂ_fld) ↾_s ℝ⁺)
106	105	reloggim 26099	. . . . . . . . 9 ⊢ (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpIso ℝ_fld)
107		gimghm 19133	. . . . . . . . 9 ⊢ ((log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpIso ℝ_fld) → (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpHom ℝ_fld))
108	106, 107	ax-mp 5	. . . . . . . 8 ⊢ (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpHom ℝ_fld)
109		ghmmhm 19097	. . . . . . . 8 ⊢ ((log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) GrpHom ℝ_fld) → (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) MndHom ℝ_fld))
110	108, 109	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (log ↾ ℝ⁺) ∈ ((𝑀 ↾_s ℝ⁺) MndHom ℝ_fld))
111		1red 11212	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℝ)
112	49, 1, 111	fdmfifsupp 9370	. . . . . . 7 ⊢ (𝜑 → (𝐹 ∘_f ↑_𝑐𝑊) finSupp 1)
113	84, 90, 97, 104, 1, 110, 49, 112	gsummhm 19801	. . . . . 6 ⊢ (𝜑 → (ℝ_fld Σ_g ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊))) = ((log ↾ ℝ⁺)‘((𝑀 ↾_s ℝ⁺) Σ_g (𝐹 ∘_f ↑_𝑐𝑊))))
114		subrgsubg 20362	. . . . . . . . . 10 ⊢ (ℝ ∈ (SubRing‘ℂ_fld) → ℝ ∈ (SubGrp‘ℂ_fld))
115	99, 114	ax-mp 5	. . . . . . . . 9 ⊢ ℝ ∈ (SubGrp‘ℂ_fld)
116		subgsubm 19023	. . . . . . . . 9 ⊢ (ℝ ∈ (SubGrp‘ℂ_fld) → ℝ ∈ (SubMnd‘ℂ_fld))
117	115, 116	ax-mp 5	. . . . . . . 8 ⊢ ℝ ∈ (SubMnd‘ℂ_fld)
118	117	a1i 11	. . . . . . 7 ⊢ (𝜑 → ℝ ∈ (SubMnd‘ℂ_fld))
119	40, 41	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → (log ↾ ℝ⁺):ℝ⁺⟶ℝ)
120		fco 6739	. . . . . . . 8 ⊢ (((log ↾ ℝ⁺):ℝ⁺⟶ℝ ∧ (𝐹 ∘_f ↑_𝑐𝑊):𝐴⟶ℝ⁺) → ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊)):𝐴⟶ℝ)
121	119, 49, 120	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊)):𝐴⟶ℝ)
122	1, 118, 121, 100	gsumsubm 18713	. . . . . 6 ⊢ (𝜑 → (ℂ_fld Σ_g ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊))) = (ℝ_fld Σ_g ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊))))
123	81	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ⁺ ∈ (SubMnd‘𝑀))
124	1, 123, 49, 82	gsumsubm 18713	. . . . . . 7 ⊢ (𝜑 → (𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)) = ((𝑀 ↾_s ℝ⁺) Σ_g (𝐹 ∘_f ↑_𝑐𝑊)))
125	124	fveq2d 6893	. . . . . 6 ⊢ (𝜑 → ((log ↾ ℝ⁺)‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))) = ((log ↾ ℝ⁺)‘((𝑀 ↾_s ℝ⁺) Σ_g (𝐹 ∘_f ↑_𝑐𝑊))))
126	113, 122, 125	3eqtr4d 2783	. . . . 5 ⊢ (𝜑 → (ℂ_fld Σ_g ((log ↾ ℝ⁺) ∘ (𝐹 ∘_f ↑_𝑐𝑊))) = ((log ↾ ℝ⁺)‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))))
127	86, 93, 1, 123, 49, 112	gsumsubmcl 19782	. . . . . 6 ⊢ (𝜑 → (𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)) ∈ ℝ⁺)
128		fvres 6908	. . . . . 6 ⊢ ((𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)) ∈ ℝ⁺ → ((log ↾ ℝ⁺)‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))) = (log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))))
129	127, 128	syl 17	. . . . 5 ⊢ (𝜑 → ((log ↾ ℝ⁺)‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))) = (log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))))
130	65, 126, 129	3eqtrd 2777	. . . 4 ⊢ (𝜑 → -(ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) = (log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))))
131		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → 𝑥 ∈ ℝ⁺)
132	131	rpcnd 13015	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → 𝑥 ∈ ℂ)
133		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → 𝑦 ∈ ℝ⁺)
134	133	rpcnd 13015	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → 𝑦 ∈ ℂ)
135	132, 134	mulcomd 11232	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
136	1, 4, 2, 135	caofcom 7702	. . . . . . . 8 ⊢ (𝜑 → (𝑊 ∘_f · 𝐹) = (𝐹 ∘_f · 𝑊))
137	136	oveq2d 7422	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) = (ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)))
138	2	feqmptd 6958	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))
139	1, 5, 3, 31, 138	offval2 7687	. . . . . . . . . 10 ⊢ (𝜑 → (𝑊 ∘_f · 𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘))))
140	139	oveq2d 7422	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) = (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))))
141	5, 3	rpmulcld 13029	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ⁺)
142	141	rpcnd 13015	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℂ)
143	1, 142	gsumfsum 21005	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑘 ∈ 𝐴 ↦ ((𝑊‘𝑘) · (𝐹‘𝑘)))) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
144	140, 143	eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) = Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)))
145		amgmwlem.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ≠ ∅)
146	1, 145, 141	fsumrpcl 15680	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝑊‘𝑘) · (𝐹‘𝑘)) ∈ ℝ⁺)
147	144, 146	eqeltrd 2834	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) ∈ ℝ⁺)
148	137, 147	eqeltrrd 2835	. . . . . 6 ⊢ (𝜑 → (ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)) ∈ ℝ⁺)
149	148	relogcld 26123	. . . . 5 ⊢ (𝜑 → (log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))) ∈ ℝ)
150		ringcmn 20093	. . . . . . 7 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ CMnd)
151	71, 150	mp1i 13	. . . . . 6 ⊢ (𝜑 → ℂ_fld ∈ CMnd)
152		remulcl 11192	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
153	152	adantl 483	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
154		rpssre 12978	. . . . . . . 8 ⊢ ℝ⁺ ⊆ ℝ
155		fss 6732	. . . . . . . 8 ⊢ ((𝑊:𝐴⟶ℝ⁺ ∧ ℝ⁺ ⊆ ℝ) → 𝑊:𝐴⟶ℝ)
156	4, 154, 155	sylancl 587	. . . . . . 7 ⊢ (𝜑 → 𝑊:𝐴⟶ℝ)
157	21	renegcld 11638	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → -(log‘(𝐹‘𝑘)) ∈ ℝ)
158	157	fmpttd 7112	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))):𝐴⟶ℝ)
159	153, 156, 158, 1, 1, 48	off 7685	. . . . . 6 ⊢ (𝜑 → (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))):𝐴⟶ℝ)
160		0red 11214	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℝ)
161	159, 1, 160	fdmfifsupp 9370	. . . . . 6 ⊢ (𝜑 → (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))) finSupp 0)
162	73, 151, 1, 118, 159, 161	gsumsubmcl 19782	. . . . 5 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) ∈ ℝ)
163	154	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ℝ⁺ ⊆ ℝ)
164		simpr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → 𝑤 ∈ ℝ⁺)
165	164	relogcld 26123	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (log‘𝑤) ∈ ℝ)
166	165	renegcld 11638	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → -(log‘𝑤) ∈ ℝ)
167	166	fmpttd 7112	. . . . . . . 8 ⊢ (𝜑 → (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)):ℝ⁺⟶ℝ)
168		simpl 484	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑎 ∈ ℝ⁺)
169		ioorp 13399	. . . . . . . . . . . 12 ⊢ (0(,)+∞) = ℝ⁺
170	168, 169	eleqtrrdi 2845	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑎 ∈ (0(,)+∞))
171		simpr 486	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑏 ∈ ℝ⁺)
172	171, 169	eleqtrrdi 2845	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → 𝑏 ∈ (0(,)+∞))
173		iccssioo2 13394	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
174	170, 172, 173	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
175	174, 169	sseqtrdi 4032	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺) → (𝑎[,]𝑏) ⊆ ℝ⁺)
176	175	adantl 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ ℝ⁺ ∧ 𝑏 ∈ ℝ⁺)) → (𝑎[,]𝑏) ⊆ ℝ⁺)
177		ioossico 13412	. . . . . . . . . 10 ⊢ (0(,)+∞) ⊆ (0[,)+∞)
178	169, 177	eqsstrri 4017	. . . . . . . . 9 ⊢ ℝ⁺ ⊆ (0[,)+∞)
179		fss 6732	. . . . . . . . 9 ⊢ ((𝑊:𝐴⟶ℝ⁺ ∧ ℝ⁺ ⊆ (0[,)+∞)) → 𝑊:𝐴⟶(0[,)+∞))
180	4, 178, 179	sylancl 587	. . . . . . . 8 ⊢ (𝜑 → 𝑊:𝐴⟶(0[,)+∞))
181		0lt1 11733	. . . . . . . . 9 ⊢ 0 < 1
182		amgmwlem.5	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g 𝑊) = 1)
183	181, 182	breqtrrid 5186	. . . . . . . 8 ⊢ (𝜑 → 0 < (ℂ_fld Σ_g 𝑊))
184		logccv 26163	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
185	184	3adant1 1131	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
186		elioore 13351	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
187	186	3ad2ant3 1136	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
188		simp21 1207	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ⁺)
189	188	relogcld 26123	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
190	187, 189	remulcld 11241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
191		1red 11212	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
192	191, 186	resubcld 11639	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
193	192	3ad2ant3 1136	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
194		simp22 1208	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ⁺)
195	194	relogcld 26123	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
196	193, 195	remulcld 11241	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
197	190, 196	readdcld 11240	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ)
198		eliooord 13380	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → (0 < 𝑡 ∧ 𝑡 < 1))
199	198	simpld 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → 0 < 𝑡)
200	186, 199	elrpd 13010	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ⁺)
201	200	3ad2ant3 1136	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ⁺)
202	201, 188	rpmulcld 13029	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · 𝑥) ∈ ℝ⁺)
203		0red 11214	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
204	198	simprd 497	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 < 1)
205		1m0e1 12330	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 − 0) = 1
206	204, 205	breqtrrdi 5190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
207	186, 191, 203, 206	ltsub13d 11817	. . . . . . . . . . . . . . . . 17 ⊢ (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
208	192, 207	elrpd 13010	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ⁺)
209	208	3ad2ant3 1136	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ⁺)
210	209, 194	rpmulcld 13029	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · 𝑦) ∈ ℝ⁺)
211		rpaddcl 12993	. . . . . . . . . . . . . 14 ⊢ (((𝑡 · 𝑥) ∈ ℝ⁺ ∧ ((1 − 𝑡) · 𝑦) ∈ ℝ⁺) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ⁺)
212	202, 210, 211	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ⁺)
213	212	relogcld 26123	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ)
214	197, 213	ltnegd 11789	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))))
215	185, 214	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
216		eqidd 2734	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)))
217		fveq2 6889	. . . . . . . . . . . . 13 ⊢ (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
218	217	adantl 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
219	218	negeqd 11451	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
220		negex 11455	. . . . . . . . . . . 12 ⊢ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V
221	220	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V)
222	216, 219, 212, 221	fvmptd 7003	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
223		fveq2 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥))
224	223	negeqd 11451	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥))
225		eqid 2733	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))
226		negex 11455	. . . . . . . . . . . . . . . 16 ⊢ -(log‘𝑤) ∈ V
227	224, 225, 226	fvmpt3i 7001	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ⁺ → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
228	188, 227	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
229	228	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥)))
230	187	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
231	189	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℂ)
232	230, 231	mulneg2d 11665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥)))
233	229, 232	eqtrd 2773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥)))
234		fveq2 6889	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦))
235	234	negeqd 11451	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦))
236	235, 225, 226	fvmpt3i 7001	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ⁺ → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
237	194, 236	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
238	237	oveq2d 7422	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦)))
239	209	rpcnd 13015	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
240	195	recnd 11239	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℂ)
241	239, 240	mulneg2d 11665	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
242	238, 241	eqtrd 2773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
243	233, 242	oveq12d 7424	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
244	190	recnd 11239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ)
245	196	recnd 11239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℂ)
246	244, 245	negdid 11581	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
247	243, 246	eqtr4d 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
248	215, 222, 247	3brtr4d 5180	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ ℝ⁺ ∧ 𝑦 ∈ ℝ⁺ ∧ 𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑦))))
249	163, 167, 176, 248	scvxcvx 26480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ ℝ⁺ ∧ 𝑣 ∈ ℝ⁺ ∧ 𝑠 ∈ (0[,]1))) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘𝑣))))
250	163, 167, 176, 1, 180, 2, 183, 249	jensen 26483	. . . . . . 7 ⊢ (𝜑 → (((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / (ℂ_fld Σ_g 𝑊)) ∈ ℝ⁺ ∧ ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / (ℂ_fld Σ_g 𝑊))) ≤ ((ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂ_fld Σ_g 𝑊))))
251	250	simprd 497	. . . . . 6 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / (ℂ_fld Σ_g 𝑊))) ≤ ((ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂ_fld Σ_g 𝑊)))
252	182	oveq2d 7422	. . . . . . . 8 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / (ℂ_fld Σ_g 𝑊)) = ((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / 1))
253	252	fveq2d 6893	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / (ℂ_fld Σ_g 𝑊))) = ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / 1)))
254	147	rpcnd 13015	. . . . . . . . 9 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) ∈ ℂ)
255	254	div1d 11979	. . . . . . . 8 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / 1) = (ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)))
256	255	fveq2d 6893	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / 1)) = ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))))
257		fveq2 6889	. . . . . . . . . . 11 ⊢ (𝑤 = (ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) → (log‘𝑤) = (log‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))))
258	257	negeqd 11451	. . . . . . . . . 10 ⊢ (𝑤 = (ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) → -(log‘𝑤) = -(log‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))))
259	258, 225, 226	fvmpt3i 7001	. . . . . . . . 9 ⊢ ((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) ∈ ℝ⁺ → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))) = -(log‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))))
260	147, 259	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))) = -(log‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))))
261	137	fveq2d 6893	. . . . . . . . 9 ⊢ (𝜑 → (log‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))) = (log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))))
262	261	negeqd 11451	. . . . . . . 8 ⊢ (𝜑 → -(log‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))) = -(log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))))
263	260, 262	eqtrd 2773	. . . . . . 7 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘(ℂ_fld Σ_g (𝑊 ∘_f · 𝐹))) = -(log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))))
264	253, 256, 263	3eqtrd 2777	. . . . . 6 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤))‘((ℂ_fld Σ_g (𝑊 ∘_f · 𝐹)) / (ℂ_fld Σ_g 𝑊))) = -(log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))))
265	182	oveq2d 7422	. . . . . . 7 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂ_fld Σ_g 𝑊)) = ((ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1))
266		ringmnd 20060	. . . . . . . . . . 11 ⊢ (ℂ_fld ∈ Ring → ℂ_fld ∈ Mnd)
267	71, 266	ax-mp 5	. . . . . . . . . 10 ⊢ ℂ_fld ∈ Mnd
268	72	submid 18688	. . . . . . . . . 10 ⊢ (ℂ_fld ∈ Mnd → ℂ ∈ (SubMnd‘ℂ_fld))
269	267, 268	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ℂ ∈ (SubMnd‘ℂ_fld))
270		mulcl 11191	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
271	270	adantl 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
272		rpcn 12981	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ⁺ → 𝑥 ∈ ℂ)
273	272	ssriv 3986	. . . . . . . . . . . 12 ⊢ ℝ⁺ ⊆ ℂ
274	273	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → ℝ⁺ ⊆ ℂ)
275	4, 274	fssd 6733	. . . . . . . . . 10 ⊢ (𝜑 → 𝑊:𝐴⟶ℂ)
276	165	recnd 11239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → (log‘𝑤) ∈ ℂ)
277	276	negcld 11555	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑤 ∈ ℝ⁺) → -(log‘𝑤) ∈ ℂ)
278	277	fmpttd 7112	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)):ℝ⁺⟶ℂ)
279		fco 6739	. . . . . . . . . . 11 ⊢ (((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)):ℝ⁺⟶ℂ ∧ 𝐹:𝐴⟶ℝ⁺) → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
280	278, 2, 279	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
281	271, 275, 280, 1, 1, 48	off 7685	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹)):𝐴⟶ℂ)
282	281, 1, 160	fdmfifsupp 9370	. . . . . . . . 9 ⊢ (𝜑 → (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹)) finSupp 0)
283	73, 151, 1, 269, 281, 282	gsumsubmcl 19782	. . . . . . . 8 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) ∈ ℂ)
284	283	div1d 11979	. . . . . . 7 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1) = (ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))))
285		eqidd 2734	. . . . . . . . . 10 ⊢ (𝜑 → (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)))
286		fveq2 6889	. . . . . . . . . . 11 ⊢ (𝑤 = (𝐹‘𝑘) → (log‘𝑤) = (log‘(𝐹‘𝑘)))
287	286	negeqd 11451	. . . . . . . . . 10 ⊢ (𝑤 = (𝐹‘𝑘) → -(log‘𝑤) = -(log‘(𝐹‘𝑘)))
288	3, 138, 285, 287	fmptco 7124	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))
289	288	oveq2d 7422	. . . . . . . 8 ⊢ (𝜑 → (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘)))))
290	289	oveq2d 7422	. . . . . . 7 ⊢ (𝜑 → (ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
291	265, 284, 290	3eqtrd 2777	. . . . . 6 ⊢ (𝜑 → ((ℂ_fld Σ_g (𝑊 ∘_f · ((𝑤 ∈ ℝ⁺ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂ_fld Σ_g 𝑊)) = (ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
292	251, 264, 291	3brtr3d 5179	. . . . 5 ⊢ (𝜑 → -(log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))) ≤ (ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))))
293	149, 162, 292	lenegcon1d 11793	. . . 4 ⊢ (𝜑 → -(ℂ_fld Σ_g (𝑊 ∘_f · (𝑘 ∈ 𝐴 ↦ -(log‘(𝐹‘𝑘))))) ≤ (log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))))
294	130, 293	eqbrtrrd 5172	. . 3 ⊢ (𝜑 → (log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))) ≤ (log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))))
295	127	relogcld 26123	. . . 4 ⊢ (𝜑 → (log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))) ∈ ℝ)
296		efle 16058	. . . 4 ⊢ (((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, 149, 296	syl2anc 585	. . 3 ⊢ (𝜑 → ((log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊))) ≤ (log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))) ↔ (exp‘(log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)))) ≤ (exp‘(log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊))))))
298	294, 297	mpbid 231	. 2 ⊢ (𝜑 → (exp‘(log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)))) ≤ (exp‘(log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)))))
299	127	reeflogd 26124	. . 3 ⊢ (𝜑 → (exp‘(log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)))) = (𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)))
300	299	eqcomd 2739	. 2 ⊢ (𝜑 → (𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)) = (exp‘(log‘(𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)))))
301	148	reeflogd 26124	. . 3 ⊢ (𝜑 → (exp‘(log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)))) = (ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)))
302	301	eqcomd 2739	. 2 ⊢ (𝜑 → (ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)) = (exp‘(log‘(ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)))))
303	298, 300, 302	3brtr4d 5180	1 ⊢ (𝜑 → (𝑀 Σ_g (𝐹 ∘_f ↑_𝑐𝑊)) ≤ (ℂ_fld Σ_g (𝐹 ∘_f · 𝑊)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 Vcvv 3475 ∖ cdif 3945 ⊆ wss 3948 ∅c0 4322 {csn 4628 class class class wbr 5148 ↦ cmpt 5231 ↾ cres 5678 ∘ ccom 5680 ⟶wf 6537 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7406 ∘_f cof 7665 Fincfn 8936 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 + caddc 11110 · cmul 11112 +∞cpnf 11242 < clt 11245 ≤ cle 11246 − cmin 11441 -cneg 11442 / cdiv 11868 ℝ⁺crp 12971 (,)cioo 13321 [,)cico 13323 [,]cicc 13324 Σcsu 15629 expce 16002 Basecbs 17141 ↾_s cress 17170 0_gc0g 17382 Σ_g cgsu 17383 Mndcmnd 18622 MndHom cmhm 18666 SubMndcsubmnd 18667 SubGrpcsubg 18995 GrpHom cghm 19084 GrpIso cgim 19126 CMndccmn 19643 mulGrpcmgp 19982 Ringcrg 20050 CRingccrg 20051 DivRingcdr 20308 SubRingcsubrg 20352 ℂ_fldccnfld 20937 ℝ_fldcrefld 21149 logclog 26055 ↑_𝑐ccxp 26056

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-tpos 8208 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-ioc 13326 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-exp 14025 df-fac 14231 df-bc 14260 df-hash 14288 df-shft 15011 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-limsup 15412 df-clim 15429 df-rlim 15430 df-sum 15630 df-ef 16008 df-sin 16010 df-cos 16011 df-pi 16013 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-mhm 18668 df-submnd 18669 df-grp 18819 df-minusg 18820 df-mulg 18946 df-subg 18998 df-ghm 19085 df-gim 19128 df-cntz 19176 df-cmn 19645 df-abl 19646 df-mgp 19983 df-ur 20000 df-ring 20052 df-cring 20053 df-oppr 20143 df-dvdsr 20164 df-unit 20165 df-invr 20195 df-dvr 20208 df-drng 20310 df-subrg 20354 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-fbas 20934 df-fg 20935 df-cnfld 20938 df-refld 21150 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cls 22517 df-nei 22594 df-lp 22632 df-perf 22633 df-cn 22723 df-cnp 22724 df-haus 22811 df-cmp 22883 df-tx 23058 df-hmeo 23251 df-fil 23342 df-fm 23434 df-flim 23435 df-flf 23436 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-limc 25375 df-dv 25376 df-log 26057 df-cxp 26058

This theorem is referenced by: amgmlemALT 47804 amgmw2d 47805

W3C validator