Step | Hyp | Ref
| Expression |
1 | | 00id 8060 |
. . . . 5
⊢ (0 + 0) =
0 |
2 | | sum0 11351 |
. . . . . 6
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
3 | | sum0 11351 |
. . . . . 6
⊢
Σ𝑘 ∈
∅ 𝐶 =
0 |
4 | 2, 3 | oveq12i 5865 |
. . . . 5
⊢
(Σ𝑘 ∈
∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶) = (0 + 0) |
5 | | sum0 11351 |
. . . . 5
⊢
Σ𝑘 ∈
∅ (𝐵 + 𝐶) = 0 |
6 | 1, 4, 5 | 3eqtr4ri 2202 |
. . . 4
⊢
Σ𝑘 ∈
∅ (𝐵 + 𝐶) = (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶) |
7 | | sumeq1 11318 |
. . . 4
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = Σ𝑘 ∈ ∅ (𝐵 + 𝐶)) |
8 | | sumeq1 11318 |
. . . . 5
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
9 | | sumeq1 11318 |
. . . . 5
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ ∅ 𝐶) |
10 | 8, 9 | oveq12d 5871 |
. . . 4
⊢ (𝐴 = ∅ → (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶) = (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶)) |
11 | 6, 7, 10 | 3eqtr4a 2229 |
. . 3
⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)) |
12 | 11 | a1i 9 |
. 2
⊢ (𝜑 → (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))) |
13 | | simprl 526 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
ℕ) |
14 | | nnuz 9522 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
15 | 13, 14 | eleqtrdi 2263 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈
(ℤ≥‘1)) |
16 | | eqid 2170 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)) |
17 | | breq1 3992 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑛 ≤ (♯‘𝐴))) |
18 | | fveq2 5496 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛)) |
19 | 17, 18 | ifbieq1d 3548 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)) |
20 | | elnnuz 9523 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
21 | 20 | biimpri 132 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘1) → 𝑛 ∈ ℕ) |
22 | 21 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ 𝑛 ∈
ℕ) |
23 | | fsumadd.2 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
24 | 23 | adantlr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
25 | 24 | fmpttd 5651 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
26 | | simprr 527 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) |
27 | | f1of 5442 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
28 | 26, 27 | syl 14 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴) |
29 | | fco 5363 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
30 | 25, 28, 29 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
31 | 30 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
32 | | 1zzd 9239 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) → 1
∈ ℤ) |
33 | 13 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(♯‘𝐴) ∈
ℕ) |
34 | 33 | nnzd 9333 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(♯‘𝐴) ∈
ℤ) |
35 | | eluzelz 9496 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘1) → 𝑛 ∈ ℤ) |
36 | 35 | ad2antlr 486 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
𝑛 ∈
ℤ) |
37 | 32, 34, 36 | 3jca 1172 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑛 ∈ ℤ)) |
38 | | eluzle 9499 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(ℤ≥‘1) → 1 ≤ 𝑛) |
39 | 38 | ad2antlr 486 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) → 1
≤ 𝑛) |
40 | | simpr 109 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
𝑛 ≤ (♯‘𝐴)) |
41 | 39, 40 | jca 304 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(1 ≤ 𝑛 ∧ 𝑛 ≤ (♯‘𝐴))) |
42 | | elfz2 9972 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(♯‘𝐴))
↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ (♯‘𝐴)))) |
43 | 37, 41, 42 | sylanbrc 415 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
𝑛 ∈
(1...(♯‘𝐴))) |
44 | 31, 43 | ffvelrnd 5632 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) ∈ ℂ) |
45 | | 0cnd 7913 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ ¬ 𝑛 ≤
(♯‘𝐴)) → 0
∈ ℂ) |
46 | 22 | nnzd 9333 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ 𝑛 ∈
ℤ) |
47 | 13 | adantr 274 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ (♯‘𝐴)
∈ ℕ) |
48 | 47 | nnzd 9333 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ (♯‘𝐴)
∈ ℤ) |
49 | | zdcle 9288 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ) → DECID 𝑛 ≤ (♯‘𝐴)) |
50 | 46, 48, 49 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ DECID 𝑛 ≤ (♯‘𝐴)) |
51 | 44, 45, 50 | ifcldadc 3555 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) ∈ ℂ) |
52 | 16, 19, 22, 51 | fvmptd3 5589 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ ((𝑗 ∈ ℕ
↦ if(𝑗 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)) |
53 | 52, 51 | eqeltrd 2247 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ ((𝑗 ∈ ℕ
↦ if(𝑗 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) ∈ ℂ) |
54 | | eqid 2170 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)) |
55 | | fveq2 5496 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)) |
56 | 17, 55 | ifbieq1d 3548 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) |
57 | | fsumadd.3 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
58 | 57 | adantlr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ) |
59 | 58 | fmpttd 5651 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ) |
60 | 59 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ) |
61 | 28 | ad2antrr 485 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
𝑓:(1...(♯‘𝐴))⟶𝐴) |
62 | | fco 5363 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
63 | 60, 61, 62 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
64 | 63, 43 | ffvelrnd 5632 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) ∈ ℂ) |
65 | 64, 45, 50 | ifcldadc 3555 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) ∈ ℂ) |
66 | 54, 56, 22, 65 | fvmptd3 5589 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ ((𝑗 ∈ ℕ
↦ if(𝑗 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) |
67 | 66, 65 | eqeltrd 2247 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ ((𝑗 ∈ ℕ
↦ if(𝑗 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛) ∈ ℂ) |
68 | | simpll 524 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(𝜑 ∧
((♯‘𝐴) ∈
ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
69 | 28 | ffvelrnda 5631 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝑓‘𝑛) ∈ 𝐴) |
70 | | simpr 109 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴) |
71 | 23, 57 | addcld 7939 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℂ) |
72 | | eqid 2170 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) = (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) |
73 | 72 | fvmpt2 5579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ 𝐴 ∧ (𝐵 + 𝐶) ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶)) |
74 | 70, 71, 73 | syl2anc 409 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶)) |
75 | | eqid 2170 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
76 | 75 | fvmpt2 5579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = 𝐵) |
77 | 70, 23, 76 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = 𝐵) |
78 | | eqid 2170 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝐴 ↦ 𝐶) = (𝑘 ∈ 𝐴 ↦ 𝐶) |
79 | 78 | fvmpt2 5579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ 𝐴 ∧ 𝐶 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = 𝐶) |
80 | 70, 57, 79 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = 𝐶) |
81 | 77, 80 | oveq12d 5871 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) = (𝐵 + 𝐶)) |
82 | 74, 81 | eqtr4d 2206 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘))) |
83 | 82 | ralrimiva 2543 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘))) |
84 | 83 | ad2antrr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘))) |
85 | | nffvmpt1 5507 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) |
86 | | nffvmpt1 5507 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) |
87 | | nfcv 2312 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘
+ |
88 | | nffvmpt1 5507 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)) |
89 | 86, 87, 88 | nfov 5883 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
90 | 85, 89 | nfeq 2320 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
91 | | fveq2 5496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛))) |
92 | | fveq2 5496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
93 | | fveq2 5496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
94 | 92, 93 | oveq12d 5871 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑓‘𝑛) → (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))) |
95 | 91, 94 | eqeq12d 2185 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑓‘𝑛) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) ↔ ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))))) |
96 | 90, 95 | rspc 2828 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))))) |
97 | 69, 84, 96 | sylc 62 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))) |
98 | | fvco3 5567 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛))) |
99 | 28, 98 | sylan 281 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛))) |
100 | | fvco3 5567 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
101 | 28, 100 | sylan 281 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
102 | | fvco3 5567 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
103 | 28, 102 | sylan 281 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
104 | 101, 103 | oveq12d 5871 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))) |
105 | 97, 99, 104 | 3eqtr4d 2213 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛))) |
106 | 68, 43, 105 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛))) |
107 | 40 | iftrued 3533 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛)) |
108 | 40 | iftrued 3533 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛)) |
109 | 40 | iftrued 3533 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)) |
110 | 108, 109 | oveq12d 5871 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛))) |
111 | 106, 107,
110 | 3eqtr4d 2213 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))) |
112 | 1 | eqcomi 2174 |
. . . . . . . . . . 11
⊢ 0 = (0 +
0) |
113 | | simpr 109 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ ¬ 𝑛 ≤
(♯‘𝐴)) →
¬ 𝑛 ≤
(♯‘𝐴)) |
114 | 113 | iffalsed 3536 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ ¬ 𝑛 ≤
(♯‘𝐴)) →
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = 0) |
115 | 113 | iffalsed 3536 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ ¬ 𝑛 ≤
(♯‘𝐴)) →
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = 0) |
116 | 113 | iffalsed 3536 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ ¬ 𝑛 ≤
(♯‘𝐴)) →
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = 0) |
117 | 115, 116 | oveq12d 5871 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ ¬ 𝑛 ≤
(♯‘𝐴)) →
(if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = (0 + 0)) |
118 | 112, 114,
117 | 3eqtr4a 2229 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ ¬ 𝑛 ≤
(♯‘𝐴)) →
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))) |
119 | | exmiddc 831 |
. . . . . . . . . . 11
⊢
(DECID 𝑛 ≤ (♯‘𝐴) → (𝑛 ≤ (♯‘𝐴) ∨ ¬ 𝑛 ≤ (♯‘𝐴))) |
120 | 50, 119 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ (𝑛 ≤
(♯‘𝐴) ∨
¬ 𝑛 ≤
(♯‘𝐴))) |
121 | 111, 118,
120 | mpjaodan 793 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))) |
122 | | eqid 2170 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)) |
123 | | fveq2 5496 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛)) |
124 | 17, 123 | ifbieq1d 3548 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)) |
125 | 71 | fmpttd 5651 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ) |
126 | 125 | ad3antrrr 489 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ) |
127 | | fco 5363 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
128 | 126, 61, 127 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ) |
129 | 128, 43 | ffvelrnd 5632 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
∧ 𝑛 ≤
(♯‘𝐴)) →
(((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) ∈ ℂ) |
130 | 129, 45, 50 | ifcldadc 3555 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) ∈ ℂ) |
131 | 122, 124,
22, 130 | fvmptd3 5589 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ ((𝑗 ∈ ℕ
↦ if(𝑗 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)) |
132 | 52, 66 | oveq12d 5871 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ (((𝑗 ∈ ℕ
↦ if(𝑗 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) + ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛)) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))) |
133 | 121, 131,
132 | 3eqtr4d 2213 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ≥‘1))
→ ((𝑗 ∈ ℕ
↦ if(𝑗 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))‘𝑛) = (((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) + ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛))) |
134 | 15, 53, 67, 133 | ser3add 10461 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) = ((seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) + (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)))) |
135 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛))) |
136 | 24, 58 | addcld 7939 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℂ) |
137 | 136 | fmpttd 5651 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ) |
138 | 137 | ffvelrnda 5631 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) ∈ ℂ) |
139 | 135, 13, 26, 138, 99 | fsum3 11350 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴))) |
140 | | breq1 3992 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴))) |
141 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗)) |
142 | 140, 141 | ifbieq1d 3548 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)) |
143 | 142 | cbvmptv 4085 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)) |
144 | | seqeq3 10406 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0))) = seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))) |
145 | 143, 144 | ax-mp 5 |
. . . . . . . . 9
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0))) = seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))) |
146 | 145 | fveq1i 5497 |
. . . . . . . 8
⊢ (seq1( +
, (𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) |
147 | 139, 146 | eqtrdi 2219 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))) |
148 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))) |
149 | 25 | ffvelrnda 5631 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
150 | 148, 13, 26, 149, 101 | fsum3 11350 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴))) |
151 | | fveq2 5496 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗)) |
152 | 140, 151 | ifbieq1d 3548 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)) |
153 | 152 | cbvmptv 4085 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)) |
154 | | seqeq3 10406 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0))) = seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))) |
155 | 153, 154 | ax-mp 5 |
. . . . . . . . . 10
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0))) = seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))) |
156 | 155 | fveq1i 5497 |
. . . . . . . . 9
⊢ (seq1( +
, (𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) |
157 | 150, 156 | eqtrdi 2219 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))) |
158 | | fveq2 5496 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))) |
159 | 59 | ffvelrnda 5631 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) ∈ ℂ) |
160 | 158, 13, 26, 159, 103 | fsum3 11350 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴))) |
161 | | fveq2 5496 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗)) |
162 | 140, 161 | ifbieq1d 3548 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)) |
163 | 162 | cbvmptv 4085 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)) |
164 | | seqeq3 10406 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)) → seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))) = seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))) |
165 | 163, 164 | ax-mp 5 |
. . . . . . . . . 10
⊢ seq1( + ,
(𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))) = seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))) |
166 | 165 | fveq1i 5497 |
. . . . . . . . 9
⊢ (seq1( +
, (𝑛 ∈ ℕ ↦
if(𝑛 ≤
(♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) |
167 | 160, 166 | eqtrdi 2219 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))) |
168 | 157, 167 | oveq12d 5871 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = ((seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) + (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)))) |
169 | 134, 147,
168 | 3eqtr4d 2213 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚))) |
170 | 71 | ralrimiva 2543 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 (𝐵 + 𝐶) ∈ ℂ) |
171 | | sumfct 11337 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 (𝐵 + 𝐶) ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶)) |
172 | 170, 171 | syl 14 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶)) |
173 | 172 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶)) |
174 | 23 | ralrimiva 2543 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
175 | | sumfct 11337 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵) |
176 | 174, 175 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵) |
177 | 57 | ralrimiva 2543 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ) |
178 | | sumfct 11337 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
𝐴 𝐶 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶) |
179 | 177, 178 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶) |
180 | 176, 179 | oveq12d 5871 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)) |
181 | 180 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)) |
182 | 169, 173,
181 | 3eqtr3d 2211 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)) |
183 | 182 | expr 373 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))) |
184 | 183 | exlimdv 1812 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))) |
185 | 184 | expimpd 361 |
. 2
⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))) |
186 | | fsumadd.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
187 | | fz1f1o 11338 |
. . 3
⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨
((♯‘𝐴) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
188 | 186, 187 | syl 14 |
. 2
⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴))) |
189 | 12, 185, 188 | mpjaod 713 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)) |