Step | Hyp | Ref
| Expression |
1 | | mpteq1 5154 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ ∅ ↦ 𝐵)) |
2 | | mpt0 6490 |
. . . . . . 7
⊢ (𝑘 ∈ ∅ ↦ 𝐵) = ∅ |
3 | 1, 2 | syl6eq 2872 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝑘 ∈ 𝐴 ↦ 𝐵) = ∅) |
4 | 3 | oveq2d 7172 |
. . . . 5
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = (ℂfld
Σg ∅)) |
5 | | cnfld0 20569 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
6 | 5 | gsum0 17894 |
. . . . . 6
⊢
(ℂfld Σg ∅) =
0 |
7 | | sum0 15078 |
. . . . . 6
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
8 | 6, 7 | eqtr4i 2847 |
. . . . 5
⊢
(ℂfld Σg ∅) =
Σ𝑘 ∈ ∅
𝐵 |
9 | 4, 8 | syl6eq 2872 |
. . . 4
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ ∅ 𝐵) |
10 | | sumeq1 15045 |
. . . 4
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
11 | 9, 10 | eqtr4d 2859 |
. . 3
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |
12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴 = ∅ → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
13 | | cnfldbas 20549 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
14 | | cnfldadd 20550 |
. . . . . . 7
⊢ + =
(+g‘ℂfld) |
15 | | eqid 2821 |
. . . . . . 7
⊢
(Cntz‘ℂfld) =
(Cntz‘ℂfld) |
16 | | cnring 20567 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
17 | | ringmnd 19306 |
. . . . . . . 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 483 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝐴 ∈ Fin) |
21 | | gsumfsum.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
22 | 21 | fmpttd 6879 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
23 | 22 | adantr 483 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
24 | | ringcmn 19331 |
. . . . . . . . 9
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
25 | 16, 24 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ℂfld
∈ CMnd) |
26 | 13, 15, 25, 23 | cntzcmnf 18965 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆
((Cntz‘ℂfld)‘ran (𝑘 ∈ 𝐴 ↦ 𝐵))) |
27 | | simprl 769 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
ℕ) |
28 | | simprr 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) |
29 | | f1of1 6614 |
. . . . . . . 8
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))–1-1→𝐴) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1→𝐴) |
31 | | suppssdm 7843 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ dom (𝑘 ∈ 𝐴 ↦ 𝐵) |
32 | 31, 23 | fssdm 6530 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ 𝐴) |
33 | | f1ofo 6622 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))–onto→𝐴) |
34 | | forn 6593 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘𝐴))–onto→𝐴 → ran 𝑓 = 𝐴) |
35 | 28, 33, 34 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ran 𝑓 = 𝐴) |
36 | 32, 35 | sseqtrrd 4008 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ ran 𝑓) |
37 | | eqid 2821 |
. . . . . . 7
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓) supp 0) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓) supp 0) |
38 | 13, 5, 14, 15, 18, 20, 23, 26, 27, 30, 36, 37 | gsumval3 19027 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) |
39 | | sumfc 15066 |
. . . . . . 7
⊢
Σ𝑥 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = Σ𝑘 ∈ 𝐴 𝐵 |
40 | | fveq2 6670 |
. . . . . . . 8
⊢ (𝑥 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
41 | 23 | ffvelrnda 6851 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ ℂ) |
42 | | f1of 6615 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
43 | 28, 42 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
44 | | fvco3 6760 |
. . . . . . . . 9
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
45 | 43, 44 | sylan 582 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
46 | 40, 27, 28, 41, 45 | fsum 15077 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑥 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) |
47 | 39, 46 | syl5eqr 2870 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) |
48 | 38, 47 | eqtr4d 2859 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |
49 | 48 | expr 459 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
50 | 49 | exlimdv 1934 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
51 | 50 | expimpd 456 |
. 2
⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
52 | | fz1f1o 15067 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
53 | 19, 52 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
54 | 12, 51, 53 | mpjaod 856 |
1
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |