amgmlem

	Ref	Expression
Hypotheses	amgm.1	$⊢ M = {mulGrp}_{ℂ_{fld}}$
	amgm.2	$⊢ φ \to A \in Fin$
	amgm.3	$⊢ φ \to A \neq \emptyset$
	amgm.4	$⊢ φ \to F : A ⟶ ℝ^{+}$
Assertion	amgmlem	$⊢ φ \to {(\sum_{M}, F)}^{\frac{1}{\|A\|}} \leq \frac{\sum_{ℂ_{fld}} F}{\|A\|}$

Proof

Step	Hyp	Ref	Expression
1		amgm.1	$⊢ M = {mulGrp}_{ℂ_{fld}}$
2		amgm.2	$⊢ φ \to A \in Fin$
3		amgm.3	$⊢ φ \to A \neq \emptyset$
4		amgm.4	$⊢ φ \to F : A ⟶ ℝ^{+}$
5		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
6		cnring	$⊢ ℂ_{fld} \in Ring$
7		ringabl	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Abel$
8	6 7	mp1i	$⊢ φ \to ℂ_{fld} \in Abel$
9		resubdrg	$⊢ (ℝ \in SubRing (ℂ_{fld}) \land ℝ_{fld} \in DivRing)$
10	9	simpli	$⊢ ℝ \in SubRing (ℂ_{fld})$
11		subrgsubg	$⊢ ℝ \in SubRing (ℂ_{fld}) \to ℝ \in SubGrp (ℂ_{fld})$
12	10 11	mp1i	$⊢ φ \to ℝ \in SubGrp (ℂ_{fld})$
13	4	ffvelrnda	$⊢ (φ \land k \in A) \to F (k) \in ℝ^{+}$
14	13	relogcld	$⊢ (φ \land k \in A) \to \log F (k) \in ℝ$
15	14	renegcld	$⊢ (φ \land k \in A) \to - \log F (k) \in ℝ$
16	15	fmpttd	$⊢ φ \to (k \in A ⟼ - \log F (k)) : A ⟶ ℝ$
17		c0ex	$⊢ 0 \in V$
18	17	a1i	$⊢ φ \to 0 \in V$
19	16 2 18	fdmfifsupp	$⊢ φ \to {finSupp}_{0} ((k \in A ⟼ - \log F (k)))$
20	5 8 2 12 16 19	gsumsubgcl	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k)) \in ℝ$
21	20	recnd	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k)) \in ℂ$
22		hashnncl	$⊢ A \in Fin \to (\|A\| \in ℕ \leftrightarrow A \neq \emptyset)$
23	2 22	syl	$⊢ φ \to (\|A\| \in ℕ \leftrightarrow A \neq \emptyset)$
24	3 23	mpbird	$⊢ φ \to \|A\| \in ℕ$
25	24	nncnd	$⊢ φ \to \|A\| \in ℂ$
26	24	nnne0d	$⊢ φ \to \|A\| \neq 0$
27	21 25 26	divnegd	$⊢ φ \to - \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|} = \frac{- (\underset{k \in A}{\sum_{ℂ_{fld}}}, (- \log F (k)))}{\|A\|}$
28	14	recnd	$⊢ (φ \land k \in A) \to \log F (k) \in ℂ$
29	2 28	gsumfsum	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} \log F (k) = \sum_{k \in A} \log F (k)$
30	28	negnegd	$⊢ (φ \land k \in A) \to - (- \log F (k)) = \log F (k)$
31	30	sumeq2dv	$⊢ φ \to \sum_{k \in A} (- (- \log F (k))) = \sum_{k \in A} \log F (k)$
32	15	recnd	$⊢ (φ \land k \in A) \to - \log F (k) \in ℂ$
33	2 32	fsumneg	$⊢ φ \to \sum_{k \in A} (- (- \log F (k))) = - \sum_{k \in A} (- \log F (k))$
34	29 31 33	3eqtr2rd	$⊢ φ \to - \sum_{k \in A} (- \log F (k)) = \underset{k \in A}{\sum_{ℂ_{fld}}} \log F (k)$
35	2 32	gsumfsum	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k)) = \sum_{k \in A} (- \log F (k))$
36	35	negeqd	$⊢ φ \to - (\underset{k \in A}{\sum_{ℂ_{fld}}}, (- \log F (k))) = - \sum_{k \in A} (- \log F (k))$
37	4	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
38		relogf1o	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{1-1 onto}{⟶} ℝ$
39		f1of	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{1-1 onto}{⟶} ℝ \to ({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$
40	38 39	mp1i	$⊢ φ \to ({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$
41	40	feqmptd	$⊢ φ \to {log ↾}_{ℝ^{+}} = (x \in ℝ^{+} ⟼ ({log ↾}_{ℝ^{+}}) (x))$
42		fvres	$⊢ x \in ℝ^{+} \to ({log ↾}_{ℝ^{+}}) (x) = \log x$
43	42	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ ({log ↾}_{ℝ^{+}}) (x)) = (x \in ℝ^{+} ⟼ \log x)$
44	41 43	eqtrdi	$⊢ φ \to {log ↾}_{ℝ^{+}} = (x \in ℝ^{+} ⟼ \log x)$
45		fveq2	$⊢ x = F (k) \to \log x = \log F (k)$
46	13 37 44 45	fmptco	$⊢ φ \to ({log ↾}_{ℝ^{+}}) \circ F = (k \in A ⟼ \log F (k))$
47	46	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} (({log ↾}_{ℝ^{+}}) \circ F) = \underset{k \in A}{\sum_{ℂ_{fld}}} \log F (k)$
48	34 36 47	3eqtr4d	$⊢ φ \to - (\underset{k \in A}{\sum_{ℂ_{fld}}}, (- \log F (k))) = \sum_{ℂ_{fld}} (({log ↾}_{ℝ^{+}}) \circ F)$
49	1	oveq1i	$⊢ M ↾_{𝑠} (ℂ ∖ \{0\}) = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
50	49	rpmsubg	$⊢ ℝ^{+} \in SubGrp (M ↾_{𝑠} (ℂ ∖ \{0\}))$
51		subgsubm	$⊢ ℝ^{+} \in SubGrp (M ↾_{𝑠} (ℂ ∖ \{0\})) \to ℝ^{+} \in SubMnd (M ↾_{𝑠} (ℂ ∖ \{0\}))$
52	50 51	ax-mp	$⊢ ℝ^{+} \in SubMnd (M ↾_{𝑠} (ℂ ∖ \{0\}))$
53		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
54		cndrng	$⊢ ℂ_{fld} \in DivRing$
55	53 5 54	drngui	$⊢ ℂ ∖ \{0\} = Unit (ℂ_{fld})$
56	55 1	unitsubm	$⊢ ℂ_{fld} \in Ring \to ℂ ∖ \{0\} \in SubMnd (M)$
57		eqid	$⊢ M ↾_{𝑠} (ℂ ∖ \{0\}) = M ↾_{𝑠} (ℂ ∖ \{0\})$
58	57	subsubm	$⊢ ℂ ∖ \{0\} \in SubMnd (M) \to (ℝ^{+} \in SubMnd (M ↾_{𝑠} (ℂ ∖ \{0\})) \leftrightarrow (ℝ^{+} \in SubMnd (M) \land ℝ^{+} \subseteq ℂ ∖ \{0\}))$
59	6 56 58	mp2b	$⊢ ℝ^{+} \in SubMnd (M ↾_{𝑠} (ℂ ∖ \{0\})) \leftrightarrow (ℝ^{+} \in SubMnd (M) \land ℝ^{+} \subseteq ℂ ∖ \{0\})$
60	52 59	mpbi	$⊢ (ℝ^{+} \in SubMnd (M) \land ℝ^{+} \subseteq ℂ ∖ \{0\})$
61	60	simpli	$⊢ ℝ^{+} \in SubMnd (M)$
62		eqid	$⊢ M ↾_{𝑠} ℝ^{+} = M ↾_{𝑠} ℝ^{+}$
63	62	submbas	$⊢ ℝ^{+} \in SubMnd (M) \to ℝ^{+} = {Base}_{(M ↾_{𝑠} ℝ^{+})}$
64	61 63	ax-mp	$⊢ ℝ^{+} = {Base}_{(M ↾_{𝑠} ℝ^{+})}$
65		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
66	1 65	ringidval	$⊢ 1 = 0_{M}$
67	62 66	subm0	$⊢ ℝ^{+} \in SubMnd (M) \to 1 = 0_{(M ↾_{𝑠} ℝ^{+})}$
68	61 67	ax-mp	$⊢ 1 = 0_{(M ↾_{𝑠} ℝ^{+})}$
69		cncrng	$⊢ ℂ_{fld} \in CRing$
70	1	crngmgp	$⊢ ℂ_{fld} \in CRing \to M \in CMnd$
71	69 70	mp1i	$⊢ φ \to M \in CMnd$
72	62	submmnd	$⊢ ℝ^{+} \in SubMnd (M) \to M ↾_{𝑠} ℝ^{+} \in Mnd$
73	61 72	mp1i	$⊢ φ \to M ↾_{𝑠} ℝ^{+} \in Mnd$
74	62	subcmn	$⊢ (M \in CMnd \land M ↾_{𝑠} ℝ^{+} \in Mnd) \to M ↾_{𝑠} ℝ^{+} \in CMnd$
75	71 73 74	syl2anc	$⊢ φ \to M ↾_{𝑠} ℝ^{+} \in CMnd$
76		df-refld	$⊢ ℝ_{fld} = ℂ_{fld} ↾_{𝑠} ℝ$
77	76	subrgring	$⊢ ℝ \in SubRing (ℂ_{fld}) \to ℝ_{fld} \in Ring$
78	10 77	ax-mp	$⊢ ℝ_{fld} \in Ring$
79		ringmnd	$⊢ ℝ_{fld} \in Ring \to ℝ_{fld} \in Mnd$
80	78 79	mp1i	$⊢ φ \to ℝ_{fld} \in Mnd$
81	1	oveq1i	$⊢ M ↾_{𝑠} ℝ^{+} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℝ^{+}$
82	81	reloggim	$⊢ {log ↾}_{ℝ^{+}} \in ((M ↾_{𝑠} ℝ^{+}) GrpIso ℝ_{fld})$
83		gimghm	$⊢ {log ↾}_{ℝ^{+}} \in ((M ↾_{𝑠} ℝ^{+}) GrpIso ℝ_{fld}) \to {log ↾}_{ℝ^{+}} \in ((M ↾_{𝑠} ℝ^{+}) GrpHom ℝ_{fld})$
84	82 83	ax-mp	$⊢ {log ↾}_{ℝ^{+}} \in ((M ↾_{𝑠} ℝ^{+}) GrpHom ℝ_{fld})$
85		ghmmhm	$⊢ {log ↾}_{ℝ^{+}} \in ((M ↾_{𝑠} ℝ^{+}) GrpHom ℝ_{fld}) \to {log ↾}_{ℝ^{+}} \in ((M ↾_{𝑠} ℝ^{+}) MndHom ℝ_{fld})$
86	84 85	mp1i	$⊢ φ \to {log ↾}_{ℝ^{+}} \in ((M ↾_{𝑠} ℝ^{+}) MndHom ℝ_{fld})$
87		1ex	$⊢ 1 \in V$
88	87	a1i	$⊢ φ \to 1 \in V$
89	4 2 88	fdmfifsupp	$⊢ φ \to {finSupp}_{1} (F)$
90	64 68 75 80 2 86 4 89	gsummhm	$⊢ φ \to \sum_{ℝ_{fld}} (({log ↾}_{ℝ^{+}}) \circ F) = ({log ↾}_{ℝ^{+}}) (\sum_{M ↾_{𝑠} ℝ^{+}} F)$
91		subgsubm	$⊢ ℝ \in SubGrp (ℂ_{fld}) \to ℝ \in SubMnd (ℂ_{fld})$
92	12 91	syl	$⊢ φ \to ℝ \in SubMnd (ℂ_{fld})$
93		fco	$⊢ (({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ \land F : A ⟶ ℝ^{+}) \to (({log ↾}_{ℝ^{+}}) \circ F) : A ⟶ ℝ$
94	40 4 93	syl2anc	$⊢ φ \to (({log ↾}_{ℝ^{+}}) \circ F) : A ⟶ ℝ$
95	2 92 94 76	gsumsubm	$⊢ φ \to \sum_{ℂ_{fld}} (({log ↾}_{ℝ^{+}}) \circ F) = \sum_{ℝ_{fld}} (({log ↾}_{ℝ^{+}}) \circ F)$
96	61	a1i	$⊢ φ \to ℝ^{+} \in SubMnd (M)$
97	2 96 4 62	gsumsubm	$⊢ φ \to \sum_{M} F = \sum_{M ↾_{𝑠} ℝ^{+}} F$
98	97	fveq2d	$⊢ φ \to ({log ↾}_{ℝ^{+}}) (\sum_{M} F) = ({log ↾}_{ℝ^{+}}) (\sum_{M ↾_{𝑠} ℝ^{+}} F)$
99	90 95 98	3eqtr4d	$⊢ φ \to \sum_{ℂ_{fld}} (({log ↾}_{ℝ^{+}}) \circ F) = ({log ↾}_{ℝ^{+}}) (\sum_{M} F)$
100	66 71 2 96 4 89	gsumsubmcl	$⊢ φ \to \sum_{M} F \in ℝ^{+}$
101	100	fvresd	$⊢ φ \to ({log ↾}_{ℝ^{+}}) (\sum_{M} F) = \log (\sum_{M}, F)$
102	48 99 101	3eqtrd	$⊢ φ \to - (\underset{k \in A}{\sum_{ℂ_{fld}}}, (- \log F (k))) = \log (\sum_{M}, F)$
103	102	oveq1d	$⊢ φ \to \frac{- (\underset{k \in A}{\sum_{ℂ_{fld}}}, (- \log F (k)))}{\|A\|} = \frac{\log (\sum_{M}, F)}{\|A\|}$
104	100	relogcld	$⊢ φ \to \log (\sum_{M}, F) \in ℝ$
105	104	recnd	$⊢ φ \to \log (\sum_{M}, F) \in ℂ$
106	105 25 26	divrec2d	$⊢ φ \to \frac{\log (\sum_{M}, F)}{\|A\|} = (\frac{1}{\|A\|}) \log (\sum_{M}, F)$
107	27 103 106	3eqtrd	$⊢ φ \to - \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|} = (\frac{1}{\|A\|}) \log (\sum_{M}, F)$
108	37	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} F = \underset{k \in A}{\sum_{ℂ_{fld}}} F (k)$
109	13	rpcnd	$⊢ (φ \land k \in A) \to F (k) \in ℂ$
110	2 109	gsumfsum	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} F (k) = \sum_{k \in A} F (k)$
111	108 110	eqtrd	$⊢ φ \to \sum_{ℂ_{fld}} F = \sum_{k \in A} F (k)$
112	2 3 13	fsumrpcl	$⊢ φ \to \sum_{k \in A} F (k) \in ℝ^{+}$
113	111 112	eqeltrd	$⊢ φ \to \sum_{ℂ_{fld}} F \in ℝ^{+}$
114	24	nnrpd	$⊢ φ \to \|A\| \in ℝ^{+}$
115	113 114	rpdivcld	$⊢ φ \to \frac{\sum_{ℂ_{fld}} F}{\|A\|} \in ℝ^{+}$
116	115	relogcld	$⊢ φ \to \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|}) \in ℝ$
117	20 24	nndivred	$⊢ φ \to \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|} \in ℝ$
118		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
119	118	a1i	$⊢ φ \to ℝ^{+} \subseteq ℝ$
120		relogcl	$⊢ w \in ℝ^{+} \to \log w \in ℝ$
121	120	adantl	$⊢ (φ \land w \in ℝ^{+}) \to \log w \in ℝ$
122	121	renegcld	$⊢ (φ \land w \in ℝ^{+}) \to - \log w \in ℝ$
123	122	fmpttd	$⊢ φ \to (w \in ℝ^{+} ⟼ - \log w) : ℝ^{+} ⟶ ℝ$
124		ioorp	$⊢ (0, +∞) = ℝ^{+}$
125	124	eleq2i	$⊢ a \in (0, +∞) \leftrightarrow a \in ℝ^{+}$
126	124	eleq2i	$⊢ b \in (0, +∞) \leftrightarrow b \in ℝ^{+}$
127		iccssioo2	$⊢ (a \in (0, +∞) \land b \in (0, +∞)) \to [a, b] \subseteq (0, +∞)$
128	125 126 127	syl2anbr	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to [a, b] \subseteq (0, +∞)$
129	128 124	sseqtrdi	$⊢ (a \in ℝ^{+} \land b \in ℝ^{+}) \to [a, b] \subseteq ℝ^{+}$
130	129	adantl	$⊢ (φ \land (a \in ℝ^{+} \land b \in ℝ^{+})) \to [a, b] \subseteq ℝ^{+}$
131	24	nnrecred	$⊢ φ \to \frac{1}{\|A\|} \in ℝ$
132	114	rpreccld	$⊢ φ \to \frac{1}{\|A\|} \in ℝ^{+}$
133	132	rpge0d	$⊢ φ \to 0 \leq \frac{1}{\|A\|}$
134		elrege0	$⊢ \frac{1}{\|A\|} \in [0, +∞) \leftrightarrow (\frac{1}{\|A\|} \in ℝ \land 0 \leq \frac{1}{\|A\|})$
135	131 133 134	sylanbrc	$⊢ φ \to \frac{1}{\|A\|} \in [0, +∞)$
136		fconst6g	$⊢ \frac{1}{\|A\|} \in [0, +∞) \to (A \times \{\frac{1}{\|A\|}\}) : A ⟶ [0, +∞)$
137	135 136	syl	$⊢ φ \to (A \times \{\frac{1}{\|A\|}\}) : A ⟶ [0, +∞)$
138		0lt1	$⊢ 0 < 1$
139		fconstmpt	$⊢ A \times \{\frac{1}{\|A\|}\} = (k \in A ⟼ \frac{1}{\|A\|})$
140	139	oveq2i	$⊢ \sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\}) = \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|})$
141		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
142	6 141	mp1i	$⊢ φ \to ℂ_{fld} \in Mnd$
143	131	recnd	$⊢ φ \to \frac{1}{\|A\|} \in ℂ$
144		eqid	$⊢ \cdot_{ℂ_{fld}} = \cdot_{ℂ_{fld}}$
145	53 144	gsumconst	$⊢ (ℂ_{fld} \in Mnd \land A \in Fin \land \frac{1}{\|A\|} \in ℂ) \to \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) = \|A\| \cdot_{ℂ_{fld}} (\frac{1}{\|A\|})$
146	142 2 143 145	syl3anc	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) = \|A\| \cdot_{ℂ_{fld}} (\frac{1}{\|A\|})$
147	24	nnzd	$⊢ φ \to \|A\| \in ℤ$
148		cnfldmulg	$⊢ (\|A\| \in ℤ \land \frac{1}{\|A\|} \in ℂ) \to \|A\| \cdot_{ℂ_{fld}} (\frac{1}{\|A\|}) = \|A\| (\frac{1}{\|A\|})$
149	147 143 148	syl2anc	$⊢ φ \to \|A\| \cdot_{ℂ_{fld}} (\frac{1}{\|A\|}) = \|A\| (\frac{1}{\|A\|})$
150	25 26	recidd	$⊢ φ \to \|A\| (\frac{1}{\|A\|}) = 1$
151	146 149 150	3eqtrd	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) = 1$
152	140 151	syl5eq	$⊢ φ \to \sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\}) = 1$
153	138 152	breqtrrid	$⊢ φ \to 0 < \sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})$
154		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)$
155	154	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)$
156		ioossre	$⊢ (0, 1) \subseteq ℝ$
157		simp3	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t \in (0, 1)$
158	156 157	sselid	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t \in ℝ$
159		simp21	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to x \in ℝ^{+}$
160	159	relogcld	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to \log x \in ℝ$
161	158 160	remulcld	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t \log x \in ℝ$
162		1re	$⊢ 1 \in ℝ$
163		resubcl	$⊢ (1 \in ℝ \land t \in ℝ) \to 1 - t \in ℝ$
164	162 158 163	sylancr	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to 1 - t \in ℝ$
165		simp22	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to y \in ℝ^{+}$
166	165	relogcld	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to \log y \in ℝ$
167	164 166	remulcld	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to (1 - t) \log y \in ℝ$
168	161 167	readdcld	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t \log x + (1 - t) \log y \in ℝ$
169		simp1	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to φ$
170		ioossicc	$⊢ (0, 1) \subseteq [0, 1]$
171	170 157	sselid	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t \in [0, 1]$
172	119 130	cvxcl	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land t \in [0, 1])) \to t x + (1 - t) y \in ℝ^{+}$
173	169 159 165 171 172	syl13anc	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t x + (1 - t) y \in ℝ^{+}$
174	173	relogcld	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to \log (t x + (1 - t) y) \in ℝ$
175	168 174	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))$
176	155 175	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)$
177		fveq2	$⊢ w = t x + (1 - t) y \to \log w = \log (t x + (1 - t) y)$
178	177	negeqd	$⊢ w = t x + (1 - t) y \to - \log w = - \log (t x + (1 - t) y)$
179		eqid	$⊢ (w \in ℝ^{+} ⟼ - \log w) = (w \in ℝ^{+} ⟼ - \log w)$
180		negex	$⊢ - \log (t x + (1 - t) y) \in V$
181	178 179 180	fvmpt	$⊢ t x + (1 - t) y \in ℝ^{+} \to (w \in ℝ^{+} ⟼ - \log w) (t x + (1 - t) y) = - \log (t x + (1 - t) y)$
182	173 181	syl	$⊢ (φ \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)$
183		fveq2	$⊢ w = x \to \log w = \log x$
184	183	negeqd	$⊢ w = x \to - \log w = - \log x$
185		negex	$⊢ - \log x \in V$
186	184 179 185	fvmpt	$⊢ x \in ℝ^{+} \to (w \in ℝ^{+} ⟼ - \log w) (x) = - \log x$
187	159 186	syl	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to (w \in ℝ^{+} ⟼ - \log w) (x) = - \log x$
188	187	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)$
189	158	recnd	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t \in ℂ$
190	160	recnd	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to \log x \in ℂ$
191	189 190	mulneg2d	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t (- \log x) = - t \log x$
192	188 191	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$
193		fveq2	$⊢ w = y \to \log w = \log y$
194	193	negeqd	$⊢ w = y \to - \log w = - \log y$
195		negex	$⊢ - \log y \in V$
196	194 179 195	fvmpt	$⊢ y \in ℝ^{+} \to (w \in ℝ^{+} ⟼ - \log w) (y) = - \log y$
197	165 196	syl	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to (w \in ℝ^{+} ⟼ - \log w) (y) = - \log y$
198	197	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)$
199	164	recnd	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to 1 - t \in ℂ$
200	166	recnd	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to \log y \in ℂ$
201	199 200	mulneg2d	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to (1 - t) (- \log y) = - (1 - t) \log y$
202	198 201	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$
203	192 202	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)$
204	161	recnd	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to t \log x \in ℂ$
205	167	recnd	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+} \land x < y) \land t \in (0, 1)) \to (1 - t) \log y \in ℂ$
206	204 205	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)$
207	203 206	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)$
208	176 182 207	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)$
209	119 123 130 208	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)$
210	119 123 130 2 137 4 153 209	jensen	$⊢ φ \to (\frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F)}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})} \in ℝ^{+} \land (w \in ℝ^{+} ⟼ - \log w) (\frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F)}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})}) \leq \frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} ((w \in ℝ^{+} ⟼ - \log w) \circ F))}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})})$
211	210	simprd	$⊢ φ \to (w \in ℝ^{+} ⟼ - \log w) (\frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F)}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})}) \leq \frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} ((w \in ℝ^{+} ⟼ - \log w) \circ F))}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})}$
212	131	adantr	$⊢ (φ \land k \in A) \to \frac{1}{\|A\|} \in ℝ$
213	139	a1i	$⊢ φ \to A \times \{\frac{1}{\|A\|}\} = (k \in A ⟼ \frac{1}{\|A\|})$
214	2 212 13 213 37	offval2	$⊢ φ \to (A \times \{\frac{1}{\|A\|}\}) \times_{f} F = (k \in A ⟼ (\frac{1}{\|A\|}) F (k))$
215	214	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F) = \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) F (k)$
216		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
217		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
218	6	a1i	$⊢ φ \to ℂ_{fld} \in Ring$
219	109	fmpttd	$⊢ φ \to (k \in A ⟼ F (k)) : A ⟶ ℂ$
220	219 2 18	fdmfifsupp	$⊢ φ \to {finSupp}_{0} ((k \in A ⟼ F (k)))$
221	53 5 216 217 218 2 143 109 220	gsummulc2	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) F (k) = (\frac{1}{\|A\|}) (\underset{k \in A}{\sum_{ℂ_{fld}}}, F (k))$
222		fss	$⊢ (F : A ⟶ ℝ^{+} \land ℝ^{+} \subseteq ℝ) \to F : A ⟶ ℝ$
223	4 118 222	sylancl	$⊢ φ \to F : A ⟶ ℝ$
224	4 2 18	fdmfifsupp	$⊢ φ \to {finSupp}_{0} (F)$
225	5 8 2 12 223 224	gsumsubgcl	$⊢ φ \to \sum_{ℂ_{fld}} F \in ℝ$
226	225	recnd	$⊢ φ \to \sum_{ℂ_{fld}} F \in ℂ$
227	226 25 26	divrec2d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} F}{\|A\|} = (\frac{1}{\|A\|}) (\sum_{ℂ_{fld}}, F)$
228	108	oveq2d	$⊢ φ \to (\frac{1}{\|A\|}) (\sum_{ℂ_{fld}}, F) = (\frac{1}{\|A\|}) (\underset{k \in A}{\sum_{ℂ_{fld}}}, F (k))$
229	227 228	eqtr2d	$⊢ φ \to (\frac{1}{\|A\|}) (\underset{k \in A}{\sum_{ℂ_{fld}}}, F (k)) = \frac{\sum_{ℂ_{fld}} F}{\|A\|}$
230	215 221 229	3eqtrd	$⊢ φ \to \sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F) = \frac{\sum_{ℂ_{fld}} F}{\|A\|}$
231	230 152	oveq12d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F)}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})} = \frac{\frac{\sum_{ℂ_{fld}} F}{\|A\|}}{1}$
232	225 24	nndivred	$⊢ φ \to \frac{\sum_{ℂ_{fld}} F}{\|A\|} \in ℝ$
233	232	recnd	$⊢ φ \to \frac{\sum_{ℂ_{fld}} F}{\|A\|} \in ℂ$
234	233	div1d	$⊢ φ \to \frac{\frac{\sum_{ℂ_{fld}} F}{\|A\|}}{1} = \frac{\sum_{ℂ_{fld}} F}{\|A\|}$
235	231 234	eqtrd	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F)}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})} = \frac{\sum_{ℂ_{fld}} F}{\|A\|}$
236	235	fveq2d	$⊢ φ \to (w \in ℝ^{+} ⟼ - \log w) (\frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F)}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})}) = (w \in ℝ^{+} ⟼ - \log w) (\frac{\sum_{ℂ_{fld}} F}{\|A\|})$
237		fveq2	$⊢ w = \frac{\sum_{ℂ_{fld}} F}{\|A\|} \to \log w = \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})$
238	237	negeqd	$⊢ w = \frac{\sum_{ℂ_{fld}} F}{\|A\|} \to - \log w = - \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})$
239		negex	$⊢ - \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|}) \in V$
240	238 179 239	fvmpt	$⊢ \frac{\sum_{ℂ_{fld}} F}{\|A\|} \in ℝ^{+} \to (w \in ℝ^{+} ⟼ - \log w) (\frac{\sum_{ℂ_{fld}} F}{\|A\|}) = - \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})$
241	115 240	syl	$⊢ φ \to (w \in ℝ^{+} ⟼ - \log w) (\frac{\sum_{ℂ_{fld}} F}{\|A\|}) = - \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})$
242	236 241	eqtrd	$⊢ φ \to (w \in ℝ^{+} ⟼ - \log w) (\frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} F)}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})}) = - \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})$
243	53 5 216 217 218 2 143 32 19	gsummulc2	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) (- \log F (k)) = (\frac{1}{\|A\|}) (\underset{k \in A}{\sum_{ℂ_{fld}}}, (- \log F (k)))$
244		negex	$⊢ - \log F (k) \in V$
245	244	a1i	$⊢ (φ \land k \in A) \to - \log F (k) \in V$
246		eqidd	$⊢ φ \to (w \in ℝ^{+} ⟼ - \log w) = (w \in ℝ^{+} ⟼ - \log w)$
247		fveq2	$⊢ w = F (k) \to \log w = \log F (k)$
248	247	negeqd	$⊢ w = F (k) \to - \log w = - \log F (k)$
249	13 37 246 248	fmptco	$⊢ φ \to (w \in ℝ^{+} ⟼ - \log w) \circ F = (k \in A ⟼ - \log F (k))$
250	2 212 245 213 249	offval2	$⊢ φ \to (A \times \{\frac{1}{\|A\|}\}) \times_{f} ((w \in ℝ^{+} ⟼ - \log w) \circ F) = (k \in A ⟼ (\frac{1}{\|A\|}) (- \log F (k)))$
251	250	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} ((w \in ℝ^{+} ⟼ - \log w) \circ F)) = \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) (- \log F (k))$
252	21 25 26	divrec2d	$⊢ φ \to \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|} = (\frac{1}{\|A\|}) (\underset{k \in A}{\sum_{ℂ_{fld}}}, (- \log F (k)))$
253	243 251 252	3eqtr4d	$⊢ φ \to \sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} ((w \in ℝ^{+} ⟼ - \log w) \circ F)) = \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|}$
254	253 152	oveq12d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} ((w \in ℝ^{+} ⟼ - \log w) \circ F))}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})} = \frac{\frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|}}{1}$
255	117	recnd	$⊢ φ \to \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|} \in ℂ$
256	255	div1d	$⊢ φ \to \frac{\frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|}}{1} = \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|}$
257	254 256	eqtrd	$⊢ φ \to \frac{\sum_{ℂ_{fld}} ((A \times \{\frac{1}{\|A\|}\}) \times_{f} ((w \in ℝ^{+} ⟼ - \log w) \circ F))}{\sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\})} = \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|}$
258	211 242 257	3brtr3d	$⊢ φ \to - \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|}) \leq \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|}$
259	116 117 258	lenegcon1d	$⊢ φ \to - \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} (- \log F (k))}{\|A\|} \leq \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})$
260	107 259	eqbrtrrd	$⊢ φ \to (\frac{1}{\|A\|}) \log (\sum_{M}, F) \leq \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})$
261	131 104	remulcld	$⊢ φ \to (\frac{1}{\|A\|}) \log (\sum_{M}, F) \in ℝ$
262		efle	$⊢ ((\frac{1}{\|A\|}) \log (\sum_{M}, F) \in ℝ \land \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|}) \in ℝ) \to ((\frac{1}{\|A\|}) \log (\sum_{M}, F) \leq \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|}) \leftrightarrow e^{(\frac{1}{\|A\|}) \log (\sum_{M}, F)} \leq e^{\log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})})$
263	261 116 262	syl2anc	$⊢ φ \to ((\frac{1}{\|A\|}) \log (\sum_{M}, F) \leq \log (\frac{\sum_{ℂ_{fld}} F}{\|A\|}) \leftrightarrow e^{(\frac{1}{\|A\|}) \log (\sum_{M}, F)} \leq e^{\log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})})$
264	260 263	mpbid	$⊢ φ \to e^{(\frac{1}{\|A\|}) \log (\sum_{M}, F)} \leq e^{\log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})}$
265	100	rpcnd	$⊢ φ \to \sum_{M} F \in ℂ$
266	100	rpne0d	$⊢ φ \to \sum_{M} F \neq 0$
267	265 266 143	cxpefd	$⊢ φ \to {(\sum_{M}, F)}^{\frac{1}{\|A\|}} = e^{(\frac{1}{\|A\|}) \log (\sum_{M}, F)}$
268	115	reeflogd	$⊢ φ \to e^{\log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})} = \frac{\sum_{ℂ_{fld}} F}{\|A\|}$
269	268	eqcomd	$⊢ φ \to \frac{\sum_{ℂ_{fld}} F}{\|A\|} = e^{\log (\frac{\sum_{ℂ_{fld}} F}{\|A\|})}$
270	264 267 269	3brtr4d	$⊢ φ \to {(\sum_{M}, F)}^{\frac{1}{\|A\|}} \leq \frac{\sum_{ℂ_{fld}} F}{\|A\|}$

Metamath Proof Explorer

Theorem amgmlem

Proof