| Step | Hyp | Ref
| Expression |
| 1 | | mpteq1 5235 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ ∅ ↦ 𝐵)) |
| 2 | | mpt0 6710 |
. . . . . . 7
⊢ (𝑘 ∈ ∅ ↦ 𝐵) = ∅ |
| 3 | 1, 2 | eqtrdi 2793 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝑘 ∈ 𝐴 ↦ 𝐵) = ∅) |
| 4 | 3 | oveq2d 7447 |
. . . . 5
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = (ℂfld
Σg ∅)) |
| 5 | | cnfld0 21405 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
| 6 | 5 | gsum0 18697 |
. . . . . 6
⊢
(ℂfld Σg ∅) =
0 |
| 7 | | sum0 15757 |
. . . . . 6
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
| 8 | 6, 7 | eqtr4i 2768 |
. . . . 5
⊢
(ℂfld Σg ∅) =
Σ𝑘 ∈ ∅
𝐵 |
| 9 | 4, 8 | eqtrdi 2793 |
. . . 4
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ ∅ 𝐵) |
| 10 | | sumeq1 15725 |
. . . 4
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
| 11 | 9, 10 | eqtr4d 2780 |
. . 3
⊢ (𝐴 = ∅ →
(ℂfld Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |
| 12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → (𝐴 = ∅ → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
| 13 | | cnfldbas 21368 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
| 14 | | cnfldadd 21370 |
. . . . . . 7
⊢ + =
(+g‘ℂfld) |
| 15 | | eqid 2737 |
. . . . . . 7
⊢
(Cntz‘ℂfld) =
(Cntz‘ℂfld) |
| 16 | | cnring 21403 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
| 17 | | ringmnd 20240 |
. . . . . . . 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 | 21 | fmpttd 7135 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
| 23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
| 24 | | ringcmn 20279 |
. . . . . . . . 9
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
| 25 | 16, 24 | mp1i 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ℂfld
∈ CMnd) |
| 26 | 13, 15, 25, 23 | cntzcmnf 19863 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ran (𝑘 ∈ 𝐴 ↦ 𝐵) ⊆
((Cntz‘ℂfld)‘ran (𝑘 ∈ 𝐴 ↦ 𝐵))) |
| 27 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
ℕ) |
| 28 | | simprr 773 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 29 | | f1of1 6847 |
. . . . . . . 8
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))–1-1→𝐴) |
| 30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1→𝐴) |
| 31 | | suppssdm 8202 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ dom (𝑘 ∈ 𝐴 ↦ 𝐵) |
| 32 | 31, 23 | fssdm 6755 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ 𝐴) |
| 33 | | f1ofo 6855 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))–onto→𝐴) |
| 34 | | forn 6823 |
. . . . . . . . 9
⊢ (𝑓:(1...(♯‘𝐴))–onto→𝐴 → ran 𝑓 = 𝐴) |
| 35 | 28, 33, 34 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ran 𝑓 = 𝐴) |
| 36 | 32, 35 | sseqtrrd 4021 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 0) ⊆ ran 𝑓) |
| 37 | | eqid 2737 |
. . . . . . 7
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓) supp 0) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓) supp 0) |
| 38 | 13, 5, 14, 15, 18, 20, 23, 26, 27, 30, 36, 37 | gsumval3 19925 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) |
| 39 | | sumfc 15745 |
. . . . . . 7
⊢
Σ𝑥 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = Σ𝑘 ∈ 𝐴 𝐵 |
| 40 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑥 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
| 41 | 23 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑥 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ ℂ) |
| 42 | | f1of 6848 |
. . . . . . . . . 10
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
| 43 | 28, 42 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
| 44 | | fvco3 7008 |
. . . . . . . . 9
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
| 45 | 43, 44 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
| 46 | 40, 27, 28, 41, 45 | fsum 15756 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑥 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑥) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) |
| 47 | 39, 46 | eqtr3id 2791 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑘 ∈ 𝐴 𝐵 = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓))‘(♯‘𝐴))) |
| 48 | 38, 47 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |
| 49 | 48 | expr 456 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
| 50 | 49 | exlimdv 1933 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
| 51 | 50 | expimpd 453 |
. 2
⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵)) |
| 52 | | fz1f1o 15746 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
| 53 | 19, 52 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
| 54 | 12, 51, 53 | mpjaod 861 |
1
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) |