Step | Hyp | Ref
| Expression |
1 | | sum0 14452 |
. . . 4
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
2 | | fsumf1o.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
3 | | f1oeq2 6128 |
. . . . . . . 8
⊢ (𝐶 = ∅ → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:∅–1-1-onto→𝐴)) |
4 | 2, 3 | syl5ibcom 235 |
. . . . . . 7
⊢ (𝜑 → (𝐶 = ∅ → 𝐹:∅–1-1-onto→𝐴)) |
5 | 4 | imp 445 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐹:∅–1-1-onto→𝐴) |
6 | | f1ofo 6144 |
. . . . . 6
⊢ (𝐹:∅–1-1-onto→𝐴 → 𝐹:∅–onto→𝐴) |
7 | | fo00 6172 |
. . . . . . 7
⊢ (𝐹:∅–onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅)) |
8 | 7 | simprbi 480 |
. . . . . 6
⊢ (𝐹:∅–onto→𝐴 → 𝐴 = ∅) |
9 | 5, 6, 8 | 3syl 18 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐴 = ∅) |
10 | 9 | sumeq1d 14431 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
11 | | simpr 477 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐶 = ∅) |
12 | 11 | sumeq1d 14431 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑛 ∈ 𝐶 𝐷 = Σ𝑛 ∈ ∅ 𝐷) |
13 | | sum0 14452 |
. . . . 5
⊢
Σ𝑛 ∈
∅ 𝐷 =
0 |
14 | 12, 13 | syl6eq 2672 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑛 ∈ 𝐶 𝐷 = 0) |
15 | 1, 10, 14 | 3eqtr4a 2682 |
. . 3
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |
16 | 15 | ex 450 |
. 2
⊢ (𝜑 → (𝐶 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
17 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑚 = (𝑓‘𝑛) → (𝐹‘𝑚) = (𝐹‘(𝑓‘𝑛))) |
18 | 17 | fveq2d 6195 |
. . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
19 | | simprl 794 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → (#‘𝐶) ∈
ℕ) |
20 | | simprr 796 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) |
21 | | f1of 6137 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴) |
22 | 2, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
23 | 22 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → (𝐹‘𝑚) ∈ 𝐴) |
24 | | fsumf1o.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
25 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
26 | 24, 25 | fmptd 6385 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
27 | 26 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹‘𝑚) ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
28 | 23, 27 | syldan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
29 | 28 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
30 | 2 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → 𝐹:𝐶–1-1-onto→𝐴) |
31 | | f1oco 6159 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐶–1-1-onto→𝐴 ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) → (𝐹 ∘ 𝑓):(1...(#‘𝐶))–1-1-onto→𝐴) |
32 | 30, 20, 31 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → (𝐹 ∘ 𝑓):(1...(#‘𝐶))–1-1-onto→𝐴) |
33 | | f1of 6137 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝑓):(1...(#‘𝐶))–1-1-onto→𝐴 → (𝐹 ∘ 𝑓):(1...(#‘𝐶))⟶𝐴) |
34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → (𝐹 ∘ 𝑓):(1...(#‘𝐶))⟶𝐴) |
35 | | fvco3 6275 |
. . . . . . . . . 10
⊢ (((𝐹 ∘ 𝑓):(1...(#‘𝐶))⟶𝐴 ∧ 𝑛 ∈ (1...(#‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
36 | 34, 35 | sylan 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
37 | | f1of 6137 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(#‘𝐶))–1-1-onto→𝐶 → 𝑓:(1...(#‘𝐶))⟶𝐶) |
38 | 37 | ad2antll 765 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → 𝑓:(1...(#‘𝐶))⟶𝐶) |
39 | | fvco3 6275 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(#‘𝐶))⟶𝐶 ∧ 𝑛 ∈ (1...(#‘𝐶))) → ((𝐹 ∘ 𝑓)‘𝑛) = (𝐹‘(𝑓‘𝑛))) |
40 | 38, 39 | sylan 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → ((𝐹 ∘ 𝑓)‘𝑛) = (𝐹‘(𝑓‘𝑛))) |
41 | 40 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
42 | 36, 41 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(#‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
43 | 18, 19, 20, 29, 42 | fsum 14451 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐶 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓)))‘(#‘𝐶))) |
44 | | fsumf1o.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
45 | 22 | ffvelrnda 6359 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
46 | 44, 45 | eqeltrrd 2702 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴) |
47 | | fsumf1o.1 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
48 | 47, 25 | fvmpti 6281 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺) = ( I ‘𝐷)) |
49 | 46, 48 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺) = ( I ‘𝐷)) |
50 | 44 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺)) |
51 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷) |
52 | 51 | fvmpt2i 6290 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ 𝐶 → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ( I ‘𝐷)) |
53 | 52 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ( I ‘𝐷)) |
54 | 49, 50, 53 | 3eqtr4rd 2667 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛))) |
55 | 54 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛))) |
56 | | nffvmpt1 6199 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) |
57 | 56 | nfeq1 2778 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) |
58 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚)) |
59 | | fveq2 6191 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
60 | 59 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
61 | 58, 60 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) ↔ ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)))) |
62 | 57, 61 | rspc 3303 |
. . . . . . . . . 10
⊢ (𝑚 ∈ 𝐶 → (∀𝑛 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)))) |
63 | 55, 62 | mpan9 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
64 | 63 | adantlr 751 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
65 | 64 | sumeq2dv 14433 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑚 ∈ 𝐶 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
66 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = ((𝐹 ∘ 𝑓)‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
67 | 26 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
68 | 67 | ffvelrnda 6359 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
69 | 66, 19, 32, 68, 36 | fsum 14451 |
. . . . . . 7
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓)))‘(#‘𝐶))) |
70 | 43, 65, 69 | 3eqtr4rd 2667 |
. . . . . 6
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚)) |
71 | | sumfc 14440 |
. . . . . 6
⊢
Σ𝑚 ∈
𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵 |
72 | | sumfc 14440 |
. . . . . 6
⊢
Σ𝑚 ∈
𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑛 ∈ 𝐶 𝐷 |
73 | 70, 71, 72 | 3eqtr3g 2679 |
. . . . 5
⊢ ((𝜑 ∧ ((#‘𝐶) ∈ ℕ ∧ 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶)) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |
74 | 73 | expr 643 |
. . . 4
⊢ ((𝜑 ∧ (#‘𝐶) ∈ ℕ) → (𝑓:(1...(#‘𝐶))–1-1-onto→𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
75 | 74 | exlimdv 1861 |
. . 3
⊢ ((𝜑 ∧ (#‘𝐶) ∈ ℕ) → (∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
76 | 75 | expimpd 629 |
. 2
⊢ (𝜑 → (((#‘𝐶) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
77 | | fsumf1o.2 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Fin) |
78 | | fz1f1o 14441 |
. . 3
⊢ (𝐶 ∈ Fin → (𝐶 = ∅ ∨ ((#‘𝐶) ∈ ℕ ∧
∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶))) |
79 | 77, 78 | syl 17 |
. 2
⊢ (𝜑 → (𝐶 = ∅ ∨ ((#‘𝐶) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘𝐶))–1-1-onto→𝐶))) |
80 | 16, 76, 79 | mpjaod 396 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |