amgmwlem

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

	Ref	Expression
Hypotheses	amgmwlem.0	$⊢ M = {mulGrp}_{ℂ_{fld}}$
	amgmwlem.1	$⊢ φ \to A \in Fin$
	amgmwlem.2	$⊢ φ \to A \neq \emptyset$
	amgmwlem.3	$⊢ φ \to F : A ⟶ ℝ^{+}$
	amgmwlem.4	$⊢ φ \to W : A ⟶ ℝ^{+}$
	amgmwlem.5	$⊢ φ \to \sum_{ℂ_{fld}} W = 1$
Assertion	amgmwlem	$⊢ φ \to \sum_{M} (F {↑_{c}}_{f} W) \leq \sum_{ℂ_{fld}} (F \times_{f} W)$

Proof

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

Metamath Proof Explorer

Theorem amgmwlem

Proof