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

Theorem amgmwlem 42409
Description: Weighted version of amgmlem 24414. (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 (𝐹𝑓𝑐𝑊)) ≤ (ℂfld Σg (𝐹𝑓 · 𝑊)))

Proof of Theorem amgmwlem
Dummy variables 𝑎 𝑏 𝑠 𝑢 𝑣 𝑘 𝑦 𝑤 𝑥 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 amgmwlem.1 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
2 amgmwlem.3 . . . . . . . . . . . 12 (𝜑𝐹:𝐴⟶ℝ+)
32ffvelrnda 6150 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
4 amgmwlem.4 . . . . . . . . . . . . 13 (𝜑𝑊:𝐴⟶ℝ+)
54ffvelrnda 6150 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
65rpred 11610 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ)
73, 6rpcxpcld 24174 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝐹𝑘)↑𝑐(𝑊𝑘)) ∈ ℝ+)
87relogcld 24071 . . . . . . . . 9 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℝ)
98recnd 9821 . . . . . . . 8 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℂ)
101, 9gsumfsum 19540 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))) = Σ𝑘𝐴 (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
112ffvelrnda 6150 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
124ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
1312rpred 11610 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ)
1411, 13rpcxpcld 24174 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝐹𝑘)↑𝑐(𝑊𝑘)) ∈ ℝ+)
1514relogcld 24071 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℝ)
1615recnd 9821 . . . . . . . . 9 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℂ)
1716negnegd 10132 . . . . . . . 8 ((𝜑𝑘𝐴) → --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
1817sumeq2dv 14145 . . . . . . 7 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = Σ𝑘𝐴 (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
192ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
204ffvelrnda 6150 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
2120rpred 11610 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ)
2219, 21rpcxpcld 24174 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → ((𝐹𝑘)↑𝑐(𝑊𝑘)) ∈ ℝ+)
2322relogcld 24071 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℝ)
2423renegcld 10206 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℝ)
2524recnd 9821 . . . . . . . . 9 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℂ)
261, 25fsumneg 14225 . . . . . . . 8 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
272ffvelrnda 6150 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
284ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
2928rpred 11610 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ)
3027, 29logcxpd 24175 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = ((𝑊𝑘) · (log‘(𝐹𝑘))))
3130negeqd 10024 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -((𝑊𝑘) · (log‘(𝐹𝑘))))
3231sumeq2dv 14145 . . . . . . . . 9 (𝜑 → Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))))
3332negeqd 10024 . . . . . . . 8 (𝜑 → -Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))))
344ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
3534rpcnd 11612 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℂ)
362ffvelrnda 6150 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
3736relogcld 24071 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℝ)
3837recnd 9821 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℂ)
3935, 38mulneg2d 10232 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝑊𝑘) · -(log‘(𝐹𝑘))) = -((𝑊𝑘) · (log‘(𝐹𝑘))))
4039eqcomd 2520 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -((𝑊𝑘) · (log‘(𝐹𝑘))) = ((𝑊𝑘) · -(log‘(𝐹𝑘))))
4140sumeq2dv 14145 . . . . . . . . 9 (𝜑 → Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
4241negeqd 10024 . . . . . . . 8 (𝜑 → -Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
4326, 33, 423eqtrd 2552 . . . . . . 7 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
4410, 18, 433eqtr2rd 2555 . . . . . 6 (𝜑 → -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))) = (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))))
454ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
46 negex 10028 . . . . . . . . . . 11 -(log‘(𝐹𝑘)) ∈ V
4746a1i 11 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ V)
484feqmptd 6042 . . . . . . . . . 10 (𝜑𝑊 = (𝑘𝐴 ↦ (𝑊𝑘)))
49 eqidd 2515 . . . . . . . . . 10 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))
501, 45, 47, 48, 49offval2 6686 . . . . . . . . 9 (𝜑 → (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) = (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘)))))
5150oveq2d 6441 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘))))))
524ffvelrnda 6150 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
5352rpcnd 11612 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℂ)
542ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
5554relogcld 24071 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℝ)
5655recnd 9821 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℂ)
5756negcld 10128 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℂ)
5853, 57mulcld 9813 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((𝑊𝑘) · -(log‘(𝐹𝑘))) ∈ ℂ)
591, 58gsumfsum 19540 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘))))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
6051, 59eqtrd 2548 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
6160negeqd 10024 . . . . . 6 (𝜑 → -(ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
62 relogf1o 24015 . . . . . . . . . 10 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
63 f1of 5933 . . . . . . . . . 10 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
6462, 63ax-mp 5 . . . . . . . . 9 (log ↾ ℝ+):ℝ+⟶ℝ
65 rpre 11577 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
6665anim2i 590 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
6766adantl 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
68 rpcxpcl 24120 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
6967, 68syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
70 inidm 3687 . . . . . . . . . 10 (𝐴𝐴) = 𝐴
7169, 2, 4, 1, 1, 70off 6684 . . . . . . . . 9 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
72 fcompt 6189 . . . . . . . . 9 (((log ↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊)) = (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹𝑓𝑐𝑊)‘𝑘))))
7364, 71, 72sylancr 693 . . . . . . . 8 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊)) = (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹𝑓𝑐𝑊)‘𝑘))))
74 rpre 11577 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
7574anim2i 590 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
7675adantl 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
77 rpcxpcl 24120 . . . . . . . . . . . . . 14 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
7876, 77syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
79 inidm 3687 . . . . . . . . . . . . 13 (𝐴𝐴) = 𝐴
8078, 2, 4, 1, 1, 79off 6684 . . . . . . . . . . . 12 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
8180ffvelrnda 6150 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝐹𝑓𝑐𝑊)‘𝑘) ∈ ℝ+)
82 fvres 6000 . . . . . . . . . . 11 (((𝐹𝑓𝑐𝑊)‘𝑘) ∈ ℝ+ → ((log ↾ ℝ+)‘((𝐹𝑓𝑐𝑊)‘𝑘)) = (log‘((𝐹𝑓𝑐𝑊)‘𝑘)))
8381, 82syl 17 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((log ↾ ℝ+)‘((𝐹𝑓𝑐𝑊)‘𝑘)) = (log‘((𝐹𝑓𝑐𝑊)‘𝑘)))
842ffnd 5844 . . . . . . . . . . . 12 (𝜑𝐹 Fn 𝐴)
854ffnd 5844 . . . . . . . . . . . 12 (𝜑𝑊 Fn 𝐴)
86 inidm 3687 . . . . . . . . . . . 12 (𝐴𝐴) = 𝐴
87 eqidd 2515 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝐹𝑘) = (𝐹𝑘))
88 eqidd 2515 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) = (𝑊𝑘))
8984, 85, 1, 1, 86, 87, 88ofval 6678 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝐹𝑓𝑐𝑊)‘𝑘) = ((𝐹𝑘)↑𝑐(𝑊𝑘)))
9089fveq2d 5990 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (log‘((𝐹𝑓𝑐𝑊)‘𝑘)) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
9183, 90eqtrd 2548 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((log ↾ ℝ+)‘((𝐹𝑓𝑐𝑊)‘𝑘)) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
9291mpteq2dva 4570 . . . . . . . 8 (𝜑 → (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹𝑓𝑐𝑊)‘𝑘))) = (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘)))))
9373, 92eqtrd 2548 . . . . . . 7 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊)) = (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘)))))
9493oveq2d 6441 . . . . . 6 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊))) = (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))))
9544, 61, 943eqtr4d 2558 . . . . 5 (𝜑 → -(ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊))))
96 amgmwlem.0 . . . . . . . . . . . . 13 𝑀 = (mulGrp‘ℂfld)
9796oveq1i 6435 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
9897rpmsubg 19537 . . . . . . . . . . 11 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
99 subgsubm 17335 . . . . . . . . . . 11 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
10098, 99ax-mp 5 . . . . . . . . . 10 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
101 cnring 19495 . . . . . . . . . . 11 fld ∈ Ring
102 cnfldbas 19479 . . . . . . . . . . . . 13 ℂ = (Base‘ℂfld)
103 cnfld0 19497 . . . . . . . . . . . . 13 0 = (0g‘ℂfld)
104 cndrng 19502 . . . . . . . . . . . . 13 fld ∈ DivRing
105102, 103, 104drngui 18487 . . . . . . . . . . . 12 (ℂ ∖ {0}) = (Unit‘ℂfld)
106105, 96unitsubm 18404 . . . . . . . . . . 11 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
107 eqid 2514 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
108107subsubm 17076 . . . . . . . . . . 11 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
109101, 106, 108mp2b 10 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
110100, 109mpbi 218 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
111110simpli 472 . . . . . . . 8 + ∈ (SubMnd‘𝑀)
112 eqid 2514 . . . . . . . . 9 (𝑀s+) = (𝑀s+)
113112submbas 17074 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ = (Base‘(𝑀s+)))
114111, 113ax-mp 5 . . . . . . 7 + = (Base‘(𝑀s+))
115 cnfld1 19498 . . . . . . . . 9 1 = (1r‘ℂfld)
11696, 115ringidval 18237 . . . . . . . 8 1 = (0g𝑀)
11796oveq1i 6435 . . . . . . . . . . . . 13 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
118117rpmsubg 19537 . . . . . . . . . . . 12 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
119 subgsubm 17335 . . . . . . . . . . . 12 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
120118, 119ax-mp 5 . . . . . . . . . . 11 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
121102, 103, 104drngui 18487 . . . . . . . . . . . . 13 (ℂ ∖ {0}) = (Unit‘ℂfld)
122121, 96unitsubm 18404 . . . . . . . . . . . 12 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
123 eqid 2514 . . . . . . . . . . . . 13 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
124123subsubm 17076 . . . . . . . . . . . 12 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
125101, 122, 124mp2b 10 . . . . . . . . . . 11 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
126120, 125mpbi 218 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
127126simpli 472 . . . . . . . . 9 + ∈ (SubMnd‘𝑀)
128 eqid 2514 . . . . . . . . . 10 (𝑀s+) = (𝑀s+)
129 eqid 2514 . . . . . . . . . 10 (0g𝑀) = (0g𝑀)
130128, 129subm0 17075 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) → (0g𝑀) = (0g‘(𝑀s+)))
131127, 130ax-mp 5 . . . . . . . 8 (0g𝑀) = (0g‘(𝑀s+))
132116, 131eqtri 2536 . . . . . . 7 1 = (0g‘(𝑀s+))
133 cncrng 19494 . . . . . . . . 9 fld ∈ CRing
13496crngmgp 18289 . . . . . . . . 9 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
135133, 134mp1i 13 . . . . . . . 8 (𝜑𝑀 ∈ CMnd)
13696oveq1i 6435 . . . . . . . . . . . . 13 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
137136rpmsubg 19537 . . . . . . . . . . . 12 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
138 subgsubm 17335 . . . . . . . . . . . 12 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
139137, 138ax-mp 5 . . . . . . . . . . 11 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
140102, 103, 104drngui 18487 . . . . . . . . . . . . 13 (ℂ ∖ {0}) = (Unit‘ℂfld)
141140, 96unitsubm 18404 . . . . . . . . . . . 12 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
142 eqid 2514 . . . . . . . . . . . . 13 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
143142subsubm 17076 . . . . . . . . . . . 12 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
144101, 141, 143mp2b 10 . . . . . . . . . . 11 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
145139, 144mpbi 218 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
146145simpli 472 . . . . . . . . 9 + ∈ (SubMnd‘𝑀)
147 eqid 2514 . . . . . . . . . 10 (𝑀s+) = (𝑀s+)
148147submmnd 17073 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀s+) ∈ Mnd)
149146, 148mp1i 13 . . . . . . . 8 (𝜑 → (𝑀s+) ∈ Mnd)
150 eqid 2514 . . . . . . . . 9 (𝑀s+) = (𝑀s+)
151150subcmn 17976 . . . . . . . 8 ((𝑀 ∈ CMnd ∧ (𝑀s+) ∈ Mnd) → (𝑀s+) ∈ CMnd)
152135, 149, 151syl2anc 690 . . . . . . 7 (𝜑 → (𝑀s+) ∈ CMnd)
153 resubdrg 19683 . . . . . . . . . 10 (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
154153simpli 472 . . . . . . . . 9 ℝ ∈ (SubRing‘ℂfld)
155 df-refld 19680 . . . . . . . . . 10 fld = (ℂflds ℝ)
156155subrgring 18517 . . . . . . . . 9 (ℝ ∈ (SubRing‘ℂfld) → ℝfld ∈ Ring)
157154, 156ax-mp 5 . . . . . . . 8 fld ∈ Ring
158 ringmnd 18290 . . . . . . . 8 (ℝfld ∈ Ring → ℝfld ∈ Mnd)
159157, 158mp1i 13 . . . . . . 7 (𝜑 → ℝfld ∈ Mnd)
16096oveq1i 6435 . . . . . . . . . 10 (𝑀s+) = ((mulGrp‘ℂfld) ↾s+)
161160reloggim 24047 . . . . . . . . 9 (log ↾ ℝ+) ∈ ((𝑀s+) GrpIso ℝfld)
162 gimghm 17425 . . . . . . . . 9 ((log ↾ ℝ+) ∈ ((𝑀s+) GrpIso ℝfld) → (log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld))
163161, 162ax-mp 5 . . . . . . . 8 (log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld)
164 ghmmhm 17389 . . . . . . . 8 ((log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld) → (log ↾ ℝ+) ∈ ((𝑀s+) MndHom ℝfld))
165163, 164mp1i 13 . . . . . . 7 (𝜑 → (log ↾ ℝ+) ∈ ((𝑀s+) MndHom ℝfld))
166 rpre 11577 . . . . . . . . . . 11 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
167166anim2i 590 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
168167adantl 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
169 rpcxpcl 24120 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
170168, 169syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
171 inidm 3687 . . . . . . . 8 (𝐴𝐴) = 𝐴
172170, 2, 4, 1, 1, 171off 6684 . . . . . . 7 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
173 rpre 11577 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
174173anim2i 590 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
175174adantl 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
176 rpcxpcl 24120 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
177175, 176syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
178 inidm 3687 . . . . . . . . 9 (𝐴𝐴) = 𝐴
179177, 2, 4, 1, 1, 178off 6684 . . . . . . . 8 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
180 1red 9808 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
181179, 1, 180fdmfifsupp 8042 . . . . . . 7 (𝜑 → (𝐹𝑓𝑐𝑊) finSupp 1)
182114, 132, 152, 159, 1, 165, 172, 181gsummhm 18072 . . . . . 6 (𝜑 → (ℝfld Σg ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊))) = ((log ↾ ℝ+)‘((𝑀s+) Σg (𝐹𝑓𝑐𝑊))))
183153simpli 472 . . . . . . . . . 10 ℝ ∈ (SubRing‘ℂfld)
184 subrgsubg 18520 . . . . . . . . . 10 (ℝ ∈ (SubRing‘ℂfld) → ℝ ∈ (SubGrp‘ℂfld))
185183, 184ax-mp 5 . . . . . . . . 9 ℝ ∈ (SubGrp‘ℂfld)
186 subgsubm 17335 . . . . . . . . 9 (ℝ ∈ (SubGrp‘ℂfld) → ℝ ∈ (SubMnd‘ℂfld))
187185, 186ax-mp 5 . . . . . . . 8 ℝ ∈ (SubMnd‘ℂfld)
188187a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ (SubMnd‘ℂfld))
189 f1of 5933 . . . . . . . . 9 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
19062, 189mp1i 13 . . . . . . . 8 (𝜑 → (log ↾ ℝ+):ℝ+⟶ℝ)
191 rpre 11577 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
192191anim2i 590 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
193192adantl 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
194 rpcxpcl 24120 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
195193, 194syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
196 inidm 3687 . . . . . . . . 9 (𝐴𝐴) = 𝐴
197195, 2, 4, 1, 1, 196off 6684 . . . . . . . 8 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
198 fco 5856 . . . . . . . 8 (((log ↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊)):𝐴⟶ℝ)
199190, 197, 198syl2anc 690 . . . . . . 7 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊)):𝐴⟶ℝ)
2001, 188, 199, 155gsumsubm 17092 . . . . . 6 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊))) = (ℝfld Σg ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊))))
20196oveq1i 6435 . . . . . . . . . . . . 13 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
202201rpmsubg 19537 . . . . . . . . . . . 12 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
203 subgsubm 17335 . . . . . . . . . . . 12 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
204202, 203ax-mp 5 . . . . . . . . . . 11 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
205102, 103, 104drngui 18487 . . . . . . . . . . . . 13 (ℂ ∖ {0}) = (Unit‘ℂfld)
206205, 96unitsubm 18404 . . . . . . . . . . . 12 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
207 eqid 2514 . . . . . . . . . . . . 13 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
208207subsubm 17076 . . . . . . . . . . . 12 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
209101, 206, 208mp2b 10 . . . . . . . . . . 11 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
210204, 209mpbi 218 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
211210simpli 472 . . . . . . . . 9 + ∈ (SubMnd‘𝑀)
212211a1i 11 . . . . . . . 8 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
213 rpre 11577 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
214213anim2i 590 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
215214adantl 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
216 rpcxpcl 24120 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
217215, 216syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
218 inidm 3687 . . . . . . . . 9 (𝐴𝐴) = 𝐴
219217, 2, 4, 1, 1, 218off 6684 . . . . . . . 8 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
220 eqid 2514 . . . . . . . 8 (𝑀s+) = (𝑀s+)
2211, 212, 219, 220gsumsubm 17092 . . . . . . 7 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐𝑊)) = ((𝑀s+) Σg (𝐹𝑓𝑐𝑊)))
222221fveq2d 5990 . . . . . 6 (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹𝑓𝑐𝑊))) = ((log ↾ ℝ+)‘((𝑀s+) Σg (𝐹𝑓𝑐𝑊))))
223182, 200, 2223eqtr4d 2558 . . . . 5 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹𝑓𝑐𝑊))) = ((log ↾ ℝ+)‘(𝑀 Σg (𝐹𝑓𝑐𝑊))))
22496, 115ringidval 18237 . . . . . . 7 1 = (0g𝑀)
22596crngmgp 18289 . . . . . . . 8 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
226133, 225mp1i 13 . . . . . . 7 (𝜑𝑀 ∈ CMnd)
22796oveq1i 6435 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
228227rpmsubg 19537 . . . . . . . . . . 11 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
229 subgsubm 17335 . . . . . . . . . . 11 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
230228, 229ax-mp 5 . . . . . . . . . 10 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
231102, 103, 104drngui 18487 . . . . . . . . . . . 12 (ℂ ∖ {0}) = (Unit‘ℂfld)
232231, 96unitsubm 18404 . . . . . . . . . . 11 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
233 eqid 2514 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
234233subsubm 17076 . . . . . . . . . . 11 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
235101, 232, 234mp2b 10 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
236230, 235mpbi 218 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
237236simpli 472 . . . . . . . 8 + ∈ (SubMnd‘𝑀)
238237a1i 11 . . . . . . 7 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
239 rpre 11577 . . . . . . . . . . 11 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
240239anim2i 590 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
241240adantl 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
242 rpcxpcl 24120 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
243241, 242syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
244 inidm 3687 . . . . . . . 8 (𝐴𝐴) = 𝐴
245243, 2, 4, 1, 1, 244off 6684 . . . . . . 7 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
246 rpre 11577 . . . . . . . . . . . 12 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
247246anim2i 590 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
248247adantl 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
249 rpcxpcl 24120 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
250248, 249syl 17 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
251 inidm 3687 . . . . . . . . 9 (𝐴𝐴) = 𝐴
252250, 2, 4, 1, 1, 251off 6684 . . . . . . . 8 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
253 1red 9808 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
254252, 1, 253fdmfifsupp 8042 . . . . . . 7 (𝜑 → (𝐹𝑓𝑐𝑊) finSupp 1)
255224, 226, 1, 238, 245, 254gsumsubmcl 18053 . . . . . 6 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐𝑊)) ∈ ℝ+)
256 fvres 6000 . . . . . 6 ((𝑀 Σg (𝐹𝑓𝑐𝑊)) ∈ ℝ+ → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹𝑓𝑐𝑊))) = (log‘(𝑀 Σg (𝐹𝑓𝑐𝑊))))
257255, 256syl 17 . . . . 5 (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹𝑓𝑐𝑊))) = (log‘(𝑀 Σg (𝐹𝑓𝑐𝑊))))
25895, 223, 2573eqtrd 2552 . . . 4 (𝜑 → -(ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (log‘(𝑀 Σg (𝐹𝑓𝑐𝑊))))
259 simprl 789 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
260259rpcnd 11612 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
261 simprr 791 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
262261rpcnd 11612 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
263260, 262mulcomd 9814 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
2641, 4, 2, 263caofcom 6701 . . . . . . . 8 (𝜑 → (𝑊𝑓 · 𝐹) = (𝐹𝑓 · 𝑊))
265264oveq2d 6441 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝐹𝑓 · 𝑊)))
2664ffvelrnda 6150 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
2672ffvelrnda 6150 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
2684feqmptd 6042 . . . . . . . . . . 11 (𝜑𝑊 = (𝑘𝐴 ↦ (𝑊𝑘)))
2692feqmptd 6042 . . . . . . . . . . 11 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
2701, 266, 267, 268, 269offval2 6686 . . . . . . . . . 10 (𝜑 → (𝑊𝑓 · 𝐹) = (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘))))
271270oveq2d 6441 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))))
2724ffvelrnda 6150 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
2732ffvelrnda 6150 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
274272, 273rpmulcld 11626 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
275274rpcnd 11612 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℂ)
2761, 275gsumfsum 19540 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
277271, 276eqtrd 2548 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
278 amgmwlem.2 . . . . . . . . 9 (𝜑𝐴 ≠ ∅)
2794ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
2802ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
281279, 280rpmulcld 11626 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
2821, 278, 281fsumrpcl 14179 . . . . . . . 8 (𝜑 → Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
283277, 282eqeltrd 2592 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) ∈ ℝ+)
284265, 283eqeltrrd 2593 . . . . . 6 (𝜑 → (ℂfld Σg (𝐹𝑓 · 𝑊)) ∈ ℝ+)
285284relogcld 24071 . . . . 5 (𝜑 → (log‘(ℂfld Σg (𝐹𝑓 · 𝑊))) ∈ ℝ)
286 ringcmn 18315 . . . . . . 7 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
287101, 286mp1i 13 . . . . . 6 (𝜑 → ℂfld ∈ CMnd)
288153simpli 472 . . . . . . . . 9 ℝ ∈ (SubRing‘ℂfld)
289 subrgsubg 18520 . . . . . . . . 9 (ℝ ∈ (SubRing‘ℂfld) → ℝ ∈ (SubGrp‘ℂfld))
290288, 289ax-mp 5 . . . . . . . 8 ℝ ∈ (SubGrp‘ℂfld)
291 subgsubm 17335 . . . . . . . 8 (ℝ ∈ (SubGrp‘ℂfld) → ℝ ∈ (SubMnd‘ℂfld))
292290, 291ax-mp 5 . . . . . . 7 ℝ ∈ (SubMnd‘ℂfld)
293292a1i 11 . . . . . 6 (𝜑 → ℝ ∈ (SubMnd‘ℂfld))
294 remulcl 9774 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
295294adantl 480 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
296 rpssre 11581 . . . . . . . 8 + ⊆ ℝ
297 fss 5854 . . . . . . . 8 ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ ℝ) → 𝑊:𝐴⟶ℝ)
2984, 296, 297sylancl 692 . . . . . . 7 (𝜑𝑊:𝐴⟶ℝ)
2992ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
300299relogcld 24071 . . . . . . . . 9 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℝ)
301300renegcld 10206 . . . . . . . 8 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℝ)
302 eqid 2514 . . . . . . . 8 (𝑘𝐴 ↦ -(log‘(𝐹𝑘))) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))
303301, 302fmptd 6175 . . . . . . 7 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))):𝐴⟶ℝ)
304 inidm 3687 . . . . . . 7 (𝐴𝐴) = 𝐴
305295, 298, 303, 1, 1, 304off 6684 . . . . . 6 (𝜑 → (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))):𝐴⟶ℝ)
306 remulcl 9774 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
307306adantl 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
308 fss 5854 . . . . . . . . 9 ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ ℝ) → 𝑊:𝐴⟶ℝ)
3094, 296, 308sylancl 692 . . . . . . . 8 (𝜑𝑊:𝐴⟶ℝ)
3102ffvelrnda 6150 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
311310relogcld 24071 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℝ)
312311renegcld 10206 . . . . . . . . 9 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℝ)
313 eqid 2514 . . . . . . . . 9 (𝑘𝐴 ↦ -(log‘(𝐹𝑘))) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))
314312, 313fmptd 6175 . . . . . . . 8 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))):𝐴⟶ℝ)
315 inidm 3687 . . . . . . . 8 (𝐴𝐴) = 𝐴
316307, 309, 314, 1, 1, 315off 6684 . . . . . . 7 (𝜑 → (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))):𝐴⟶ℝ)
317 0red 9794 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
318316, 1, 317fdmfifsupp 8042 . . . . . 6 (𝜑 → (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) finSupp 0)
319103, 287, 1, 293, 305, 318gsumsubmcl 18053 . . . . 5 (𝜑 → (ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) ∈ ℝ)
320296a1i 11 . . . . . . . 8 (𝜑 → ℝ+ ⊆ ℝ)
321 simpr 475 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
322321relogcld 24071 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
323322renegcld 10206 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℝ)
324 eqid 2514 . . . . . . . . 9 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
325323, 324fmptd 6175 . . . . . . . 8 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℝ)
326 simpl 471 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ ℝ+)
327 ioorp 11987 . . . . . . . . . . . 12 (0(,)+∞) = ℝ+
328326, 327syl6eleqr 2603 . . . . . . . . . . 11 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ (0(,)+∞))
329 simpr 475 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ ℝ+)
330329, 327syl6eleqr 2603 . . . . . . . . . . 11 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ (0(,)+∞))
331 iccssioo2 11982 . . . . . . . . . . 11 ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
332328, 330, 331syl2anc 690 . . . . . . . . . 10 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
333332, 327syl6sseq 3518 . . . . . . . . 9 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ ℝ+)
334333adantl 480 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → (𝑎[,]𝑏) ⊆ ℝ+)
335 ioossico 11998 . . . . . . . . . 10 (0(,)+∞) ⊆ (0[,)+∞)
336327, 335eqsstr3i 3503 . . . . . . . . 9 + ⊆ (0[,)+∞)
337 fss 5854 . . . . . . . . 9 ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ (0[,)+∞)) → 𝑊:𝐴⟶(0[,)+∞))
3384, 336, 337sylancl 692 . . . . . . . 8 (𝜑𝑊:𝐴⟶(0[,)+∞))
339 0lt1 10297 . . . . . . . . 9 0 < 1
340 amgmwlem.5 . . . . . . . . 9 (𝜑 → (ℂfld Σg 𝑊) = 1)
341339, 340syl5breqr 4519 . . . . . . . 8 (𝜑 → 0 < (ℂfld Σg 𝑊))
342296a1i 11 . . . . . . . . 9 (𝜑 → ℝ+ ⊆ ℝ)
343 simpr 475 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
344343relogcld 24071 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
345344renegcld 10206 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℝ)
346 eqid 2514 . . . . . . . . . 10 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
347345, 346fmptd 6175 . . . . . . . . 9 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℝ)
348 simpl 471 . . . . . . . . . . . . 13 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ ℝ+)
349348, 327syl6eleqr 2603 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ (0(,)+∞))
350 simpr 475 . . . . . . . . . . . . 13 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ ℝ+)
351350, 327syl6eleqr 2603 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ (0(,)+∞))
352 iccssioo2 11982 . . . . . . . . . . . 12 ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
353349, 351, 352syl2anc 690 . . . . . . . . . . 11 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
354353, 327syl6sseq 3518 . . . . . . . . . 10 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ ℝ+)
355354adantl 480 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → (𝑎[,]𝑏) ⊆ ℝ+)
356 logccv 24107 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
3573563adant1 1071 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
358 elioore 11941 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
3593583ad2ant3 1076 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
360 simp21 1086 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
361360relogcld 24071 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
362359, 361remulcld 9823 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
363 1red 9808 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
364 elioore 11941 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
365363, 364resubcld 10207 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
3663653ad2ant3 1076 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
367 simp22 1087 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
368367relogcld 24071 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
369366, 368remulcld 9823 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
370362, 369readdcld 9822 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ)
371 elioore 11941 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
372 eliooord 11969 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
373372simpld 473 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 0 < 𝑡)
374371, 373elrpd 11607 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ+)
3753743ad2ant3 1076 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ+)
376 simp21 1086 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
377375, 376rpmulcld 11626 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · 𝑥) ∈ ℝ+)
378 1red 9808 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
379 elioore 11941 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
380378, 379resubcld 10207 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
381 elioore 11941 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
382 1red 9808 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
383 0red 9794 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
384 eliooord 11969 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
385384simprd 477 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (0(,)1) → 𝑡 < 1)
386 1m0e1 10884 . . . . . . . . . . . . . . . . . . 19 (1 − 0) = 1
387385, 386syl6breqr 4523 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
388381, 382, 383, 387ltsub13d 10380 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
389380, 388elrpd 11607 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ+)
3903893ad2ant3 1076 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ+)
391 simp22 1087 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
392390, 391rpmulcld 11626 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · 𝑦) ∈ ℝ+)
393 rpaddcl 11592 . . . . . . . . . . . . . 14 (((𝑡 · 𝑥) ∈ ℝ+ ∧ ((1 − 𝑡) · 𝑦) ∈ ℝ+) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
394377, 392, 393syl2anc 690 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
395394relogcld 24071 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ)
396370, 395ltnegd 10352 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))))
397357, 396mpbid 220 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
398 eqidd 2515 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
399 fveq2 5986 . . . . . . . . . . . . 13 (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
400399adantl 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
401400negeqd 10024 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
402 elioore 11941 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
403 eliooord 11969 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
404403simpld 473 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → 0 < 𝑡)
405402, 404elrpd 11607 . . . . . . . . . . . . . 14 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ+)
4064053ad2ant3 1076 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ+)
407 simp21 1086 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
408406, 407rpmulcld 11626 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · 𝑥) ∈ ℝ+)
409 1red 9808 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
410 elioore 11941 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
411409, 410resubcld 10207 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
412 elioore 11941 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
413 1red 9808 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
414 0red 9794 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
415 eliooord 11969 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
416415simprd 477 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 𝑡 < 1)
417416, 386syl6breqr 4523 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
418412, 413, 414, 417ltsub13d 10380 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
419411, 418elrpd 11607 . . . . . . . . . . . . . 14 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ+)
4204193ad2ant3 1076 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ+)
421 simp22 1087 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
422420, 421rpmulcld 11626 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · 𝑦) ∈ ℝ+)
423 rpaddcl 11592 . . . . . . . . . . . 12 (((𝑡 · 𝑥) ∈ ℝ+ ∧ ((1 − 𝑡) · 𝑦) ∈ ℝ+) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
424408, 422, 423syl2anc 690 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
425 negex 10028 . . . . . . . . . . . 12 -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V
426425a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V)
427398, 401, 424, 426fvmptd 6080 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
428 simp21 1086 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
429 fveq2 5986 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥))
430429negeqd 10024 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥))
431 eqid 2514 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
432 negex 10028 . . . . . . . . . . . . . . . 16 -(log‘𝑤) ∈ V
433430, 431, 432fvmpt3i 6079 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
434428, 433syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
435434oveq2d 6441 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥)))
436 elioore 11941 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
4374363ad2ant3 1076 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
438437recnd 9821 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
439 simp21 1086 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
440439relogcld 24071 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
441440recnd 9821 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℂ)
442438, 441mulneg2d 10232 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥)))
443435, 442eqtrd 2548 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥)))
444 simp22 1087 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
445 fveq2 5986 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦))
446445negeqd 10024 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦))
447 eqid 2514 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
448 negex 10028 . . . . . . . . . . . . . . . 16 -(log‘𝑤) ∈ V
449446, 447, 448fvmpt3i 6079 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
450444, 449syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
451450oveq2d 6441 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦)))
452 1red 9808 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
453 elioore 11941 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
454452, 453resubcld 10207 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
455 elioore 11941 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
456 1red 9808 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
457 0red 9794 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
458 eliooord 11969 . . . . . . . . . . . . . . . . . . . 20 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
459458simprd 477 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (0(,)1) → 𝑡 < 1)
460459, 386syl6breqr 4523 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
461455, 456, 457, 460ltsub13d 10380 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
462454, 461elrpd 11607 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ+)
4634623ad2ant3 1076 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ+)
464463rpcnd 11612 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
465 simp22 1087 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
466465relogcld 24071 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
467466recnd 9821 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℂ)
468464, 467mulneg2d 10232 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
469451, 468eqtrd 2548 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
470443, 469oveq12d 6443 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
471 elioore 11941 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
4724713ad2ant3 1076 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
473 simp21 1086 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
474473relogcld 24071 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
475472, 474remulcld 9823 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
476475recnd 9821 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ)
477 1red 9808 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
478 elioore 11941 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
479477, 478resubcld 10207 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
4804793ad2ant3 1076 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
481 simp22 1087 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
482481relogcld 24071 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
483480, 482remulcld 9823 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
484483recnd 9821 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℂ)
485476, 484negdid 10154 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
486470, 485eqtr4d 2551 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
487397, 427, 4863brtr4d 4513 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))))
488342, 347, 355, 487scvxcvx 24410 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ ℝ+𝑣 ∈ ℝ+𝑠 ∈ (0[,]1))) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑣))))
489320, 325, 334, 1, 338, 2, 341, 488jensen 24413 . . . . . . 7 (𝜑 → (((ℂfld Σg (𝑊𝑓 · 𝐹)) / (ℂfld Σg 𝑊)) ∈ ℝ+ ∧ ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊𝑓 · 𝐹)) / (ℂfld Σg 𝑊))) ≤ ((ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊))))
490489simprd 477 . . . . . 6 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊𝑓 · 𝐹)) / (ℂfld Σg 𝑊))) ≤ ((ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)))
491340oveq2d 6441 . . . . . . . 8 (𝜑 → ((ℂfld Σg (𝑊𝑓 · 𝐹)) / (ℂfld Σg 𝑊)) = ((ℂfld Σg (𝑊𝑓 · 𝐹)) / 1))
492491fveq2d 5990 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊𝑓 · 𝐹)) / (ℂfld Σg 𝑊))) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊𝑓 · 𝐹)) / 1)))
4934ffvelrnda 6150 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
4942ffvelrnda 6150 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
4954feqmptd 6042 . . . . . . . . . . . . . 14 (𝜑𝑊 = (𝑘𝐴 ↦ (𝑊𝑘)))
4962feqmptd 6042 . . . . . . . . . . . . . 14 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
4971, 493, 494, 495, 496offval2 6686 . . . . . . . . . . . . 13 (𝜑 → (𝑊𝑓 · 𝐹) = (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘))))
498497oveq2d 6441 . . . . . . . . . . . 12 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))))
4994ffvelrnda 6150 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
5002ffvelrnda 6150 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
501499, 500rpmulcld 11626 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
502501rpcnd 11612 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℂ)
5031, 502gsumfsum 19540 . . . . . . . . . . . 12 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
504498, 503eqtrd 2548 . . . . . . . . . . 11 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
5054ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
5062ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
507505, 506rpmulcld 11626 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
5081, 278, 507fsumrpcl 14179 . . . . . . . . . . 11 (𝜑 → Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
509504, 508eqeltrd 2592 . . . . . . . . . 10 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) ∈ ℝ+)
510509rpcnd 11612 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) ∈ ℂ)
511510div1d 10540 . . . . . . . 8 (𝜑 → ((ℂfld Σg (𝑊𝑓 · 𝐹)) / 1) = (ℂfld Σg (𝑊𝑓 · 𝐹)))
512511fveq2d 5990 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊𝑓 · 𝐹)) / 1)) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊𝑓 · 𝐹))))
5134ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
5142ffvelrnda 6150 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
5154feqmptd 6042 . . . . . . . . . . . . 13 (𝜑𝑊 = (𝑘𝐴 ↦ (𝑊𝑘)))
5162feqmptd 6042 . . . . . . . . . . . . 13 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
5171, 513, 514, 515, 516offval2 6686 . . . . . . . . . . . 12 (𝜑 → (𝑊𝑓 · 𝐹) = (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘))))
518517oveq2d 6441 . . . . . . . . . . 11 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))))
5194ffvelrnda 6150 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
5202ffvelrnda 6150 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
521519, 520rpmulcld 11626 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
522521rpcnd 11612 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℂ)
5231, 522gsumfsum 19540 . . . . . . . . . . 11 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
524518, 523eqtrd 2548 . . . . . . . . . 10 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
5254ffvelrnda 6150 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
5262ffvelrnda 6150 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
527525, 526rpmulcld 11626 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
5281, 278, 527fsumrpcl 14179 . . . . . . . . . 10 (𝜑 → Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
529524, 528eqeltrd 2592 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) ∈ ℝ+)
530 fveq2 5986 . . . . . . . . . . 11 (𝑤 = (ℂfld Σg (𝑊𝑓 · 𝐹)) → (log‘𝑤) = (log‘(ℂfld Σg (𝑊𝑓 · 𝐹))))
531530negeqd 10024 . . . . . . . . . 10 (𝑤 = (ℂfld Σg (𝑊𝑓 · 𝐹)) → -(log‘𝑤) = -(log‘(ℂfld Σg (𝑊𝑓 · 𝐹))))
532 eqid 2514 . . . . . . . . . 10 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
533 negex 10028 . . . . . . . . . 10 -(log‘𝑤) ∈ V
534531, 532, 533fvmpt3i 6079 . . . . . . . . 9 ((ℂfld Σg (𝑊𝑓 · 𝐹)) ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊𝑓 · 𝐹))) = -(log‘(ℂfld Σg (𝑊𝑓 · 𝐹))))
535529, 534syl 17 . . . . . . . 8 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊𝑓 · 𝐹))) = -(log‘(ℂfld Σg (𝑊𝑓 · 𝐹))))
536 simprl 789 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
537536rpcnd 11612 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
538 simprr 791 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
539538rpcnd 11612 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
540537, 539mulcomd 9814 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
5411, 4, 2, 540caofcom 6701 . . . . . . . . . . 11 (𝜑 → (𝑊𝑓 · 𝐹) = (𝐹𝑓 · 𝑊))
542541oveq2d 6441 . . . . . . . . . 10 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝐹𝑓 · 𝑊)))
543542fveq2d 5990 . . . . . . . . 9 (𝜑 → (log‘(ℂfld Σg (𝑊𝑓 · 𝐹))) = (log‘(ℂfld Σg (𝐹𝑓 · 𝑊))))
544543negeqd 10024 . . . . . . . 8 (𝜑 → -(log‘(ℂfld Σg (𝑊𝑓 · 𝐹))) = -(log‘(ℂfld Σg (𝐹𝑓 · 𝑊))))
545535, 544eqtrd 2548 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊𝑓 · 𝐹))) = -(log‘(ℂfld Σg (𝐹𝑓 · 𝑊))))
546492, 512, 5453eqtrd 2552 . . . . . 6 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊𝑓 · 𝐹)) / (ℂfld Σg 𝑊))) = -(log‘(ℂfld Σg (𝐹𝑓 · 𝑊))))
547340oveq2d 6441 . . . . . . 7 (𝜑 → ((ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)) = ((ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1))
548 ringcmn 18315 . . . . . . . . . 10 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
549101, 548mp1i 13 . . . . . . . . 9 (𝜑 → ℂfld ∈ CMnd)
550 ringmnd 18290 . . . . . . . . . . 11 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
551101, 550ax-mp 5 . . . . . . . . . 10 fld ∈ Mnd
552102submid 17070 . . . . . . . . . 10 (ℂfld ∈ Mnd → ℂ ∈ (SubMnd‘ℂfld))
553551, 552mp1i 13 . . . . . . . . 9 (𝜑 → ℂ ∈ (SubMnd‘ℂfld))
554 mulcl 9773 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
555554adantl 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
556 rpcn 11579 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
557556ssriv 3476 . . . . . . . . . . . 12 + ⊆ ℂ
558557a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ+ ⊆ ℂ)
5594, 558fssd 5855 . . . . . . . . . 10 (𝜑𝑊:𝐴⟶ℂ)
560 simpr 475 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
561560relogcld 24071 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
562561recnd 9821 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℂ)
563562negcld 10128 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℂ)
564 eqid 2514 . . . . . . . . . . . 12 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
565563, 564fmptd 6175 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ)
566 fco 5856 . . . . . . . . . . 11 (((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ ∧ 𝐹:𝐴⟶ℝ+) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
567565, 2, 566syl2anc 690 . . . . . . . . . 10 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
568 inidm 3687 . . . . . . . . . 10 (𝐴𝐴) = 𝐴
569555, 559, 567, 1, 1, 568off 6684 . . . . . . . . 9 (𝜑 → (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)):𝐴⟶ℂ)
570 mulcl 9773 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
571570adantl 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
572 rpcn 11579 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
573572ssriv 3476 . . . . . . . . . . . . 13 + ⊆ ℂ
574573a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ+ ⊆ ℂ)
5754, 574fssd 5855 . . . . . . . . . . 11 (𝜑𝑊:𝐴⟶ℂ)
576 simpr 475 . . . . . . . . . . . . . . . 16 ((𝜑𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
577576relogcld 24071 . . . . . . . . . . . . . . 15 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
578577recnd 9821 . . . . . . . . . . . . . 14 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℂ)
579578negcld 10128 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℂ)
580 eqid 2514 . . . . . . . . . . . . 13 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
581579, 580fmptd 6175 . . . . . . . . . . . 12 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ)
582 fco 5856 . . . . . . . . . . . 12 (((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ ∧ 𝐹:𝐴⟶ℝ+) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
583581, 2, 582syl2anc 690 . . . . . . . . . . 11 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
584 inidm 3687 . . . . . . . . . . 11 (𝐴𝐴) = 𝐴
585571, 575, 583, 1, 1, 584off 6684 . . . . . . . . . 10 (𝜑 → (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)):𝐴⟶ℂ)
586 0red 9794 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
587585, 1, 586fdmfifsupp 8042 . . . . . . . . 9 (𝜑 → (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) finSupp 0)
588103, 549, 1, 553, 569, 587gsumsubmcl 18053 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) ∈ ℂ)
589588div1d 10540 . . . . . . 7 (𝜑 → ((ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1) = (ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))))
5902ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
5912feqmptd 6042 . . . . . . . . . 10 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
592 eqidd 2515 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
593 fveq2 5986 . . . . . . . . . . 11 (𝑤 = (𝐹𝑘) → (log‘𝑤) = (log‘(𝐹𝑘)))
594593negeqd 10024 . . . . . . . . . 10 (𝑤 = (𝐹𝑘) → -(log‘𝑤) = -(log‘(𝐹𝑘)))
595590, 591, 592, 594fmptco 6186 . . . . . . . . 9 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))
596595oveq2d 6441 . . . . . . . 8 (𝜑 → (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))))
597596oveq2d 6441 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
598547, 589, 5973eqtrd 2552 . . . . . 6 (𝜑 → ((ℂfld Σg (𝑊𝑓 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)) = (ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
599490, 546, 5983brtr3d 4512 . . . . 5 (𝜑 → -(log‘(ℂfld Σg (𝐹𝑓 · 𝑊))) ≤ (ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
600285, 319, 599lenegcon1d 10356 . . . 4 (𝜑 → -(ℂfld Σg (𝑊𝑓 · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) ≤ (log‘(ℂfld Σg (𝐹𝑓 · 𝑊))))
601258, 600eqbrtrrd 4505 . . 3 (𝜑 → (log‘(𝑀 Σg (𝐹𝑓𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹𝑓 · 𝑊))))
60296, 115ringidval 18237 . . . . . 6 1 = (0g𝑀)
60396crngmgp 18289 . . . . . . 7 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
604133, 603mp1i 13 . . . . . 6 (𝜑𝑀 ∈ CMnd)
60596oveq1i 6435 . . . . . . . . . . 11 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
606605rpmsubg 19537 . . . . . . . . . 10 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
607 subgsubm 17335 . . . . . . . . . 10 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
608606, 607ax-mp 5 . . . . . . . . 9 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
609102, 103, 104drngui 18487 . . . . . . . . . . 11 (ℂ ∖ {0}) = (Unit‘ℂfld)
610609, 96unitsubm 18404 . . . . . . . . . 10 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
611 eqid 2514 . . . . . . . . . . 11 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
612611subsubm 17076 . . . . . . . . . 10 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
613101, 610, 612mp2b 10 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
614608, 613mpbi 218 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
615614simpli 472 . . . . . . 7 + ∈ (SubMnd‘𝑀)
616615a1i 11 . . . . . 6 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
617 rpre 11577 . . . . . . . . . 10 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
618617anim2i 590 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
619618adantl 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
620 rpcxpcl 24120 . . . . . . . 8 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
621619, 620syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
622 inidm 3687 . . . . . . 7 (𝐴𝐴) = 𝐴
623621, 2, 4, 1, 1, 622off 6684 . . . . . 6 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
624 rpre 11577 . . . . . . . . . . 11 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
625624anim2i 590 . . . . . . . . . 10 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
626625adantl 480 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
627 rpcxpcl 24120 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
628626, 627syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
629 inidm 3687 . . . . . . . 8 (𝐴𝐴) = 𝐴
630628, 2, 4, 1, 1, 629off 6684 . . . . . . 7 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
631 1red 9808 . . . . . . 7 (𝜑 → 1 ∈ ℝ)
632630, 1, 631fdmfifsupp 8042 . . . . . 6 (𝜑 → (𝐹𝑓𝑐𝑊) finSupp 1)
633602, 604, 1, 616, 623, 632gsumsubmcl 18053 . . . . 5 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐𝑊)) ∈ ℝ+)
634633relogcld 24071 . . . 4 (𝜑 → (log‘(𝑀 Σg (𝐹𝑓𝑐𝑊))) ∈ ℝ)
635 simprl 789 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
636635rpcnd 11612 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
637 simprr 791 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
638637rpcnd 11612 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
639636, 638mulcomd 9814 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
6401, 4, 2, 639caofcom 6701 . . . . . . 7 (𝜑 → (𝑊𝑓 · 𝐹) = (𝐹𝑓 · 𝑊))
641640oveq2d 6441 . . . . . 6 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝐹𝑓 · 𝑊)))
6424ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
6432ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
6444feqmptd 6042 . . . . . . . . . 10 (𝜑𝑊 = (𝑘𝐴 ↦ (𝑊𝑘)))
6452feqmptd 6042 . . . . . . . . . 10 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
6461, 642, 643, 644, 645offval2 6686 . . . . . . . . 9 (𝜑 → (𝑊𝑓 · 𝐹) = (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘))))
647646oveq2d 6441 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))))
6484ffvelrnda 6150 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
6492ffvelrnda 6150 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
650648, 649rpmulcld 11626 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
651650rpcnd 11612 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℂ)
6521, 651gsumfsum 19540 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
653647, 652eqtrd 2548 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
6544ffvelrnda 6150 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
6552ffvelrnda 6150 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
656654, 655rpmulcld 11626 . . . . . . . 8 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
6571, 278, 656fsumrpcl 14179 . . . . . . 7 (𝜑 → Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
658653, 657eqeltrd 2592 . . . . . 6 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) ∈ ℝ+)
659641, 658eqeltrrd 2593 . . . . 5 (𝜑 → (ℂfld Σg (𝐹𝑓 · 𝑊)) ∈ ℝ+)
660659relogcld 24071 . . . 4 (𝜑 → (log‘(ℂfld Σg (𝐹𝑓 · 𝑊))) ∈ ℝ)
661 efle 14551 . . . 4 (((log‘(𝑀 Σg (𝐹𝑓𝑐𝑊))) ∈ ℝ ∧ (log‘(ℂfld Σg (𝐹𝑓 · 𝑊))) ∈ ℝ) → ((log‘(𝑀 Σg (𝐹𝑓𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹𝑓 · 𝑊))) ↔ (exp‘(log‘(𝑀 Σg (𝐹𝑓𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹𝑓 · 𝑊))))))
662634, 660, 661syl2anc 690 . . 3 (𝜑 → ((log‘(𝑀 Σg (𝐹𝑓𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹𝑓 · 𝑊))) ↔ (exp‘(log‘(𝑀 Σg (𝐹𝑓𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹𝑓 · 𝑊))))))
663601, 662mpbid 220 . 2 (𝜑 → (exp‘(log‘(𝑀 Σg (𝐹𝑓𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹𝑓 · 𝑊)))))
66496, 115ringidval 18237 . . . . 5 1 = (0g𝑀)
66596crngmgp 18289 . . . . . 6 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
666133, 665mp1i 13 . . . . 5 (𝜑𝑀 ∈ CMnd)
66796oveq1i 6435 . . . . . . . . . 10 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
668667rpmsubg 19537 . . . . . . . . 9 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
669 subgsubm 17335 . . . . . . . . 9 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
670668, 669ax-mp 5 . . . . . . . 8 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
671102, 103, 104drngui 18487 . . . . . . . . . 10 (ℂ ∖ {0}) = (Unit‘ℂfld)
672671, 96unitsubm 18404 . . . . . . . . 9 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
673 eqid 2514 . . . . . . . . . 10 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
674673subsubm 17076 . . . . . . . . 9 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
675101, 672, 674mp2b 10 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
676670, 675mpbi 218 . . . . . . 7 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
677676simpli 472 . . . . . 6 + ∈ (SubMnd‘𝑀)
678677a1i 11 . . . . 5 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
679 rpre 11577 . . . . . . . . 9 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
680679anim2i 590 . . . . . . . 8 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
681680adantl 480 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
682 rpcxpcl 24120 . . . . . . 7 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
683681, 682syl 17 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
684 inidm 3687 . . . . . 6 (𝐴𝐴) = 𝐴
685683, 2, 4, 1, 1, 684off 6684 . . . . 5 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
686 rpre 11577 . . . . . . . . . 10 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
687686anim2i 590 . . . . . . . . 9 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
688687adantl 480 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
689 rpcxpcl 24120 . . . . . . . 8 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
690688, 689syl 17 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
691 inidm 3687 . . . . . . 7 (𝐴𝐴) = 𝐴
692690, 2, 4, 1, 1, 691off 6684 . . . . . 6 (𝜑 → (𝐹𝑓𝑐𝑊):𝐴⟶ℝ+)
693 1red 9808 . . . . . 6 (𝜑 → 1 ∈ ℝ)
694692, 1, 693fdmfifsupp 8042 . . . . 5 (𝜑 → (𝐹𝑓𝑐𝑊) finSupp 1)
695664, 666, 1, 678, 685, 694gsumsubmcl 18053 . . . 4 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐𝑊)) ∈ ℝ+)
696695reeflogd 24072 . . 3 (𝜑 → (exp‘(log‘(𝑀 Σg (𝐹𝑓𝑐𝑊)))) = (𝑀 Σg (𝐹𝑓𝑐𝑊)))
697696eqcomd 2520 . 2 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐𝑊)) = (exp‘(log‘(𝑀 Σg (𝐹𝑓𝑐𝑊)))))
698 simprl 789 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
699698rpcnd 11612 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
700 simprr 791 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
701700rpcnd 11612 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
702699, 701mulcomd 9814 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
7031, 4, 2, 702caofcom 6701 . . . . . 6 (𝜑 → (𝑊𝑓 · 𝐹) = (𝐹𝑓 · 𝑊))
704703oveq2d 6441 . . . . 5 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝐹𝑓 · 𝑊)))
7054ffvelrnda 6150 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
7062ffvelrnda 6150 . . . . . . . . 9 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
7074feqmptd 6042 . . . . . . . . 9 (𝜑𝑊 = (𝑘𝐴 ↦ (𝑊𝑘)))
7082feqmptd 6042 . . . . . . . . 9 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
7091, 705, 706, 707, 708offval2 6686 . . . . . . . 8 (𝜑 → (𝑊𝑓 · 𝐹) = (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘))))
710709oveq2d 6441 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))))
7114ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
7122ffvelrnda 6150 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
713711, 712rpmulcld 11626 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
714713rpcnd 11612 . . . . . . . 8 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℂ)
7151, 714gsumfsum 19540 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
716710, 715eqtrd 2548 . . . . . 6 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
7174ffvelrnda 6150 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
7182ffvelrnda 6150 . . . . . . . 8 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
719717, 718rpmulcld 11626 . . . . . . 7 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
7201, 278, 719fsumrpcl 14179 . . . . . 6 (𝜑 → Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
721716, 720eqeltrd 2592 . . . . 5 (𝜑 → (ℂfld Σg (𝑊𝑓 · 𝐹)) ∈ ℝ+)
722704, 721eqeltrrd 2593 . . . 4 (𝜑 → (ℂfld Σg (𝐹𝑓 · 𝑊)) ∈ ℝ+)
723722reeflogd 24072 . . 3 (𝜑 → (exp‘(log‘(ℂfld Σg (𝐹𝑓 · 𝑊)))) = (ℂfld Σg (𝐹𝑓 · 𝑊)))
724723eqcomd 2520 . 2 (𝜑 → (ℂfld Σg (𝐹𝑓 · 𝑊)) = (exp‘(log‘(ℂfld Σg (𝐹𝑓 · 𝑊)))))
725663, 697, 7243brtr4d 4513 1 (𝜑 → (𝑀 Σg (𝐹𝑓𝑐𝑊)) ≤ (ℂfld Σg (𝐹𝑓 · 𝑊)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1938  wne 2684  Vcvv 3077  cdif 3441  wss 3444  c0 3777  {csn 4028   class class class wbr 4481  cmpt 4541  cres 4934  ccom 4936  wf 5685  1-1-ontowf1o 5688  cfv 5689  (class class class)co 6425  𝑓 cof 6667  Fincfn 7715  cc 9687  cr 9688  0cc0 9689  1c1 9690   + caddc 9692   · cmul 9694  +∞cpnf 9824   < clt 9827  cle 9828  cmin 10015  -cneg 10016   / cdiv 10431  +crp 11570  (,)cioo 11911  [,)cico 11913  [,]cicc 11914  Σcsu 14128  expce 14495  Basecbs 15583  s cress 15584  0gc0g 15811   Σg cgsu 15812  Mndcmnd 17013   MndHom cmhm 17052  SubMndcsubmnd 17053  SubGrpcsubg 17307   GrpHom cghm 17376   GrpIso cgim 17418  CMndccmn 17928  mulGrpcmgp 18223  Ringcrg 18281  CRingccrg 18282  DivRingcdr 18481  SubRingcsubrg 18510  fldccnfld 19475  fldcrefld 19679  logclog 24003  𝑐ccxp 24004
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721  ax-inf2 8295  ax-cnex 9745  ax-resscn 9746  ax-1cn 9747  ax-icn 9748  ax-addcl 9749  ax-addrcl 9750  ax-mulcl 9751  ax-mulrcl 9752  ax-mulcom 9753  ax-addass 9754  ax-mulass 9755  ax-distr 9756  ax-i2m1 9757  ax-1ne0 9758  ax-1rid 9759  ax-rnegex 9760  ax-rrecex 9761  ax-cnre 9762  ax-pre-lttri 9763  ax-pre-lttrn 9764  ax-pre-ltadd 9765  ax-pre-mulgt0 9766  ax-pre-sup 9767  ax-addf 9768  ax-mulf 9769
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-iin 4356  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6387  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-of 6669  df-om 6832  df-1st 6932  df-2nd 6933  df-supp 7056  df-tpos 7112  df-wrecs 7167  df-recs 7229  df-rdg 7267  df-1o 7321  df-2o 7322  df-oadd 7325  df-er 7503  df-map 7620  df-pm 7621  df-ixp 7669  df-en 7716  df-dom 7717  df-sdom 7718  df-fin 7719  df-fsupp 8033  df-fi 8074  df-sup 8105  df-inf 8106  df-oi 8172  df-card 8522  df-cda 8747  df-pnf 9829  df-mnf 9830  df-xr 9831  df-ltxr 9832  df-le 9833  df-sub 10017  df-neg 10018  df-div 10432  df-nn 10774  df-2 10832  df-3 10833  df-4 10834  df-5 10835  df-6 10836  df-7 10837  df-8 10838  df-9 10839  df-10OLD 10840  df-n0 11046  df-z 11117  df-dec 11232  df-uz 11424  df-q 11527  df-rp 11571  df-xneg 11684  df-xadd 11685  df-xmul 11686  df-ioo 11915  df-ioc 11916  df-ico 11917  df-icc 11918  df-fz 12062  df-fzo 12199  df-fl 12319  df-mod 12395  df-seq 12528  df-exp 12587  df-fac 12787  df-bc 12816  df-hash 12844  df-shft 13509  df-cj 13541  df-re 13542  df-im 13543  df-sqrt 13677  df-abs 13678  df-limsup 13905  df-clim 13928  df-rlim 13929  df-sum 14129  df-ef 14501  df-sin 14503  df-cos 14504  df-pi 14506  df-struct 15585  df-ndx 15586  df-slot 15587  df-base 15588  df-sets 15589  df-ress 15590  df-plusg 15669  df-mulr 15670  df-starv 15671  df-sca 15672  df-vsca 15673  df-ip 15674  df-tset 15675  df-ple 15676  df-ds 15679  df-unif 15680  df-hom 15681  df-cco 15682  df-rest 15794  df-topn 15795  df-0g 15813  df-gsum 15814  df-topgen 15815  df-pt 15816  df-prds 15819  df-xrs 15873  df-qtop 15879  df-imas 15880  df-xps 15883  df-mre 15965  df-mrc 15966  df-acs 15968  df-mgm 16961  df-sgrp 17003  df-mnd 17014  df-mhm 17054  df-submnd 17055  df-grp 17144  df-minusg 17145  df-mulg 17260  df-subg 17310  df-ghm 17377  df-gim 17420  df-cntz 17469  df-cmn 17930  df-abl 17931  df-mgp 18224  df-ur 18236  df-ring 18283  df-cring 18284  df-oppr 18357  df-dvdsr 18375  df-unit 18376  df-invr 18406  df-dvr 18417  df-drng 18483  df-subrg 18512  df-psmet 19467  df-xmet 19468  df-met 19469  df-bl 19470  df-mopn 19471  df-fbas 19472  df-fg 19473  df-cnfld 19476  df-refld 19680  df-top 20428  df-bases 20429  df-topon 20430  df-topsp 20431  df-cld 20540  df-ntr 20541  df-cls 20542  df-nei 20619  df-lp 20657  df-perf 20658  df-cn 20748  df-cnp 20749  df-haus 20836  df-cmp 20907  df-tx 21082  df-hmeo 21275  df-fil 21367  df-fm 21459  df-flim 21460  df-flf 21461  df-xms 21841  df-ms 21842  df-tms 21843  df-cncf 22416  df-limc 23322  df-dv 23323  df-log 24005  df-cxp 24006
This theorem is referenced by:  amgmlemALT  42410  amgmw2d  42411
  Copyright terms: Public domain W3C validator