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 13018 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
6 | 2, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
7 | 3, 6 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
8 | 7 | nnrpd 11746 |
. . . . 5
⊢ (𝜑 → (#‘𝐴) ∈
ℝ+) |
9 | 8 | rpreccld 11758 |
. . . 4
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ+) |
10 | | fconst6g 6007 |
. . . 4
⊢ ((1 /
(#‘𝐴)) ∈
ℝ+ → (𝐴 × {(1 / (#‘𝐴))}):𝐴⟶ℝ+) |
11 | 9, 10 | syl 17 |
. . 3
⊢ (𝜑 → (𝐴 × {(1 / (#‘𝐴))}):𝐴⟶ℝ+) |
12 | | fconstmpt 5085 |
. . . . . 6
⊢ (𝐴 × {(1 / (#‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴))) |
13 | 12 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 × {(1 / (#‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) |
14 | 13 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg (𝐴 × {(1 / (#‘𝐴))})) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴))))) |
15 | | hashnncl 13018 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
16 | 2, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
17 | 3, 16 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
18 | 17 | nnrecred 10943 |
. . . . . 6
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
19 | 18 | recnd 9947 |
. . . . 5
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℂ) |
20 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (1 /
(#‘𝐴)) ∈
ℂ) → 𝐴 ∈
Fin) |
21 | | simplr 788 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ (1 /
(#‘𝐴)) ∈
ℂ) ∧ 𝑘 ∈
𝐴) → (1 /
(#‘𝐴)) ∈
ℂ) |
22 | 20, 21 | gsumfsum 19632 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ (1 /
(#‘𝐴)) ∈
ℂ) → (ℂfld Σg (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) = Σ𝑘 ∈ 𝐴 (1 / (#‘𝐴))) |
23 | 2, 19, 22 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) = Σ𝑘 ∈ 𝐴 (1 / (#‘𝐴))) |
24 | | hashnncl 13018 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
25 | 2, 24 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
26 | 3, 25 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
27 | 26 | nnrecred 10943 |
. . . . . . 7
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
28 | 27 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℂ) |
29 | | fsumconst 14364 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ (1 /
(#‘𝐴)) ∈
ℂ) → Σ𝑘
∈ 𝐴 (1 /
(#‘𝐴)) =
((#‘𝐴) · (1 /
(#‘𝐴)))) |
30 | 2, 28, 29 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (1 / (#‘𝐴)) = ((#‘𝐴) · (1 / (#‘𝐴)))) |
31 | | hashnncl 13018 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
32 | 2, 31 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
33 | 3, 32 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
34 | 33 | nncnd 10913 |
. . . . . 6
⊢ (𝜑 → (#‘𝐴) ∈ ℂ) |
35 | | hashnncl 13018 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
36 | 2, 35 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
37 | 3, 36 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
38 | 37 | nnne0d 10942 |
. . . . . 6
⊢ (𝜑 → (#‘𝐴) ≠ 0) |
39 | 34, 38 | recidd 10675 |
. . . . 5
⊢ (𝜑 → ((#‘𝐴) · (1 / (#‘𝐴))) = 1) |
40 | 30, 39 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (1 / (#‘𝐴)) = 1) |
41 | 14, 23, 40 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (ℂfld
Σg (𝐴 × {(1 / (#‘𝐴))})) = 1) |
42 | 1, 2, 3, 4, 11, 41 | amgmwlem 42357 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓
↑𝑐(𝐴 × {(1 / (#‘𝐴))}))) ≤ (ℂfld
Σg (𝐹 ∘𝑓 · (𝐴 × {(1 / (#‘𝐴))})))) |
43 | | rpssre 11719 |
. . . . . 6
⊢
ℝ+ ⊆ ℝ |
44 | | ax-resscn 9872 |
. . . . . 6
⊢ ℝ
⊆ ℂ |
45 | 43, 44 | sstri 3577 |
. . . . 5
⊢
ℝ+ ⊆ ℂ |
46 | | eqid 2610 |
. . . . . 6
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
47 | | cnfldbas 19571 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
48 | 1, 47 | mgpbas 18318 |
. . . . . 6
⊢ ℂ =
(Base‘𝑀) |
49 | 46, 48 | ressbas2 15758 |
. . . . 5
⊢
(ℝ+ ⊆ ℂ → ℝ+ =
(Base‘(𝑀
↾s ℝ+))) |
50 | 45, 49 | ax-mp 5 |
. . . 4
⊢
ℝ+ = (Base‘(𝑀 ↾s
ℝ+)) |
51 | | cnfld1 19590 |
. . . . . 6
⊢ 1 =
(1r‘ℂfld) |
52 | 1, 51 | ringidval 18326 |
. . . . 5
⊢ 1 =
(0g‘𝑀) |
53 | 1 | oveq1i 6559 |
. . . . . . . . . 10
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
54 | 53 | rpmsubg 19629 |
. . . . . . . . 9
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
55 | | subgsubm 17439 |
. . . . . . . . 9
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . 8
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
57 | | cnring 19587 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
58 | | cnfld0 19589 |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘ℂfld) |
59 | | cndrng 19594 |
. . . . . . . . . . . 12
⊢
ℂfld ∈ DivRing |
60 | 47, 58, 59 | drngui 18576 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
61 | 60, 1 | unitsubm 18493 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
62 | 57, 61 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ∈ (SubMnd‘𝑀) |
63 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
64 | 63 | subsubm 17180 |
. . . . . . . . 9
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
65 | 62, 64 | ax-mp 5 |
. . . . . . . 8
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
66 | 56, 65 | mpbi 219 |
. . . . . . 7
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
67 | 66 | simpli 473 |
. . . . . 6
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
68 | | eqid 2610 |
. . . . . . 7
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
69 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑀) = (0g‘𝑀) |
70 | 68, 69 | subm0 17179 |
. . . . . 6
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (0g‘𝑀) = (0g‘(𝑀 ↾s
ℝ+))) |
71 | 67, 70 | ax-mp 5 |
. . . . 5
⊢
(0g‘𝑀) = (0g‘(𝑀 ↾s
ℝ+)) |
72 | 52, 71 | eqtri 2632 |
. . . 4
⊢ 1 =
(0g‘(𝑀
↾s ℝ+)) |
73 | | cncrng 19586 |
. . . . . 6
⊢
ℂfld ∈ CRing |
74 | 1 | crngmgp 18378 |
. . . . . 6
⊢
(ℂfld ∈ CRing → 𝑀 ∈ CMnd) |
75 | 73, 74 | ax-mp 5 |
. . . . 5
⊢ 𝑀 ∈ CMnd |
76 | 1 | oveq1i 6559 |
. . . . . . . . . 10
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
77 | 76 | rpmsubg 19629 |
. . . . . . . . 9
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
78 | | subgsubm 17439 |
. . . . . . . . 9
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
79 | 77, 78 | ax-mp 5 |
. . . . . . . 8
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
80 | 47, 58, 59 | drngui 18576 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
81 | 80, 1 | unitsubm 18493 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
82 | 57, 81 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ∈ (SubMnd‘𝑀) |
83 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
84 | 83 | subsubm 17180 |
. . . . . . . . 9
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
85 | 82, 84 | ax-mp 5 |
. . . . . . . 8
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
86 | 79, 85 | mpbi 219 |
. . . . . . 7
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
87 | 86 | simpli 473 |
. . . . . 6
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
88 | | eqid 2610 |
. . . . . . 7
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
89 | 88 | submmnd 17177 |
. . . . . 6
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+)
∈ Mnd) |
90 | 87, 89 | mp1i 13 |
. . . . 5
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Mnd) |
91 | | eqid 2610 |
. . . . . 6
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
92 | 91 | subcmn 18065 |
. . . . 5
⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾s
ℝ+) ∈ Mnd) → (𝑀 ↾s ℝ+)
∈ CMnd) |
93 | 75, 90, 92 | sylancr 694 |
. . . 4
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ CMnd) |
94 | 1 | oveq1i 6559 |
. . . . . . . . 9
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
95 | 94 | rpmsubg 19629 |
. . . . . . . 8
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
96 | | subgsubm 17439 |
. . . . . . . 8
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
97 | 95, 96 | ax-mp 5 |
. . . . . . 7
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
98 | 47, 58, 59 | drngui 18576 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
99 | 98, 1 | unitsubm 18493 |
. . . . . . . . 9
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
100 | 57, 99 | ax-mp 5 |
. . . . . . . 8
⊢ (ℂ
∖ {0}) ∈ (SubMnd‘𝑀) |
101 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
102 | 101 | subsubm 17180 |
. . . . . . . 8
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
103 | 100, 102 | ax-mp 5 |
. . . . . . 7
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
104 | 97, 103 | mpbi 219 |
. . . . . 6
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
105 | 104 | simpli 473 |
. . . . 5
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
106 | | eqid 2610 |
. . . . . 6
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
107 | 106 | submmnd 17177 |
. . . . 5
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+)
∈ Mnd) |
108 | 105, 107 | mp1i 13 |
. . . 4
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Mnd) |
109 | 43, 44 | sstri 3577 |
. . . . . . 7
⊢
ℝ+ ⊆ ℂ |
110 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
111 | 1, 47 | mgpbas 18318 |
. . . . . . . 8
⊢ ℂ =
(Base‘𝑀) |
112 | 110, 111 | ressbas2 15758 |
. . . . . . 7
⊢
(ℝ+ ⊆ ℂ → ℝ+ =
(Base‘(𝑀
↾s ℝ+))) |
113 | 109, 112 | ax-mp 5 |
. . . . . 6
⊢
ℝ+ = (Base‘(𝑀 ↾s
ℝ+)) |
114 | 43, 44 | sstri 3577 |
. . . . . . 7
⊢
ℝ+ ⊆ ℂ |
115 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
116 | 1, 47 | mgpbas 18318 |
. . . . . . . 8
⊢ ℂ =
(Base‘𝑀) |
117 | 115, 116 | ressbas2 15758 |
. . . . . . 7
⊢
(ℝ+ ⊆ ℂ → ℝ+ =
(Base‘(𝑀
↾s ℝ+))) |
118 | 114, 117 | ax-mp 5 |
. . . . . 6
⊢
ℝ+ = (Base‘(𝑀 ↾s
ℝ+)) |
119 | | reex 9906 |
. . . . . . . 8
⊢ ℝ
∈ V |
120 | 119, 43 | ssexi 4731 |
. . . . . . 7
⊢
ℝ+ ∈ V |
121 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
122 | | cnfldmul 19573 |
. . . . . . . . 9
⊢ ·
= (.r‘ℂfld) |
123 | 1, 122 | mgpplusg 18316 |
. . . . . . . 8
⊢ ·
= (+g‘𝑀) |
124 | 121, 123 | ressplusg 15818 |
. . . . . . 7
⊢
(ℝ+ ∈ V → · =
(+g‘(𝑀
↾s ℝ+))) |
125 | 120, 124 | ax-mp 5 |
. . . . . 6
⊢ ·
= (+g‘(𝑀
↾s ℝ+)) |
126 | 119, 43 | ssexi 4731 |
. . . . . . 7
⊢
ℝ+ ∈ V |
127 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
128 | 1, 122 | mgpplusg 18316 |
. . . . . . . 8
⊢ ·
= (+g‘𝑀) |
129 | 127, 128 | ressplusg 15818 |
. . . . . . 7
⊢
(ℝ+ ∈ V → · =
(+g‘(𝑀
↾s ℝ+))) |
130 | 126, 129 | ax-mp 5 |
. . . . . 6
⊢ ·
= (+g‘(𝑀
↾s ℝ+)) |
131 | | eqid 2610 |
. . . . . . . 8
⊢
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
132 | 131 | rpmsubg 19629 |
. . . . . . 7
⊢
ℝ+ ∈
(SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) |
133 | 1 | oveq1i 6559 |
. . . . . . . . 9
⊢ (𝑀 ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+) |
134 | | cnex 9896 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
135 | | difss 3699 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) ⊆ ℂ |
136 | 134, 135 | ssexi 4731 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) ∈ V |
137 | | rpcndif0 11727 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ+
→ 𝑤 ∈ (ℂ
∖ {0})) |
138 | 137 | ssriv 3572 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ (ℂ ∖ {0}) |
139 | | ressabs 15766 |
. . . . . . . . . 10
⊢
(((ℂ ∖ {0}) ∈ V ∧ ℝ+ ⊆
(ℂ ∖ {0})) → (((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})) ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+)) |
140 | 136, 138,
139 | mp2an 704 |
. . . . . . . . 9
⊢
(((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) ↾s ℝ+) =
((mulGrp‘ℂfld) ↾s
ℝ+) |
141 | 133, 140 | eqtr4i 2635 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})) ↾s
ℝ+) |
142 | 141 | subggrp 17420 |
. . . . . . 7
⊢
(ℝ+ ∈
(SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) → (𝑀 ↾s ℝ+)
∈ Grp) |
143 | 132, 142 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Grp) |
144 | | eqid 2610 |
. . . . . . . 8
⊢
((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
145 | 144 | rpmsubg 19629 |
. . . . . . 7
⊢
ℝ+ ∈
(SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) |
146 | 1 | oveq1i 6559 |
. . . . . . . . 9
⊢ (𝑀 ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+) |
147 | | difss 3699 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) ⊆ ℂ |
148 | 134, 147 | ssexi 4731 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) ∈ V |
149 | | rpcndif0 11727 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ℝ+
→ 𝑤 ∈ (ℂ
∖ {0})) |
150 | 149 | ssriv 3572 |
. . . . . . . . . 10
⊢
ℝ+ ⊆ (ℂ ∖ {0}) |
151 | | ressabs 15766 |
. . . . . . . . . 10
⊢
(((ℂ ∖ {0}) ∈ V ∧ ℝ+ ⊆
(ℂ ∖ {0})) → (((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})) ↾s
ℝ+) = ((mulGrp‘ℂfld)
↾s ℝ+)) |
152 | 148, 150,
151 | mp2an 704 |
. . . . . . . . 9
⊢
(((mulGrp‘ℂfld) ↾s (ℂ
∖ {0})) ↾s ℝ+) =
((mulGrp‘ℂfld) ↾s
ℝ+) |
153 | 146, 152 | eqtr4i 2635 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (((mulGrp‘ℂfld)
↾s (ℂ ∖ {0})) ↾s
ℝ+) |
154 | 153 | subggrp 17420 |
. . . . . . 7
⊢
(ℝ+ ∈
(SubGrp‘((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0}))) → (𝑀 ↾s ℝ+)
∈ Grp) |
155 | 145, 154 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Grp) |
156 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ+) → 𝑘 ∈
ℝ+) |
157 | | hashnncl 13018 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
158 | 2, 157 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
159 | 3, 158 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
160 | 159 | nnrecred 10943 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
161 | 160 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ+) → (1 /
(#‘𝐴)) ∈
ℝ) |
162 | 156, 161 | rpcxpcld 24276 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℝ+) → (𝑘↑𝑐(1 /
(#‘𝐴))) ∈
ℝ+) |
163 | | eqid 2610 |
. . . . . . 7
⊢ (𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) |
164 | 162, 163 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))):ℝ+⟶ℝ+) |
165 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑥 ∈
ℝ+) |
166 | 165 | rprege0d 11755 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
167 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑦 ∈
ℝ+) |
168 | 167 | rprege0d 11755 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑦 ∈ ℝ
∧ 0 ≤ 𝑦)) |
169 | | hashnncl 13018 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
170 | 2, 169 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
171 | 3, 170 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
172 | 171 | nnrecred 10943 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
173 | 172 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℂ) |
174 | 173 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (1 / (#‘𝐴))
∈ ℂ) |
175 | | mulcxp 24231 |
. . . . . . . 8
⊢ (((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) ∧ (𝑦 ∈ ℝ ∧ 0 ≤
𝑦) ∧ (1 /
(#‘𝐴)) ∈
ℂ) → ((𝑥
· 𝑦)↑𝑐(1 /
(#‘𝐴))) = ((𝑥↑𝑐(1 /
(#‘𝐴))) ·
(𝑦↑𝑐(1 / (#‘𝐴))))) |
176 | 166, 168,
174, 175 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑥 · 𝑦)↑𝑐(1 /
(#‘𝐴))) = ((𝑥↑𝑐(1 /
(#‘𝐴))) ·
(𝑦↑𝑐(1 / (#‘𝐴))))) |
177 | | rpmulcl 11731 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → (𝑥 · 𝑦) ∈
ℝ+) |
178 | 177 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (𝑥 · 𝑦) ∈
ℝ+) |
179 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑘 = (𝑥 · 𝑦) → (𝑘↑𝑐(1 / (#‘𝐴))) = ((𝑥 · 𝑦)↑𝑐(1 /
(#‘𝐴)))) |
180 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) |
181 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑘↑𝑐(1 /
(#‘𝐴))) ∈
V |
182 | 179, 180,
181 | fvmpt3i 6196 |
. . . . . . . 8
⊢ ((𝑥 · 𝑦) ∈ ℝ+ → ((𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘(𝑥 · 𝑦)) = ((𝑥 · 𝑦)↑𝑐(1 /
(#‘𝐴)))) |
183 | 178, 182 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘(𝑥 · 𝑦)) = ((𝑥 · 𝑦)↑𝑐(1 /
(#‘𝐴)))) |
184 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑥 ∈
ℝ+) |
185 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑥 → (𝑘↑𝑐(1 / (#‘𝐴))) = (𝑥↑𝑐(1 / (#‘𝐴)))) |
186 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) |
187 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑘↑𝑐(1 /
(#‘𝐴))) ∈
V |
188 | 185, 186,
187 | fvmpt3i 6196 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘𝑥) = (𝑥↑𝑐(1 / (#‘𝐴)))) |
189 | 184, 188 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘𝑥) = (𝑥↑𝑐(1 / (#‘𝐴)))) |
190 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ 𝑦 ∈
ℝ+) |
191 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → (𝑘↑𝑐(1 / (#‘𝐴))) = (𝑦↑𝑐(1 / (#‘𝐴)))) |
192 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) |
193 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑘↑𝑐(1 /
(#‘𝐴))) ∈
V |
194 | 191, 192,
193 | fvmpt3i 6196 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ+
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘𝑦) = (𝑦↑𝑐(1 / (#‘𝐴)))) |
195 | 190, 194 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘𝑦) = (𝑦↑𝑐(1 / (#‘𝐴)))) |
196 | 189, 195 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ (((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘𝑥) · ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴))))‘𝑦)) = ((𝑥↑𝑐(1 / (#‘𝐴))) · (𝑦↑𝑐(1 / (#‘𝐴))))) |
197 | 176, 183,
196 | 3eqtr4d 2654 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑦 ∈ ℝ+))
→ ((𝑘 ∈
ℝ+ ↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘(𝑥 · 𝑦)) = (((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴))))‘𝑥) · ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴))))‘𝑦))) |
198 | 113, 118,
125, 130, 143, 155, 164, 197 | isghmd 17492 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) ∈
((𝑀 ↾s
ℝ+) GrpHom (𝑀 ↾s
ℝ+))) |
199 | | ghmmhm 17493 |
. . . . 5
⊢ ((𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴)))) ∈ ((𝑀 ↾s ℝ+)
GrpHom (𝑀
↾s ℝ+)) → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) ∈
((𝑀 ↾s
ℝ+) MndHom (𝑀 ↾s
ℝ+))) |
200 | 198, 199 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) ∈
((𝑀 ↾s
ℝ+) MndHom (𝑀 ↾s
ℝ+))) |
201 | | 1red 9934 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
202 | 4, 2, 201 | fdmfifsupp 8168 |
. . . 4
⊢ (𝜑 → 𝐹 finSupp 1) |
203 | 50, 72, 93, 108, 2, 200, 4, 202 | gsummhm 18161 |
. . 3
⊢ (𝜑 → ((𝑀 ↾s ℝ+)
Σg ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) ∘
𝐹)) = ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴))))‘((𝑀 ↾s ℝ+)
Σg 𝐹))) |
204 | 1 | oveq1i 6559 |
. . . . . . . . . 10
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
205 | 204 | rpmsubg 19629 |
. . . . . . . . 9
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
206 | | subgsubm 17439 |
. . . . . . . . 9
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
207 | 205, 206 | ax-mp 5 |
. . . . . . . 8
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
208 | 47, 58, 59 | drngui 18576 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
209 | 208, 1 | unitsubm 18493 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
210 | 57, 209 | ax-mp 5 |
. . . . . . . . 9
⊢ (ℂ
∖ {0}) ∈ (SubMnd‘𝑀) |
211 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
212 | 211 | subsubm 17180 |
. . . . . . . . 9
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
213 | 210, 212 | ax-mp 5 |
. . . . . . . 8
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
214 | 207, 213 | mpbi 219 |
. . . . . . 7
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
215 | 214 | simpli 473 |
. . . . . 6
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
216 | 215 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℝ+ ∈
(SubMnd‘𝑀)) |
217 | 4 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
218 | | hashnncl 13018 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
219 | 2, 218 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
220 | 3, 219 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
221 | 220 | nnrecred 10943 |
. . . . . . . 8
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
222 | 221 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (#‘𝐴)) ∈ ℝ) |
223 | 217, 222 | rpcxpcld 24276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴))) ∈
ℝ+) |
224 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴)))) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴)))) |
225 | 223, 224 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴)))):𝐴⟶ℝ+) |
226 | | eqid 2610 |
. . . . 5
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
227 | 2, 216, 225, 226 | gsumsubm 17196 |
. . . 4
⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴))))) = ((𝑀 ↾s
ℝ+) Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴)))))) |
228 | 4 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
229 | | hashnncl 13018 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
230 | 2, 229 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
231 | 3, 230 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
232 | 231 | nnrpd 11746 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝐴) ∈
ℝ+) |
233 | 232 | rpreccld 11758 |
. . . . . . 7
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ+) |
234 | 233 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (#‘𝐴)) ∈
ℝ+) |
235 | 4 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
236 | | fconstmpt 5085 |
. . . . . . 7
⊢ (𝐴 × {(1 / (#‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴))) |
237 | 236 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 × {(1 / (#‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) |
238 | 2, 228, 234, 235, 237 | offval2 6812 |
. . . . 5
⊢ (𝜑 → (𝐹 ∘𝑓
↑𝑐(𝐴 × {(1 / (#‘𝐴))})) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴))))) |
239 | 238 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓
↑𝑐(𝐴 × {(1 / (#‘𝐴))}))) = (𝑀 Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴)))))) |
240 | 4 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
241 | 4 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
242 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑘 = 𝑥 → (𝑘↑𝑐(1 / (#‘𝐴))) = (𝑥↑𝑐(1 / (#‘𝐴)))) |
243 | 242 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴)))) = (𝑥 ∈ ℝ+ ↦ (𝑥↑𝑐(1 /
(#‘𝐴)))) |
244 | 243 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) = (𝑥 ∈ ℝ+
↦ (𝑥↑𝑐(1 / (#‘𝐴))))) |
245 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = (𝐹‘𝑘) → (𝑥↑𝑐(1 / (#‘𝐴))) = ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴)))) |
246 | 240, 241,
244, 245 | fmptco 6303 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) ∘
𝐹) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴))))) |
247 | 246 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → ((𝑀 ↾s ℝ+)
Σg ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) ∘
𝐹)) = ((𝑀 ↾s ℝ+)
Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘)↑𝑐(1 /
(#‘𝐴)))))) |
248 | 227, 239,
247 | 3eqtr4rd 2655 |
. . 3
⊢ (𝜑 → ((𝑀 ↾s ℝ+)
Σg ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) ∘
𝐹)) = (𝑀 Σg (𝐹 ∘𝑓
↑𝑐(𝐴 × {(1 / (#‘𝐴))})))) |
249 | 43, 44 | sstri 3577 |
. . . . . . 7
⊢
ℝ+ ⊆ ℂ |
250 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
251 | 1, 47 | mgpbas 18318 |
. . . . . . . 8
⊢ ℂ =
(Base‘𝑀) |
252 | 250, 251 | ressbas2 15758 |
. . . . . . 7
⊢
(ℝ+ ⊆ ℂ → ℝ+ =
(Base‘(𝑀
↾s ℝ+))) |
253 | 249, 252 | ax-mp 5 |
. . . . . 6
⊢
ℝ+ = (Base‘(𝑀 ↾s
ℝ+)) |
254 | 1, 51 | ringidval 18326 |
. . . . . . 7
⊢ 1 =
(0g‘𝑀) |
255 | 1 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
256 | 255 | rpmsubg 19629 |
. . . . . . . . . . 11
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
257 | | subgsubm 17439 |
. . . . . . . . . . 11
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
258 | 256, 257 | ax-mp 5 |
. . . . . . . . . 10
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
259 | 47, 58, 59 | drngui 18576 |
. . . . . . . . . . . . 13
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
260 | 259, 1 | unitsubm 18493 |
. . . . . . . . . . . 12
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
261 | 57, 260 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) ∈ (SubMnd‘𝑀) |
262 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
263 | 262 | subsubm 17180 |
. . . . . . . . . . 11
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
264 | 261, 263 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
265 | 258, 264 | mpbi 219 |
. . . . . . . . 9
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
266 | 265 | simpli 473 |
. . . . . . . 8
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
267 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
268 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝑀) = (0g‘𝑀) |
269 | 267, 268 | subm0 17179 |
. . . . . . . 8
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (0g‘𝑀) = (0g‘(𝑀 ↾s
ℝ+))) |
270 | 266, 269 | ax-mp 5 |
. . . . . . 7
⊢
(0g‘𝑀) = (0g‘(𝑀 ↾s
ℝ+)) |
271 | 254, 270 | eqtri 2632 |
. . . . . 6
⊢ 1 =
(0g‘(𝑀
↾s ℝ+)) |
272 | 1 | crngmgp 18378 |
. . . . . . . 8
⊢
(ℂfld ∈ CRing → 𝑀 ∈ CMnd) |
273 | 73, 272 | ax-mp 5 |
. . . . . . 7
⊢ 𝑀 ∈ CMnd |
274 | 1 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
275 | 274 | rpmsubg 19629 |
. . . . . . . . . . 11
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
276 | | subgsubm 17439 |
. . . . . . . . . . 11
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
277 | 275, 276 | ax-mp 5 |
. . . . . . . . . 10
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
278 | 47, 58, 59 | drngui 18576 |
. . . . . . . . . . . . 13
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
279 | 278, 1 | unitsubm 18493 |
. . . . . . . . . . . 12
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
280 | 57, 279 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℂ
∖ {0}) ∈ (SubMnd‘𝑀) |
281 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
282 | 281 | subsubm 17180 |
. . . . . . . . . . 11
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
283 | 280, 282 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
284 | 277, 283 | mpbi 219 |
. . . . . . . . 9
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
285 | 284 | simpli 473 |
. . . . . . . 8
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
286 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
287 | 286 | submmnd 17177 |
. . . . . . . 8
⊢
(ℝ+ ∈ (SubMnd‘𝑀) → (𝑀 ↾s ℝ+)
∈ Mnd) |
288 | 285, 287 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ Mnd) |
289 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
290 | 289 | subcmn 18065 |
. . . . . . 7
⊢ ((𝑀 ∈ CMnd ∧ (𝑀 ↾s
ℝ+) ∈ Mnd) → (𝑀 ↾s ℝ+)
∈ CMnd) |
291 | 273, 288,
290 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → (𝑀 ↾s ℝ+)
∈ CMnd) |
292 | | 1red 9934 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
293 | 4, 2, 292 | fdmfifsupp 8168 |
. . . . . 6
⊢ (𝜑 → 𝐹 finSupp 1) |
294 | 253, 271,
291, 2, 4, 293 | gsumcl 18139 |
. . . . 5
⊢ (𝜑 → ((𝑀 ↾s ℝ+)
Σg 𝐹) ∈
ℝ+) |
295 | | oveq1 6556 |
. . . . . 6
⊢ (𝑘 = ((𝑀 ↾s ℝ+)
Σg 𝐹) → (𝑘↑𝑐(1 / (#‘𝐴))) = (((𝑀 ↾s ℝ+)
Σg 𝐹)↑𝑐(1 /
(#‘𝐴)))) |
296 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴)))) = (𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴)))) |
297 | | ovex 6577 |
. . . . . 6
⊢ (𝑘↑𝑐(1 /
(#‘𝐴))) ∈
V |
298 | 295, 296,
297 | fvmpt3i 6196 |
. . . . 5
⊢ (((𝑀 ↾s
ℝ+) Σg 𝐹) ∈ ℝ+ → ((𝑘 ∈ ℝ+
↦ (𝑘↑𝑐(1 / (#‘𝐴))))‘((𝑀 ↾s ℝ+)
Σg 𝐹)) = (((𝑀 ↾s ℝ+)
Σg 𝐹)↑𝑐(1 /
(#‘𝐴)))) |
299 | 294, 298 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴))))‘((𝑀 ↾s ℝ+)
Σg 𝐹)) = (((𝑀 ↾s ℝ+)
Σg 𝐹)↑𝑐(1 /
(#‘𝐴)))) |
300 | 1 | oveq1i 6559 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s (ℂ
∖ {0})) = ((mulGrp‘ℂfld) ↾s
(ℂ ∖ {0})) |
301 | 300 | rpmsubg 19629 |
. . . . . . . . . 10
⊢
ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖
{0}))) |
302 | | subgsubm 17439 |
. . . . . . . . . 10
⊢
(ℝ+ ∈ (SubGrp‘(𝑀 ↾s (ℂ ∖ {0})))
→ ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0})))) |
303 | 301, 302 | ax-mp 5 |
. . . . . . . . 9
⊢
ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖
{0}))) |
304 | 47, 58, 59 | drngui 18576 |
. . . . . . . . . . . 12
⊢ (ℂ
∖ {0}) = (Unit‘ℂfld) |
305 | 304, 1 | unitsubm 18493 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ Ring → (ℂ ∖ {0}) ∈
(SubMnd‘𝑀)) |
306 | 57, 305 | ax-mp 5 |
. . . . . . . . . 10
⊢ (ℂ
∖ {0}) ∈ (SubMnd‘𝑀) |
307 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s (ℂ
∖ {0})) = (𝑀
↾s (ℂ ∖ {0})) |
308 | 307 | subsubm 17180 |
. . . . . . . . . 10
⊢ ((ℂ
∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈
(SubMnd‘(𝑀
↾s (ℂ ∖ {0}))) ↔ (ℝ+ ∈
(SubMnd‘𝑀) ∧
ℝ+ ⊆ (ℂ ∖ {0})))) |
309 | 306, 308 | ax-mp 5 |
. . . . . . . . 9
⊢
(ℝ+ ∈ (SubMnd‘(𝑀 ↾s (ℂ ∖ {0})))
↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0}))) |
310 | 303, 309 | mpbi 219 |
. . . . . . . 8
⊢
(ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ
∖ {0})) |
311 | 310 | simpli 473 |
. . . . . . 7
⊢
ℝ+ ∈ (SubMnd‘𝑀) |
312 | 311 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℝ+ ∈
(SubMnd‘𝑀)) |
313 | | eqid 2610 |
. . . . . 6
⊢ (𝑀 ↾s
ℝ+) = (𝑀
↾s ℝ+) |
314 | 2, 312, 4, 313 | gsumsubm 17196 |
. . . . 5
⊢ (𝜑 → (𝑀 Σg 𝐹) = ((𝑀 ↾s ℝ+)
Σg 𝐹)) |
315 | 314 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) = (((𝑀 ↾s
ℝ+) Σg 𝐹)↑𝑐(1 /
(#‘𝐴)))) |
316 | 299, 315 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → ((𝑘 ∈ ℝ+ ↦ (𝑘↑𝑐(1 /
(#‘𝐴))))‘((𝑀 ↾s ℝ+)
Σg 𝐹)) = ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴)))) |
317 | 203, 248,
316 | 3eqtr3d 2652 |
. 2
⊢ (𝜑 → (𝑀 Σg (𝐹 ∘𝑓
↑𝑐(𝐴 × {(1 / (#‘𝐴))}))) = ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴)))) |
318 | 4 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
319 | 318 | rpcnd 11750 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ) |
320 | 2, 319 | fsumcl 14311 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) ∈ ℂ) |
321 | | hashnncl 13018 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
322 | 2, 321 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
323 | 3, 322 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
324 | 323 | nncnd 10913 |
. . . . . 6
⊢ (𝜑 → (#‘𝐴) ∈ ℂ) |
325 | | hashnncl 13018 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
326 | 2, 325 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
327 | 3, 326 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
328 | 327 | nnne0d 10942 |
. . . . . 6
⊢ (𝜑 → (#‘𝐴) ≠ 0) |
329 | 320, 324,
328 | divrecd 10683 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) / (#‘𝐴)) = (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) · (1 / (#‘𝐴)))) |
330 | | hashnncl 13018 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
331 | 2, 330 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
332 | 3, 331 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
333 | 332 | nnrecred 10943 |
. . . . . . 7
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
334 | 333 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℂ) |
335 | 4 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
336 | 335 | rpcnd 11750 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ) |
337 | 2, 334, 336 | fsummulc1 14359 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) · (1 / (#‘𝐴))) = Σ𝑘 ∈ 𝐴 ((𝐹‘𝑘) · (1 / (#‘𝐴)))) |
338 | 329, 337 | eqtr2d 2645 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((𝐹‘𝑘) · (1 / (#‘𝐴))) = (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) / (#‘𝐴))) |
339 | 4 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
340 | 339 | rpcnd 11750 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ) |
341 | | hashnncl 13018 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
342 | 2, 341 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
343 | 3, 342 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
344 | 343 | nnrecred 10943 |
. . . . . . . 8
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
345 | 344 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℂ) |
346 | 345 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (#‘𝐴)) ∈ ℂ) |
347 | 340, 346 | mulcld 9939 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) · (1 / (#‘𝐴))) ∈ ℂ) |
348 | 2, 347 | gsumfsum 19632 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) · (1 / (#‘𝐴))))) = Σ𝑘 ∈ 𝐴 ((𝐹‘𝑘) · (1 / (#‘𝐴)))) |
349 | 4 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
350 | 349 | rpcnd 11750 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ℂ) |
351 | 2, 350 | gsumfsum 19632 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) = Σ𝑘 ∈ 𝐴 (𝐹‘𝑘)) |
352 | 351 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) / (#‘𝐴)) = (Σ𝑘 ∈ 𝐴 (𝐹‘𝑘) / (#‘𝐴))) |
353 | 338, 348,
352 | 3eqtr4d 2654 |
. . 3
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) · (1 / (#‘𝐴))))) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) / (#‘𝐴))) |
354 | 4 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈
ℝ+) |
355 | | hashnncl 13018 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin →
((#‘𝐴) ∈ ℕ
↔ 𝐴 ≠
∅)) |
356 | 2, 355 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((#‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅)) |
357 | 3, 356 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝐴) ∈ ℕ) |
358 | 357 | nnrecred 10943 |
. . . . . . 7
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℝ) |
359 | 358 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → (1 / (#‘𝐴)) ∈
ℂ) |
360 | 359 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (1 / (#‘𝐴)) ∈ ℂ) |
361 | 4 | feqmptd 6159 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
362 | | fconstmpt 5085 |
. . . . . 6
⊢ (𝐴 × {(1 / (#‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴))) |
363 | 362 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝐴 × {(1 / (#‘𝐴))}) = (𝑘 ∈ 𝐴 ↦ (1 / (#‘𝐴)))) |
364 | 2, 354, 360, 361, 363 | offval2 6812 |
. . . 4
⊢ (𝜑 → (𝐹 ∘𝑓 · (𝐴 × {(1 / (#‘𝐴))})) = (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) · (1 / (#‘𝐴))))) |
365 | 364 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (ℂfld
Σg (𝐹 ∘𝑓 · (𝐴 × {(1 / (#‘𝐴))}))) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) · (1 / (#‘𝐴)))))) |
366 | 4 | feqmptd 6159 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
367 | 366 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (ℂfld
Σg 𝐹) = (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)))) |
368 | 367 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((ℂfld
Σg 𝐹) / (#‘𝐴)) = ((ℂfld
Σg (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) / (#‘𝐴))) |
369 | 353, 365,
368 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → (ℂfld
Σg (𝐹 ∘𝑓 · (𝐴 × {(1 / (#‘𝐴))}))) = ((ℂfld
Σg 𝐹) / (#‘𝐴))) |
370 | 42, 317, 369 | 3brtr3d 4614 |
1
⊢ (𝜑 → ((𝑀 Σg 𝐹)↑𝑐(1 /
(#‘𝐴))) ≤
((ℂfld Σg 𝐹) / (#‘𝐴))) |