amgmlemALT

Description: Alternate proof of amgmlem using amgmwlem . (Contributed by Kunhao Zheng, 20-Jun-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		amgmlemALT.0	$⊢ M = {mulGrp}_{ℂ_{fld}}$
2		amgmlemALT.1	$⊢ φ \to A \in Fin$
3		amgmlemALT.2	$⊢ φ \to A \neq \emptyset$
4		amgmlemALT.3	$⊢ φ \to F : A ⟶ ℝ^{+}$
5		hashnncl	$⊢ A \in Fin \to (\|A\| \in ℕ \leftrightarrow A \neq \emptyset)$
6	2 5	syl	$⊢ φ \to (\|A\| \in ℕ \leftrightarrow A \neq \emptyset)$
7	3 6	mpbird	$⊢ φ \to \|A\| \in ℕ$
8	7	nnrpd	$⊢ φ \to \|A\| \in ℝ^{+}$
9	8	rpreccld	$⊢ φ \to \frac{1}{\|A\|} \in ℝ^{+}$
10		fconst6g	$⊢ \frac{1}{\|A\|} \in ℝ^{+} \to (A \times \{\frac{1}{\|A\|}\}) : A ⟶ ℝ^{+}$
11	9 10	syl	$⊢ φ \to (A \times \{\frac{1}{\|A\|}\}) : A ⟶ ℝ^{+}$
12		fconstmpt	$⊢ A \times \{\frac{1}{\|A\|}\} = (k \in A ⟼ \frac{1}{\|A\|})$
13	12	a1i	$⊢ φ \to A \times \{\frac{1}{\|A\|}\} = (k \in A ⟼ \frac{1}{\|A\|})$
14	13	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\}) = \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|})$
15	7	nnrecred	$⊢ φ \to \frac{1}{\|A\|} \in ℝ$
16	15	recnd	$⊢ φ \to \frac{1}{\|A\|} \in ℂ$
17		simpl	$⊢ (A \in Fin \land \frac{1}{\|A\|} \in ℂ) \to A \in Fin$
18		simplr	$⊢ ((A \in Fin \land \frac{1}{\|A\|} \in ℂ) \land k \in A) \to \frac{1}{\|A\|} \in ℂ$
19	17 18	gsumfsum	$⊢ (A \in Fin \land \frac{1}{\|A\|} \in ℂ) \to \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) = \sum_{k \in A} (\frac{1}{\|A\|})$
20	2 16 19	syl2anc	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} (\frac{1}{\|A\|}) = \sum_{k \in A} (\frac{1}{\|A\|})$
21		fsumconst	$⊢ (A \in Fin \land \frac{1}{\|A\|} \in ℂ) \to \sum_{k \in A} (\frac{1}{\|A\|}) = \|A\| (\frac{1}{\|A\|})$
22	2 16 21	syl2anc	$⊢ φ \to \sum_{k \in A} (\frac{1}{\|A\|}) = \|A\| (\frac{1}{\|A\|})$
23	7	nncnd	$⊢ φ \to \|A\| \in ℂ$
24	7	nnne0d	$⊢ φ \to \|A\| \neq 0$
25	23 24	recidd	$⊢ φ \to \|A\| (\frac{1}{\|A\|}) = 1$
26	22 25	eqtrd	$⊢ φ \to \sum_{k \in A} (\frac{1}{\|A\|}) = 1$
27	14 20 26	3eqtrd	$⊢ φ \to \sum_{ℂ_{fld}} (A \times \{\frac{1}{\|A\|}\}) = 1$
28	1 2 3 4 11 27	amgmwlem	$⊢ φ \to \sum_{M} (F {↑_{c}}_{f} (A \times \{\frac{1}{\|A\|}\})) \leq \sum_{ℂ_{fld}} (F \times_{f} (A \times \{\frac{1}{\|A\|}\}))$
29		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
30		ax-resscn	$⊢ ℝ \subseteq ℂ$
31	29 30	sstri	$⊢ ℝ^{+} \subseteq ℂ$
32		eqid	$⊢ M ↾_{𝑠} ℝ^{+} = M ↾_{𝑠} ℝ^{+}$
33		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
34	1 33	mgpbas	$⊢ ℂ = {Base}_{M}$
35	32 34	ressbas2	$⊢ ℝ^{+} \subseteq ℂ \to ℝ^{+} = {Base}_{(M ↾_{𝑠} ℝ^{+})}$
36	31 35	ax-mp	$⊢ ℝ^{+} = {Base}_{(M ↾_{𝑠} ℝ^{+})}$
37		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
38	1 37	ringidval	$⊢ 1 = 0_{M}$
39	1	oveq1i	$⊢ M ↾_{𝑠} (ℂ ∖ \{0\}) = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
40	39	rpmsubg	$⊢ ℝ^{+} \in SubGrp (M ↾_{𝑠} (ℂ ∖ \{0\}))$
41		subgsubm	$⊢ ℝ^{+} \in SubGrp (M ↾_{𝑠} (ℂ ∖ \{0\})) \to ℝ^{+} \in SubMnd (M ↾_{𝑠} (ℂ ∖ \{0\}))$
42	40 41	ax-mp	$⊢ ℝ^{+} \in SubMnd (M ↾_{𝑠} (ℂ ∖ \{0\}))$
43		cnring	$⊢ ℂ_{fld} \in Ring$
44		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
45		cndrng	$⊢ ℂ_{fld} \in DivRing$
46	33 44 45	drngui	$⊢ ℂ ∖ \{0\} = Unit (ℂ_{fld})$
47	46 1	unitsubm	$⊢ ℂ_{fld} \in Ring \to ℂ ∖ \{0\} \in SubMnd (M)$
48	43 47	ax-mp	$⊢ ℂ ∖ \{0\} \in SubMnd (M)$
49		eqid	$⊢ M ↾_{𝑠} (ℂ ∖ \{0\}) = M ↾_{𝑠} (ℂ ∖ \{0\})$
50	49	subsubm	$⊢ ℂ ∖ \{0\} \in SubMnd (M) \to (ℝ^{+} \in SubMnd (M ↾_{𝑠} (ℂ ∖ \{0\})) \leftrightarrow (ℝ^{+} \in SubMnd (M) \land ℝ^{+} \subseteq ℂ ∖ \{0\}))$
51	48 50	ax-mp	$⊢ ℝ^{+} \in SubMnd (M ↾_{𝑠} (ℂ ∖ \{0\})) \leftrightarrow (ℝ^{+} \in SubMnd (M) \land ℝ^{+} \subseteq ℂ ∖ \{0\})$
52	42 51	mpbi	$⊢ (ℝ^{+} \in SubMnd (M) \land ℝ^{+} \subseteq ℂ ∖ \{0\})$
53	52	simpli	$⊢ ℝ^{+} \in SubMnd (M)$
54		eqid	$⊢ 0_{M} = 0_{M}$
55	32 54	subm0	$⊢ ℝ^{+} \in SubMnd (M) \to 0_{M} = 0_{(M ↾_{𝑠} ℝ^{+})}$
56	53 55	ax-mp	$⊢ 0_{M} = 0_{(M ↾_{𝑠} ℝ^{+})}$
57	38 56	eqtri	$⊢ 1 = 0_{(M ↾_{𝑠} ℝ^{+})}$
58		cncrng	$⊢ ℂ_{fld} \in CRing$
59	1	crngmgp	$⊢ ℂ_{fld} \in CRing \to M \in CMnd$
60	58 59	ax-mp	$⊢ M \in CMnd$
61	32	submmnd	$⊢ ℝ^{+} \in SubMnd (M) \to M ↾_{𝑠} ℝ^{+} \in Mnd$
62	53 61	mp1i	$⊢ φ \to M ↾_{𝑠} ℝ^{+} \in Mnd$
63	32	subcmn	$⊢ (M \in CMnd \land M ↾_{𝑠} ℝ^{+} \in Mnd) \to M ↾_{𝑠} ℝ^{+} \in CMnd$
64	60 62 63	sylancr	$⊢ φ \to M ↾_{𝑠} ℝ^{+} \in CMnd$
65		reex	$⊢ ℝ \in V$
66	65 29	ssexi	$⊢ ℝ^{+} \in V$
67		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
68	1 67	mgpplusg	$⊢ \times = +_{M}$
69	32 68	ressplusg	$⊢ ℝ^{+} \in V \to \times = +_{(M ↾_{𝑠} ℝ^{+})}$
70	66 69	ax-mp	$⊢ \times = +_{(M ↾_{𝑠} ℝ^{+})}$
71		eqid	$⊢ {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\}) = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
72	71	rpmsubg	$⊢ ℝ^{+} \in SubGrp ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\}))$
73	1	oveq1i	$⊢ M ↾_{𝑠} ℝ^{+} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℝ^{+}$
74		cnex	$⊢ ℂ \in V$
75		difss	$⊢ ℂ ∖ \{0\} \subseteq ℂ$
76	74 75	ssexi	$⊢ ℂ ∖ \{0\} \in V$
77		rpcndif0	$⊢ w \in ℝ^{+} \to w \in (ℂ ∖ \{0\})$
78	77	ssriv	$⊢ ℝ^{+} \subseteq ℂ ∖ \{0\}$
79		ressabs	$⊢ (ℂ ∖ \{0\} \in V \land ℝ^{+} \subseteq ℂ ∖ \{0\}) \to ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})) ↾_{𝑠} ℝ^{+} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℝ^{+}$
80	76 78 79	mp2an	$⊢ ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})) ↾_{𝑠} ℝ^{+} = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} ℝ^{+}$
81	73 80	eqtr4i	$⊢ M ↾_{𝑠} ℝ^{+} = ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})) ↾_{𝑠} ℝ^{+}$
82	81	subggrp	$⊢ ℝ^{+} \in SubGrp ({mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})) \to M ↾_{𝑠} ℝ^{+} \in Grp$
83	72 82	mp1i	$⊢ φ \to M ↾_{𝑠} ℝ^{+} \in Grp$
84		simpr	$⊢ (φ \land k \in ℝ^{+}) \to k \in ℝ^{+}$
85	15	adantr	$⊢ (φ \land k \in ℝ^{+}) \to \frac{1}{\|A\|} \in ℝ$
86	84 85	rpcxpcld	$⊢ (φ \land k \in ℝ^{+}) \to k^{\frac{1}{\|A\|}} \in ℝ^{+}$
87		eqid	$⊢ (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) = (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}})$
88	86 87	fmptd	$⊢ φ \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) : ℝ^{+} ⟶ ℝ^{+}$
89		simprl	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to x \in ℝ^{+}$
90	89	rprege0d	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (x \in ℝ \land 0 \leq x)$
91		simprr	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to y \in ℝ^{+}$
92	91	rprege0d	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (y \in ℝ \land 0 \leq y)$
93	16	adantr	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to \frac{1}{\|A\|} \in ℂ$
94		mulcxp	$⊢ ((x \in ℝ \land 0 \leq x) \land (y \in ℝ \land 0 \leq y) \land \frac{1}{\|A\|} \in ℂ) \to {x y}^{\frac{1}{\|A\|}} = x^{\frac{1}{\|A\|}} y^{\frac{1}{\|A\|}}$
95	90 92 93 94	syl3anc	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to {x y}^{\frac{1}{\|A\|}} = x^{\frac{1}{\|A\|}} y^{\frac{1}{\|A\|}}$
96		rpmulcl	$⊢ (x \in ℝ^{+} \land y \in ℝ^{+}) \to x y \in ℝ^{+}$
97	96	adantl	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to x y \in ℝ^{+}$
98		oveq1	$⊢ k = x y \to k^{\frac{1}{\|A\|}} = {x y}^{\frac{1}{\|A\|}}$
99		ovex	$⊢ k^{\frac{1}{\|A\|}} \in V$
100	98 87 99	fvmpt3i	$⊢ x y \in ℝ^{+} \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (x y) = {x y}^{\frac{1}{\|A\|}}$
101	97 100	syl	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (x y) = {x y}^{\frac{1}{\|A\|}}$
102		oveq1	$⊢ k = x \to k^{\frac{1}{\|A\|}} = x^{\frac{1}{\|A\|}}$
103	102 87 99	fvmpt3i	$⊢ x \in ℝ^{+} \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (x) = x^{\frac{1}{\|A\|}}$
104	89 103	syl	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (x) = x^{\frac{1}{\|A\|}}$
105		oveq1	$⊢ k = y \to k^{\frac{1}{\|A\|}} = y^{\frac{1}{\|A\|}}$
106	105 87 99	fvmpt3i	$⊢ y \in ℝ^{+} \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (y) = y^{\frac{1}{\|A\|}}$
107	91 106	syl	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (y) = y^{\frac{1}{\|A\|}}$
108	104 107	oveq12d	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (x) (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (y) = x^{\frac{1}{\|A\|}} y^{\frac{1}{\|A\|}}$
109	95 101 108	3eqtr4d	$⊢ (φ \land (x \in ℝ^{+} \land y \in ℝ^{+})) \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (x y) = (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (x) (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (y)$
110	36 36 70 70 83 83 88 109	isghmd	$⊢ φ \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) \in ((M ↾_{𝑠} ℝ^{+}) GrpHom (M ↾_{𝑠} ℝ^{+}))$
111		ghmmhm	$⊢ (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) \in ((M ↾_{𝑠} ℝ^{+}) GrpHom (M ↾_{𝑠} ℝ^{+})) \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) \in ((M ↾_{𝑠} ℝ^{+}) MndHom (M ↾_{𝑠} ℝ^{+}))$
112	110 111	syl	$⊢ φ \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) \in ((M ↾_{𝑠} ℝ^{+}) MndHom (M ↾_{𝑠} ℝ^{+}))$
113		1red	$⊢ φ \to 1 \in ℝ$
114	4 2 113	fdmfifsupp	$⊢ φ \to {finSupp}_{1} (F)$
115	36 57 64 62 2 112 4 114	gsummhm	$⊢ φ \to \sum_{M ↾_{𝑠} ℝ^{+}} ((k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) \circ F) = (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (\sum_{M ↾_{𝑠} ℝ^{+}} F)$
116	53	a1i	$⊢ φ \to ℝ^{+} \in SubMnd (M)$
117	4	ffvelrnda	$⊢ (φ \land k \in A) \to F (k) \in ℝ^{+}$
118	15	adantr	$⊢ (φ \land k \in A) \to \frac{1}{\|A\|} \in ℝ$
119	117 118	rpcxpcld	$⊢ (φ \land k \in A) \to {F (k)}^{\frac{1}{\|A\|}} \in ℝ^{+}$
120		eqid	$⊢ (k \in A ⟼ {F (k)}^{\frac{1}{\|A\|}}) = (k \in A ⟼ {F (k)}^{\frac{1}{\|A\|}})$
121	119 120	fmptd	$⊢ φ \to (k \in A ⟼ {F (k)}^{\frac{1}{\|A\|}}) : A ⟶ ℝ^{+}$
122	2 116 121 32	gsumsubm	$⊢ φ \to \underset{k \in A}{\sum_{M}} {F (k)}^{\frac{1}{\|A\|}} = \underset{k \in A}{\sum_{M ↾_{𝑠} ℝ^{+}}} {F (k)}^{\frac{1}{\|A\|}}$
123	9	adantr	$⊢ (φ \land k \in A) \to \frac{1}{\|A\|} \in ℝ^{+}$
124	4	feqmptd	$⊢ φ \to F = (k \in A ⟼ F (k))$
125	2 117 123 124 13	offval2	$⊢ φ \to F {↑_{c}}_{f} (A \times \{\frac{1}{\|A\|}\}) = (k \in A ⟼ {F (k)}^{\frac{1}{\|A\|}})$
126	125	oveq2d	$⊢ φ \to \sum_{M} (F {↑_{c}}_{f} (A \times \{\frac{1}{\|A\|}\})) = \underset{k \in A}{\sum_{M}} {F (k)}^{\frac{1}{\|A\|}}$
127	102	cbvmptv	$⊢ (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) = (x \in ℝ^{+} ⟼ x^{\frac{1}{\|A\|}})$
128	127	a1i	$⊢ φ \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) = (x \in ℝ^{+} ⟼ x^{\frac{1}{\|A\|}})$
129		oveq1	$⊢ x = F (k) \to x^{\frac{1}{\|A\|}} = {F (k)}^{\frac{1}{\|A\|}}$
130	117 124 128 129	fmptco	$⊢ φ \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) \circ F = (k \in A ⟼ {F (k)}^{\frac{1}{\|A\|}})$
131	130	oveq2d	$⊢ φ \to \sum_{M ↾_{𝑠} ℝ^{+}} ((k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) \circ F) = \underset{k \in A}{\sum_{M ↾_{𝑠} ℝ^{+}}} {F (k)}^{\frac{1}{\|A\|}}$
132	122 126 131	3eqtr4rd	$⊢ φ \to \sum_{M ↾_{𝑠} ℝ^{+}} ((k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) \circ F) = \sum_{M} (F {↑_{c}}_{f} (A \times \{\frac{1}{\|A\|}\}))$
133	36 57 64 2 4 114	gsumcl	$⊢ φ \to \sum_{M ↾_{𝑠} ℝ^{+}} F \in ℝ^{+}$
134		oveq1	$⊢ k = \sum_{M ↾_{𝑠} ℝ^{+}} F \to k^{\frac{1}{\|A\|}} = {(\sum_{M ↾_{𝑠} ℝ^{+}}, F)}^{\frac{1}{\|A\|}}$
135	134 87 99	fvmpt3i	$⊢ \sum_{M ↾_{𝑠} ℝ^{+}} F \in ℝ^{+} \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (\sum_{M ↾_{𝑠} ℝ^{+}} F) = {(\sum_{M ↾_{𝑠} ℝ^{+}}, F)}^{\frac{1}{\|A\|}}$
136	133 135	syl	$⊢ φ \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (\sum_{M ↾_{𝑠} ℝ^{+}} F) = {(\sum_{M ↾_{𝑠} ℝ^{+}}, F)}^{\frac{1}{\|A\|}}$
137	2 116 4 32	gsumsubm	$⊢ φ \to \sum_{M} F = \sum_{M ↾_{𝑠} ℝ^{+}} F$
138	137	oveq1d	$⊢ φ \to {(\sum_{M}, F)}^{\frac{1}{\|A\|}} = {(\sum_{M ↾_{𝑠} ℝ^{+}}, F)}^{\frac{1}{\|A\|}}$
139	136 138	eqtr4d	$⊢ φ \to (k \in ℝ^{+} ⟼ k^{\frac{1}{\|A\|}}) (\sum_{M ↾_{𝑠} ℝ^{+}} F) = {(\sum_{M}, F)}^{\frac{1}{\|A\|}}$
140	115 132 139	3eqtr3d	$⊢ φ \to \sum_{M} (F {↑_{c}}_{f} (A \times \{\frac{1}{\|A\|}\})) = {(\sum_{M}, F)}^{\frac{1}{\|A\|}}$
141	117	rpcnd	$⊢ (φ \land k \in A) \to F (k) \in ℂ$
142	2 141	fsumcl	$⊢ φ \to \sum_{k \in A} F (k) \in ℂ$
143	142 23 24	divrecd	$⊢ φ \to \frac{\sum_{k \in A} F (k)}{\|A\|} = \sum_{k \in A} F (k) (\frac{1}{\|A\|})$
144	2 16 141	fsummulc1	$⊢ φ \to \sum_{k \in A} F (k) (\frac{1}{\|A\|}) = \sum_{k \in A} F (k) (\frac{1}{\|A\|})$
145	143 144	eqtr2d	$⊢ φ \to \sum_{k \in A} F (k) (\frac{1}{\|A\|}) = \frac{\sum_{k \in A} F (k)}{\|A\|}$
146	16	adantr	$⊢ (φ \land k \in A) \to \frac{1}{\|A\|} \in ℂ$
147	141 146	mulcld	$⊢ (φ \land k \in A) \to F (k) (\frac{1}{\|A\|}) \in ℂ$
148	2 147	gsumfsum	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} F (k) (\frac{1}{\|A\|}) = \sum_{k \in A} F (k) (\frac{1}{\|A\|})$
149	2 141	gsumfsum	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} F (k) = \sum_{k \in A} F (k)$
150	149	oveq1d	$⊢ φ \to \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} F (k)}{\|A\|} = \frac{\sum_{k \in A} F (k)}{\|A\|}$
151	145 148 150	3eqtr4d	$⊢ φ \to \underset{k \in A}{\sum_{ℂ_{fld}}} F (k) (\frac{1}{\|A\|}) = \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} F (k)}{\|A\|}$
152	2 117 146 124 13	offval2	$⊢ φ \to F \times_{f} (A \times \{\frac{1}{\|A\|}\}) = (k \in A ⟼ F (k) (\frac{1}{\|A\|}))$
153	152	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} (F \times_{f} (A \times \{\frac{1}{\|A\|}\})) = \underset{k \in A}{\sum_{ℂ_{fld}}} F (k) (\frac{1}{\|A\|})$
154	124	oveq2d	$⊢ φ \to \sum_{ℂ_{fld}} F = \underset{k \in A}{\sum_{ℂ_{fld}}} F (k)$
155	154	oveq1d	$⊢ φ \to \frac{\sum_{ℂ_{fld}} F}{\|A\|} = \frac{\underset{k \in A}{\sum_{ℂ_{fld}}} F (k)}{\|A\|}$
156	151 153 155	3eqtr4d	$⊢ φ \to \sum_{ℂ_{fld}} (F \times_{f} (A \times \{\frac{1}{\|A\|}\})) = \frac{\sum_{ℂ_{fld}} F}{\|A\|}$
157	28 140 156	3brtr3d	$⊢ φ \to {(\sum_{M}, F)}^{\frac{1}{\|A\|}} \leq \frac{\sum_{ℂ_{fld}} F}{\|A\|}$

Metamath Proof Explorer

Theorem amgmlemALT

Proof