Metamath Proof Explorer

Theorem 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 ` CCfld )
amgmlemALT.1 
|- ( ph -> A e. Fin )
amgmlemALT.2 
|- ( ph -> A =/= (/) )
amgmlemALT.3 
|- ( ph -> F : A --> RR+ )
Assertion amgmlemALT 
|- ( ph -> ( ( M gsum F ) ^c ( 1 / ( # ` A ) ) ) <_ ( ( CCfld gsum F ) / ( # ` A ) ) )

Proof

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