Step | Hyp | Ref
| Expression |
1 | | mpteq1 4665 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ ∅ ↦ 𝐵)) |
2 | | mpt0 5934 |
. . . . . . 7
⊢ (𝑘 ∈ ∅ ↦ 𝐵) = ∅ |
3 | 1, 2 | syl6eq 2660 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝑘 ∈ 𝐴 ↦ 𝐵) = ∅) |
4 | 3 | oveq2d 6565 |
. . . . 5
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = (ℂfld
Σg ∅)) |
5 | | cnfld0 19589 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
6 | 5 | gsum0 17101 |
. . . . . 6
⊢
(ℂfld Σg ∅) =
0 |
7 | | sum0 14299 |
. . . . . 6
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
8 | 6, 7 | eqtr4i 2635 |
. . . . 5
⊢
(ℂfld Σg ∅) =
Σ𝑘 ∈ ∅
𝐵 |
9 | 4, 8 | syl6eq 2660 |
. . . 4
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ ∅ 𝐵) |
10 | | sumeq1 14267 |
. . . 4
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
11 | 9, 10 | eqtr4d 2647 |
. . 3
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |
12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴 = ∅ → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
13 | | cnfldbas 19571 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
14 | | cnfldadd 19572 |
. . . . . . 7
⊢ + =
(+g‘ℂfld) |
15 | | eqid 2610 |
. . . . . . 7
⊢
(Cntz‘ℂfld) =
(Cntz‘ℂfld) |
16 | | cnring 19587 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
17 | | ringmnd 18379 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
18 | 16, 17 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ℂfld
∈ Mnd) |
19 | | gsumfsum.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ Fin) |
20 | 19 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝐴 ∈ Fin) |
21 | | gsumfsum.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
22 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
23 | 21, 22 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
25 | | ringcmn 18404 |
. . . . . . . . 9
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
26 | 16, 25 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ℂfld
∈ CMnd) |
27 | 13, 15, 26, 24 | cntzcmnf 18071 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆
((Cntz‘ℂfld)‘ran (𝑘 ∈ 𝐴 ↦ 𝐵))) |
28 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (#‘𝐴) ∈
ℕ) |
29 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) |
30 | | f1of1 6049 |
. . . . . . . 8
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(#‘𝐴))–1-1→𝐴) |
31 | 29, 30 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))–1-1→𝐴) |
32 | | suppssdm 7195 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ dom (𝑘 ∈ 𝐴 ↦ 𝐵) |
33 | | fdm 5964 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ → dom (𝑘 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
34 | 24, 33 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → dom (𝑘 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
35 | 32, 34 | syl5sseq 3616 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ 𝐴) |
36 | | f1ofo 6057 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(#‘𝐴))–onto→𝐴) |
37 | | forn 6031 |
. . . . . . . . 9
⊢ (𝑓:(1...(#‘𝐴))–onto→𝐴 → ran 𝑓 = 𝐴) |
38 | 29, 36, 37 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ran 𝑓 = 𝐴) |
39 | 35, 38 | sseqtr4d 3605 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ ran 𝑓) |
40 | | eqid 2610 |
. . . . . . 7
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓) supp 0) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓) supp 0) |
41 | 13, 5, 14, 15, 18, 20, 24, 27, 28, 31, 39, 40 | gsumval3 18131 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴))) |
42 | | sumfc 14287 |
. . . . . . 7
⊢
Σ𝑥 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = Σ𝑘 ∈ 𝐴 𝐵 |
43 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑥 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
44 | 24 | ffvelrnda 6267 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ ℂ) |
45 | | f1of 6050 |
. . . . . . . . . 10
⊢ (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(#‘𝐴))⟶𝐴) |
46 | 29, 45 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(#‘𝐴))⟶𝐴) |
47 | | fvco3 6185 |
. . . . . . . . 9
⊢ ((𝑓:(1...(#‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
48 | 46, 47 | sylan 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(#‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
49 | 43, 28, 29, 44, 48 | fsum 14298 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → Σ𝑥 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴))) |
50 | 42, 49 | syl5eqr 2658 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(#‘𝐴))) |
51 | 41, 50 | eqtr4d 2647 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝐴) ∈ ℕ ∧ 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴)) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |
52 | 51 | expr 641 |
. . . 4
⊢ ((𝜑 ∧ (#‘𝐴) ∈ ℕ) → (𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
53 | 52 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (#‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
54 | 53 | expimpd 627 |
. 2
⊢ (𝜑 → (((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
55 | | fz1f1o 14288 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
56 | 19, 55 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((#‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐴))–1-1-onto→𝐴))) |
57 | 12, 54, 56 | mpjaod 395 |
1
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |