| Step | Hyp | Ref
| Expression |
| 1 | | amgmlemALT.0 |
. . 3
⊢ 𝑀 =
(mulGrp‘ℂfld) |
| 2 | | amgmlemALT.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 3 | | amgmlemALT.2 |
. . 3
⊢ (𝜑 → 𝐴 ≠ ∅) |
| 4 | | amgmlemALT.3 |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶ℝ+) |
| 5 | | hashnncl 14405 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin →
((♯‘𝐴) ∈
ℕ ↔ 𝐴 ≠
∅)) |
| 6 | 2, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
| 7 | 3, 6 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐴) ∈
ℕ) |
| 8 | 7 | nnrpd 13075 |
. . . . 5
⊢ (𝜑 → (♯‘𝐴) ∈
ℝ+) |
| 9 | 8 | rpreccld 13087 |
. . . 4
⊢ (𝜑 → (1 / (♯‘𝐴)) ∈
ℝ+) |
| 10 | | fconst6g 6797 |
. . . 4
⊢ ((1 /
(♯‘𝐴)) ∈
ℝ+ → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶ℝ+) |
| 11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}):𝐴⟶ℝ+) |
| 12 | | fconstmpt 5747 |
. . . . . 6
⊢ (𝐴 × {(1 /
(♯‘𝐴))}) =
(𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴))) |
| 13 | 12 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 × {(1 / (♯‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) |
| 14 | 13 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg (𝐴 × {(1 / (♯‘𝐴))})) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴))))) |
| 15 | 7 | nnrecred 12317 |
. . . . . 6
⊢ (𝜑 → (1 / (♯‘𝐴)) ∈
ℝ) |
| 16 | 15 | recnd 11289 |
. . . . 5
⊢ (𝜑 → (1 / (♯‘𝐴)) ∈
ℂ) |
| 17 | | simpl 482 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (1 /
(♯‘𝐴)) ∈
ℂ) → 𝐴 ∈
Fin) |
| 18 | | simplr 769 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ (1 /
(♯‘𝐴)) ∈
ℂ) ∧ 𝑘 ∈
𝐴) → (1 /
(♯‘𝐴)) ∈
ℂ) |
| 19 | 17, 18 | gsumfsum 21452 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (1 /
(♯‘𝐴)) ∈
ℂ) → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = Σ𝑘 ∈ 𝐴 (1 / (♯‘𝐴))) |
| 20 | 2, 16, 19 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (♯‘𝐴)))) = Σ𝑘 ∈ 𝐴 (1 / (♯‘𝐴))) |
| 21 | | fsumconst 15826 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (1 /
(♯‘𝐴)) ∈
ℂ) → Σ𝑘
∈ 𝐴 (1 /
(♯‘𝐴)) =
((♯‘𝐴) ·
(1 / (♯‘𝐴)))) |
| 22 | 2, 16, 21 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (1 / (♯‘𝐴)) = ((♯‘𝐴) · (1 / (♯‘𝐴)))) |
| 23 | 7 | nncnd 12282 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐴) ∈
ℂ) |
| 24 | 7 | nnne0d 12316 |
. . . . . 6
⊢ (𝜑 → (♯‘𝐴) ≠ 0) |
| 25 | 23, 24 | recidd 12038 |
. . . . 5
⊢ (𝜑 → ((♯‘𝐴) · (1 /
(♯‘𝐴))) =
1) |
| 26 | 22, 25 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (1 / (♯‘𝐴)) = 1) |
| 27 | 14, 20, 26 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (ℂfld
Σg (𝐴 × {(1 / (♯‘𝐴))})) = 1) |
| 28 | 1, 2, 3, 4, 11, 27 | amgmwlem 49321 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f
↑𝑐(𝐴 × {(1 / (♯‘𝐴))}))) ≤
(ℂfld Σg (𝐹 ∘f · (𝐴 × {(1 /
(♯‘𝐴))})))) |
| 29 | | rpssre 13042 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
| 30 | | ax-resscn 11212 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
| 31 | 29, 30 | sstri 3993 |
. . . . 5
⊢
ℝ+ ⊆ ℂ |
| 32 | | eqid 2737 |
. . . . . 6
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
| 33 | | cnfldbas 21368 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
| 34 | 1, 33 | mgpbas 20142 |
. . . . . 6
⊢ ℂ =
(Base‘𝑀) |
| 35 | 32, 34 | ressbas2 17283 |
. . . . 5
⊢
(ℝ+ ⊆ ℂ → ℝ+ =
(Base‘(𝑀
↾s ℝ+))) |
| 36 | 31, 35 | ax-mp 5 |
. . . 4
⊢
ℝ+ = (Base‘(𝑀 ↾s
ℝ+)) |
| 37 | | cnfld1 21406 |
. . . . . 6
⊢ 1 =
(1r‘ℂfld) |
| 38 | 1, 37 | ringidval 20180 |
. . . . 5
⊢ 1 =
(0g‘𝑀) |
| 39 | 1 | oveq1i 7441 |
. . . . . . . . . 10
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
| 40 | 39 | rpmsubg 21449 |
. . . . . . . . 9
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
| 41 | | subgsubm 19166 |
. . . . . . . . 9
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
| 42 | 40, 41 | ax-mp 5 |
. . . . . . . 8
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
| 43 | | cnring 21403 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
| 44 | | cnfld0 21405 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) |
| 45 | | cndrng 21411 |
. . . . . . . . . . . 12
⊢
ℂfld ∈ DivRing |
| 46 | 33, 44, 45 | drngui 20735 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
| 47 | 46, 1 | unitsubm 20386 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
| 48 | 43, 47 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ∈ (SubMnd‘𝑀) |
| 49 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
| 50 | 49 | subsubm 18829 |
. . . . . . . . 9
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
| 51 | 48, 50 | ax-mp 5 |
. . . . . . . 8
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
| 52 | 42, 51 | mpbi 230 |
. . . . . . 7
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
| 53 | 52 | simpli 483 |
. . . . . 6
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
| 54 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 55 | 32, 54 | subm0 18828 |
. . . . . 6
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (0g‘𝑀) = (0g‘(𝑀 ↾s
ℝ+))) |
| 56 | 53, 55 | ax-mp 5 |
. . . . 5
⊢
(0g‘𝑀) = (0g‘(𝑀 ↾s
ℝ+)) |
| 57 | 38, 56 | eqtri 2765 |
. . . 4
⊢ 1 =
(0g‘(𝑀
↾s ℝ+)) |
| 58 | | cncrng 21401 |
. . . . . 6
⊢
ℂfld ∈ CRing |
| 59 | 1 | crngmgp 20238 |
. . . . . 6
⊢
(ℂfld ∈ CRing → 𝑀 ∈ CMnd) |
| 60 | 58, 59 | ax-mp 5 |
. . . . 5
⊢ 𝑀 ∈ CMnd |
| 61 | 32 | submmnd 18826 |
. . . . . 6
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+)
∈ Mnd) |
| 62 | 53, 61 | mp1i 13 |
. . . . 5
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Mnd) |
| 63 | 32 | subcmn 19855 |
. . . . 5
⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾s
ℝ+) ∈ Mnd) → (𝑀 ↾s ℝ+)
∈ CMnd) |
| 64 | 60, 62, 63 | sylancr 587 |
. . . 4
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ CMnd) |
| 65 | | reex 11246 |
. . . . . . . 8
⊢ ℝ
∈ V |
| 66 | 65, 29 | ssexi 5322 |
. . . . . . 7
⊢
ℝ+ ∈ V |
| 67 | | cnfldmul 21372 |
. . . . . . . . 9
⊢ ·
= (.r‘ℂfld) |
| 68 | 1, 67 | mgpplusg 20141 |
. . . . . . . 8
⊢ ·
= (+g‘𝑀) |
| 69 | 32, 68 | ressplusg 17334 |
. . . . . . 7
⊢
(ℝ+ ∈ V → · =
(+g‘(𝑀
↾s ℝ+))) |
| 70 | 66, 69 | ax-mp 5 |
. . . . . 6
⊢ ·
= (+g‘(𝑀
↾s ℝ+)) |
| 71 | | eqid 2737 |
. . . . . . . 8
⊢
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
| 72 | 71 | rpmsubg 21449 |
. . . . . . 7
⊢
ℝ+ ∈
(SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) |
| 73 | 1 | oveq1i 7441 |
. . . . . . . . 9
⊢ (𝑀 ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+) |
| 74 | | cnex 11236 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
| 75 | | difss 4136 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) ⊆ ℂ |
| 76 | 74, 75 | ssexi 5322 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) ∈ V |
| 77 | | rpcndif0 13054 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ+
→ 𝑤 ∈ (ℂ
∖ {0})) |
| 78 | 77 | ssriv 3987 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ (ℂ ∖ {0}) |
| 79 | | ressabs 17294 |
. . . . . . . . . 10
⊢
(((ℂ ∖ {0}) ∈ V ∧ ℝ+ ⊆
(ℂ ∖ {0})) → (((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})) ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+)) |
| 80 | 76, 78, 79 | mp2an 692 |
. . . . . . . . 9
⊢
(((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) ↾s ℝ+) =
((mulGrp‘ℂfld) ↾s
ℝ+) |
| 81 | 73, 80 | eqtr4i 2768 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})) ↾s
ℝ+) |
| 82 | 81 | subggrp 19147 |
. . . . . . 7
⊢
(ℝ+ ∈
(SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) → (𝑀 ↾s ℝ+)
∈ Grp) |
| 83 | 72, 82 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Grp) |
| 84 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ+) → 𝑘 ∈
ℝ+) |
| 85 | 15 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ+) → (1 /
(♯‘𝐴)) ∈
ℝ) |
| 86 | 84, 85 | rpcxpcld 26775 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ+) → (𝑘↑𝑐(1 /
(♯‘𝐴))) ∈
ℝ+) |
| 87 | | eqid 2737 |
. . . . . . 7
⊢ (𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))) =
(𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))) |
| 88 | 86, 87 | fmptd 7134 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))):ℝ+⟶ℝ+) |
| 89 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑥 ∈
ℝ+) |
| 90 | 89 | rprege0d 13084 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
| 91 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑦 ∈
ℝ+) |
| 92 | 91 | rprege0d 13084 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑦 ∈ ℝ
∧ 0 ≤ 𝑦)) |
| 93 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (1 / (♯‘𝐴)) ∈ ℂ) |
| 94 | | mulcxp 26727 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) ∧ (𝑦 ∈ ℝ ∧ 0 ≤
𝑦) ∧ (1 /
(♯‘𝐴)) ∈
ℂ) → ((𝑥
· 𝑦)↑𝑐(1 /
(♯‘𝐴))) =
((𝑥↑𝑐(1 /
(♯‘𝐴)))
· (𝑦↑𝑐(1 /
(♯‘𝐴))))) |
| 95 | 90, 92, 93, 94 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑥 · 𝑦)↑𝑐(1 /
(♯‘𝐴))) =
((𝑥↑𝑐(1 /
(♯‘𝐴)))
· (𝑦↑𝑐(1 /
(♯‘𝐴))))) |
| 96 | | rpmulcl 13058 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → (𝑥 · 𝑦) ∈
ℝ+) |
| 97 | 96 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑥 · 𝑦) ∈
ℝ+) |
| 98 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑘 = (𝑥 · 𝑦) → (𝑘↑𝑐(1 /
(♯‘𝐴))) =
((𝑥 · 𝑦)↑𝑐(1 /
(♯‘𝐴)))) |
| 99 | | ovex 7464 |
. . . . . . . . 9
⊢ (𝑘↑𝑐(1 /
(♯‘𝐴))) ∈
V |
| 100 | 98, 87, 99 | fvmpt3i 7021 |
. . . . . . . 8
⊢ ((𝑥 · 𝑦) ∈ ℝ+ → ((𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘(𝑥 · 𝑦)) = ((𝑥 · 𝑦)↑𝑐(1 /
(♯‘𝐴)))) |
| 101 | 97, 100 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘(𝑥 · 𝑦)) = ((𝑥 · 𝑦)↑𝑐(1 /
(♯‘𝐴)))) |
| 102 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑥 → (𝑘↑𝑐(1 /
(♯‘𝐴))) =
(𝑥↑𝑐(1 /
(♯‘𝐴)))) |
| 103 | 102, 87, 99 | fvmpt3i 7021 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘𝑥) = (𝑥↑𝑐(1 /
(♯‘𝐴)))) |
| 104 | 89, 103 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘𝑥) = (𝑥↑𝑐(1 /
(♯‘𝐴)))) |
| 105 | | oveq1 7438 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → (𝑘↑𝑐(1 /
(♯‘𝐴))) =
(𝑦↑𝑐(1 /
(♯‘𝐴)))) |
| 106 | 105, 87, 99 | fvmpt3i 7021 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘𝑦) = (𝑦↑𝑐(1 /
(♯‘𝐴)))) |
| 107 | 91, 106 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘𝑦) = (𝑦↑𝑐(1 /
(♯‘𝐴)))) |
| 108 | 104, 107 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘𝑥) · ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘𝑦)) = ((𝑥↑𝑐(1 /
(♯‘𝐴)))
· (𝑦↑𝑐(1 /
(♯‘𝐴))))) |
| 109 | 95, 101, 108 | 3eqtr4d 2787 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘(𝑥 · 𝑦)) = (((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘𝑥) · ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘𝑦))) |
| 110 | 36, 36, 70, 70, 83, 83, 88, 109 | isghmd 19243 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))) ∈
((𝑀 ↾s
ℝ+) GrpHom (𝑀 ↾s
ℝ+))) |
| 111 | | ghmmhm 19244 |
. . . . 5
⊢ ((𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))) ∈
((𝑀 ↾s
ℝ+) GrpHom (𝑀 ↾s ℝ+))
→ (𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))) ∈
((𝑀 ↾s
ℝ+) MndHom (𝑀 ↾s
ℝ+))) |
| 112 | 110, 111 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))) ∈
((𝑀 ↾s
ℝ+) MndHom (𝑀 ↾s
ℝ+))) |
| 113 | | 1red 11262 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
| 114 | 4, 2, 113 | fdmfifsupp 9415 |
. . . 4
⊢ (𝜑 → 𝐹 finSupp 1) |
| 115 | 36, 57, 64, 62, 2, 112, 4, 114 | gsummhm 19956 |
. . 3
⊢ (𝜑 → ((𝑀 ↾s ℝ+)
Σg ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))
∘ 𝐹)) = ((𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘((𝑀 ↾s ℝ+)
Σg 𝐹))) |
| 116 | 53 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ+ ∈
(SubMnd‘𝑀)) |
| 117 | 4 | ffvelcdmda 7104 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
| 118 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (♯‘𝐴)) ∈
ℝ) |
| 119 | 117, 118 | rpcxpcld 26775 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴))) ∈
ℝ+) |
| 120 | | eqid 2737 |
. . . . . 6
⊢ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴)))) =
(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴)))) |
| 121 | 119, 120 | fmptd 7134 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴)))):𝐴⟶ℝ+) |
| 122 | 2, 116, 121, 32 | gsumsubm 18848 |
. . . 4
⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴))))) =
((𝑀 ↾s
ℝ+) Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴)))))) |
| 123 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (♯‘𝐴)) ∈
ℝ+) |
| 124 | 4 | feqmptd 6977 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
| 125 | 2, 117, 123, 124, 13 | offval2 7717 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘f
↑𝑐(𝐴 × {(1 / (♯‘𝐴))})) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴))))) |
| 126 | 125 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f
↑𝑐(𝐴 × {(1 / (♯‘𝐴))}))) = (𝑀 Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴)))))) |
| 127 | 102 | cbvmptv 5255 |
. . . . . . 7
⊢ (𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))) =
(𝑥 ∈
ℝ+ ↦ (𝑥↑𝑐(1 /
(♯‘𝐴)))) |
| 128 | 127 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴)))) =
(𝑥 ∈
ℝ+ ↦ (𝑥↑𝑐(1 /
(♯‘𝐴))))) |
| 129 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝑘) → (𝑥↑𝑐(1 /
(♯‘𝐴))) =
((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴)))) |
| 130 | 117, 124,
128, 129 | fmptco 7149 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))
∘ 𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴))))) |
| 131 | 130 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → ((𝑀 ↾s ℝ+)
Σg ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))
∘ 𝐹)) = ((𝑀 ↾s
ℝ+) Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(♯‘𝐴)))))) |
| 132 | 122, 126,
131 | 3eqtr4rd 2788 |
. . 3
⊢ (𝜑 → ((𝑀 ↾s ℝ+)
Σg ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))
∘ 𝐹)) = (𝑀 Σg
(𝐹 ∘f
↑𝑐(𝐴 × {(1 / (♯‘𝐴))})))) |
| 133 | 36, 57, 64, 2, 4, 114 | gsumcl 19933 |
. . . . 5
⊢ (𝜑 → ((𝑀 ↾s ℝ+)
Σg 𝐹) ∈
ℝ+) |
| 134 | | oveq1 7438 |
. . . . . 6
⊢ (𝑘 = ((𝑀 ↾s ℝ+)
Σg 𝐹) → (𝑘↑𝑐(1 /
(♯‘𝐴))) =
(((𝑀 ↾s
ℝ+) Σg 𝐹)↑𝑐(1 /
(♯‘𝐴)))) |
| 135 | 134, 87, 99 | fvmpt3i 7021 |
. . . . 5
⊢ (((𝑀 ↾s
ℝ+) Σg 𝐹) ∈ ℝ+ → ((𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘((𝑀 ↾s ℝ+)
Σg 𝐹)) = (((𝑀 ↾s ℝ+)
Σg 𝐹)↑𝑐(1 /
(♯‘𝐴)))) |
| 136 | 133, 135 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘((𝑀 ↾s ℝ+)
Σg 𝐹)) = (((𝑀 ↾s ℝ+)
Σg 𝐹)↑𝑐(1 /
(♯‘𝐴)))) |
| 137 | 2, 116, 4, 32 | gsumsubm 18848 |
. . . . 5
⊢ (𝜑 → (𝑀 Σg 𝐹) = ((𝑀 ↾s ℝ+)
Σg 𝐹)) |
| 138 | 137 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) =
(((𝑀 ↾s
ℝ+) Σg 𝐹)↑𝑐(1 /
(♯‘𝐴)))) |
| 139 | 136, 138 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(♯‘𝐴))))‘((𝑀 ↾s ℝ+)
Σg 𝐹)) = ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴)))) |
| 140 | 115, 132,
139 | 3eqtr3d 2785 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘f
↑𝑐(𝐴 × {(1 / (♯‘𝐴))}))) = ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴)))) |
| 141 | 117 | rpcnd 13079 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ) |
| 142 | 2, 141 | fsumcl 15769 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) ∈ ℂ) |
| 143 | 142, 23, 24 | divrecd 12046 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) / (♯‘𝐴)) = (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) · (1 / (♯‘𝐴)))) |
| 144 | 2, 16, 141 | fsummulc1 15821 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) · (1 / (♯‘𝐴))) = Σ𝑘 ∈ 𝐴 ((𝐹‘𝑘) · (1 / (♯‘𝐴)))) |
| 145 | 143, 144 | eqtr2d 2778 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝐹‘𝑘) · (1 / (♯‘𝐴))) = (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) / (♯‘𝐴))) |
| 146 | 16 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (♯‘𝐴)) ∈
ℂ) |
| 147 | 141, 146 | mulcld 11281 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) · (1 / (♯‘𝐴))) ∈
ℂ) |
| 148 | 2, 147 | gsumfsum 21452 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) · (1 / (♯‘𝐴))))) = Σ𝑘 ∈ 𝐴 ((𝐹‘𝑘) · (1 / (♯‘𝐴)))) |
| 149 | 2, 141 | gsumfsum 21452 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘)) |
| 150 | 149 | oveq1d 7446 |
. . . 4
⊢ (𝜑 → ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) / (♯‘𝐴)) = (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) / (♯‘𝐴))) |
| 151 | 145, 148,
150 | 3eqtr4d 2787 |
. . 3
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) · (1 / (♯‘𝐴))))) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) / (♯‘𝐴))) |
| 152 | 2, 117, 146, 124, 13 | offval2 7717 |
. . . 4
⊢ (𝜑 → (𝐹 ∘f · (𝐴 × {(1 /
(♯‘𝐴))})) =
(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) · (1 / (♯‘𝐴))))) |
| 153 | 152 | oveq2d 7447 |
. . 3
⊢ (𝜑 → (ℂfld
Σg (𝐹 ∘f · (𝐴 × {(1 /
(♯‘𝐴))}))) =
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) · (1 / (♯‘𝐴)))))) |
| 154 | 124 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg 𝐹) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))) |
| 155 | 154 | oveq1d 7446 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (♯‘𝐴)) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) / (♯‘𝐴))) |
| 156 | 151, 153,
155 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 → (ℂfld
Σg (𝐹 ∘f · (𝐴 × {(1 /
(♯‘𝐴))}))) =
((ℂfld Σg 𝐹) / (♯‘𝐴))) |
| 157 | 28, 140, 156 | 3brtr3d 5174 |
1
⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(♯‘𝐴))) ≤
((ℂfld Σg 𝐹) / (♯‘𝐴))) |