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 ⊢ 𝑀 = ( mulGrp ‘ ℂfld )
amgmlemALT.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
amgmlemALT.2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
amgmlemALT.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ+ )
Assertion amgmlemALT ( 𝜑 → ( ( 𝑀 Σg 𝐹 ) ↑𝑐 ( 1 / ( ♯ ‘ 𝐴 ) ) ) ≤ ( ( ℂfld Σg 𝐹 ) / ( ♯ ‘ 𝐴 ) ) )

Proof

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