MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsumadd Structured version   Visualization version   GIF version

Theorem fsumadd 14679
Description: The sum of two finite sums. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 22-Apr-2014.)
Hypotheses
Ref Expression
fsumadd.1 (𝜑𝐴 ∈ Fin)
fsumadd.2 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
fsumadd.3 ((𝜑𝑘𝐴) → 𝐶 ∈ ℂ)
Assertion
Ref Expression
fsumadd (𝜑 → Σ𝑘𝐴 (𝐵 + 𝐶) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶))
Distinct variable groups:   𝐴,𝑘   𝜑,𝑘
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)

Proof of Theorem fsumadd
Dummy variables 𝑓 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 00id 10414 . . . . 5 (0 + 0) = 0
2 sum0 14661 . . . . . 6 Σ𝑘 ∈ ∅ 𝐵 = 0
3 sum0 14661 . . . . . 6 Σ𝑘 ∈ ∅ 𝐶 = 0
42, 3oveq12i 6806 . . . . 5 𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶) = (0 + 0)
5 sum0 14661 . . . . 5 Σ𝑘 ∈ ∅ (𝐵 + 𝐶) = 0
61, 4, 53eqtr4ri 2804 . . . 4 Σ𝑘 ∈ ∅ (𝐵 + 𝐶) = (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶)
7 sumeq1 14628 . . . 4 (𝐴 = ∅ → Σ𝑘𝐴 (𝐵 + 𝐶) = Σ𝑘 ∈ ∅ (𝐵 + 𝐶))
8 sumeq1 14628 . . . . 5 (𝐴 = ∅ → Σ𝑘𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵)
9 sumeq1 14628 . . . . 5 (𝐴 = ∅ → Σ𝑘𝐴 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
108, 9oveq12d 6812 . . . 4 (𝐴 = ∅ → (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶) = (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶))
116, 7, 103eqtr4a 2831 . . 3 (𝐴 = ∅ → Σ𝑘𝐴 (𝐵 + 𝐶) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶))
1211a1i 11 . 2 (𝜑 → (𝐴 = ∅ → Σ𝑘𝐴 (𝐵 + 𝐶) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶)))
13 simprl 748 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (♯‘𝐴) ∈ ℕ)
14 nnuz 11926 . . . . . . . . 9 ℕ = (ℤ‘1)
1513, 14syl6eleq 2860 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (♯‘𝐴) ∈ (ℤ‘1))
16 fsumadd.2 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
1716adantlr 688 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑘𝐴) → 𝐵 ∈ ℂ)
18 eqid 2771 . . . . . . . . . . 11 (𝑘𝐴𝐵) = (𝑘𝐴𝐵)
1917, 18fmptd 6528 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (𝑘𝐴𝐵):𝐴⟶ℂ)
20 simprr 750 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)
21 f1of 6279 . . . . . . . . . . 11 (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴𝑓:(1...(♯‘𝐴))⟶𝐴)
2220, 21syl 17 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
23 fco 6199 . . . . . . . . . 10 (((𝑘𝐴𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘𝐴𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
2419, 22, 23syl2anc 567 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → ((𝑘𝐴𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
2524ffvelrnda 6503 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛) ∈ ℂ)
26 fsumadd.3 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → 𝐶 ∈ ℂ)
2726adantlr 688 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑘𝐴) → 𝐶 ∈ ℂ)
28 eqid 2771 . . . . . . . . . . 11 (𝑘𝐴𝐶) = (𝑘𝐴𝐶)
2927, 28fmptd 6528 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (𝑘𝐴𝐶):𝐴⟶ℂ)
30 fco 6199 . . . . . . . . . 10 (((𝑘𝐴𝐶):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘𝐴𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
3129, 22, 30syl2anc 567 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → ((𝑘𝐴𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
3231ffvelrnda 6503 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐶) ∘ 𝑓)‘𝑛) ∈ ℂ)
3322ffvelrnda 6503 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝑓𝑛) ∈ 𝐴)
34 ovex 6824 . . . . . . . . . . . . . . 15 (𝐵 + 𝐶) ∈ V
35 eqid 2771 . . . . . . . . . . . . . . . 16 (𝑘𝐴 ↦ (𝐵 + 𝐶)) = (𝑘𝐴 ↦ (𝐵 + 𝐶))
3635fvmpt2 6434 . . . . . . . . . . . . . . 15 ((𝑘𝐴 ∧ (𝐵 + 𝐶) ∈ V) → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶))
3734, 36mpan2 665 . . . . . . . . . . . . . 14 (𝑘𝐴 → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶))
3837adantl 467 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶))
39 simpr 471 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → 𝑘𝐴)
4018fvmpt2 6434 . . . . . . . . . . . . . . 15 ((𝑘𝐴𝐵 ∈ ℂ) → ((𝑘𝐴𝐵)‘𝑘) = 𝐵)
4139, 16, 40syl2anc 567 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ((𝑘𝐴𝐵)‘𝑘) = 𝐵)
4228fvmpt2 6434 . . . . . . . . . . . . . . 15 ((𝑘𝐴𝐶 ∈ ℂ) → ((𝑘𝐴𝐶)‘𝑘) = 𝐶)
4339, 26, 42syl2anc 567 . . . . . . . . . . . . . 14 ((𝜑𝑘𝐴) → ((𝑘𝐴𝐶)‘𝑘) = 𝐶)
4441, 43oveq12d 6812 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (((𝑘𝐴𝐵)‘𝑘) + ((𝑘𝐴𝐶)‘𝑘)) = (𝐵 + 𝐶))
4538, 44eqtr4d 2808 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘𝐴𝐵)‘𝑘) + ((𝑘𝐴𝐶)‘𝑘)))
4645ralrimiva 3115 . . . . . . . . . . 11 (𝜑 → ∀𝑘𝐴 ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘𝐴𝐵)‘𝑘) + ((𝑘𝐴𝐶)‘𝑘)))
4746ad2antrr 699 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ∀𝑘𝐴 ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘𝐴𝐵)‘𝑘) + ((𝑘𝐴𝐶)‘𝑘)))
48 nffvmpt1 6341 . . . . . . . . . . . 12 𝑘((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛))
49 nffvmpt1 6341 . . . . . . . . . . . . 13 𝑘((𝑘𝐴𝐵)‘(𝑓𝑛))
50 nfcv 2913 . . . . . . . . . . . . 13 𝑘 +
51 nffvmpt1 6341 . . . . . . . . . . . . 13 𝑘((𝑘𝐴𝐶)‘(𝑓𝑛))
5249, 50, 51nfov 6822 . . . . . . . . . . . 12 𝑘(((𝑘𝐴𝐵)‘(𝑓𝑛)) + ((𝑘𝐴𝐶)‘(𝑓𝑛)))
5348, 52nfeq 2925 . . . . . . . . . . 11 𝑘((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛)) = (((𝑘𝐴𝐵)‘(𝑓𝑛)) + ((𝑘𝐴𝐶)‘(𝑓𝑛)))
54 fveq2 6333 . . . . . . . . . . . 12 (𝑘 = (𝑓𝑛) → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛)))
55 fveq2 6333 . . . . . . . . . . . . 13 (𝑘 = (𝑓𝑛) → ((𝑘𝐴𝐵)‘𝑘) = ((𝑘𝐴𝐵)‘(𝑓𝑛)))
56 fveq2 6333 . . . . . . . . . . . . 13 (𝑘 = (𝑓𝑛) → ((𝑘𝐴𝐶)‘𝑘) = ((𝑘𝐴𝐶)‘(𝑓𝑛)))
5755, 56oveq12d 6812 . . . . . . . . . . . 12 (𝑘 = (𝑓𝑛) → (((𝑘𝐴𝐵)‘𝑘) + ((𝑘𝐴𝐶)‘𝑘)) = (((𝑘𝐴𝐵)‘(𝑓𝑛)) + ((𝑘𝐴𝐶)‘(𝑓𝑛))))
5854, 57eqeq12d 2786 . . . . . . . . . . 11 (𝑘 = (𝑓𝑛) → (((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘𝐴𝐵)‘𝑘) + ((𝑘𝐴𝐶)‘𝑘)) ↔ ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛)) = (((𝑘𝐴𝐵)‘(𝑓𝑛)) + ((𝑘𝐴𝐶)‘(𝑓𝑛)))))
5953, 58rspc 3455 . . . . . . . . . 10 ((𝑓𝑛) ∈ 𝐴 → (∀𝑘𝐴 ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘𝐴𝐵)‘𝑘) + ((𝑘𝐴𝐶)‘𝑘)) → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛)) = (((𝑘𝐴𝐵)‘(𝑓𝑛)) + ((𝑘𝐴𝐶)‘(𝑓𝑛)))))
6033, 47, 59sylc 65 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛)) = (((𝑘𝐴𝐵)‘(𝑓𝑛)) + ((𝑘𝐴𝐶)‘(𝑓𝑛))))
61 fvco3 6418 . . . . . . . . . 10 ((𝑓:(1...(♯‘𝐴))⟶𝐴𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛)))
6222, 61sylan 563 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛)))
63 fvco3 6418 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝐴))⟶𝐴𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛) = ((𝑘𝐴𝐵)‘(𝑓𝑛)))
6422, 63sylan 563 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛) = ((𝑘𝐴𝐵)‘(𝑓𝑛)))
65 fvco3 6418 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝐴))⟶𝐴𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐶) ∘ 𝑓)‘𝑛) = ((𝑘𝐴𝐶)‘(𝑓𝑛)))
6622, 65sylan 563 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴𝐶) ∘ 𝑓)‘𝑛) = ((𝑘𝐴𝐶)‘(𝑓𝑛)))
6764, 66oveq12d 6812 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛) + (((𝑘𝐴𝐶) ∘ 𝑓)‘𝑛)) = (((𝑘𝐴𝐵)‘(𝑓𝑛)) + ((𝑘𝐴𝐶)‘(𝑓𝑛))))
6860, 62, 673eqtr4d 2815 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((((𝑘𝐴𝐵) ∘ 𝑓)‘𝑛) + (((𝑘𝐴𝐶) ∘ 𝑓)‘𝑛)))
6915, 25, 32, 68seradd 13051 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (seq1( + , ((𝑘𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓))‘(♯‘𝐴)) = ((seq1( + , ((𝑘𝐴𝐵) ∘ 𝑓))‘(♯‘𝐴)) + (seq1( + , ((𝑘𝐴𝐶) ∘ 𝑓))‘(♯‘𝐴))))
70 fveq2 6333 . . . . . . . 8 (𝑚 = (𝑓𝑛) → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘(𝑓𝑛)))
7117, 27addcld 10262 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑘𝐴) → (𝐵 + 𝐶) ∈ ℂ)
7271, 35fmptd 6528 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (𝑘𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ)
7372ffvelrnda 6503 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑚𝐴) → ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑚) ∈ ℂ)
7470, 13, 20, 73, 62fsum 14660 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → Σ𝑚𝐴 ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (seq1( + , ((𝑘𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓))‘(♯‘𝐴)))
75 fveq2 6333 . . . . . . . . 9 (𝑚 = (𝑓𝑛) → ((𝑘𝐴𝐵)‘𝑚) = ((𝑘𝐴𝐵)‘(𝑓𝑛)))
7619ffvelrnda 6503 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑚𝐴) → ((𝑘𝐴𝐵)‘𝑚) ∈ ℂ)
7775, 13, 20, 76, 64fsum 14660 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = (seq1( + , ((𝑘𝐴𝐵) ∘ 𝑓))‘(♯‘𝐴)))
78 fveq2 6333 . . . . . . . . 9 (𝑚 = (𝑓𝑛) → ((𝑘𝐴𝐶)‘𝑚) = ((𝑘𝐴𝐶)‘(𝑓𝑛)))
7929ffvelrnda 6503 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) ∧ 𝑚𝐴) → ((𝑘𝐴𝐶)‘𝑚) ∈ ℂ)
8078, 13, 20, 79, 66fsum 14660 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = (seq1( + , ((𝑘𝐴𝐶) ∘ 𝑓))‘(♯‘𝐴)))
8177, 80oveq12d 6812 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → (Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) + Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚)) = ((seq1( + , ((𝑘𝐴𝐵) ∘ 𝑓))‘(♯‘𝐴)) + (seq1( + , ((𝑘𝐴𝐶) ∘ 𝑓))‘(♯‘𝐴))))
8269, 74, 813eqtr4d 2815 . . . . . 6 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → Σ𝑚𝐴 ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) + Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚)))
83 sumfc 14649 . . . . . 6 Σ𝑚𝐴 ((𝑘𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘𝐴 (𝐵 + 𝐶)
84 sumfc 14649 . . . . . . 7 Σ𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = Σ𝑘𝐴 𝐵
85 sumfc 14649 . . . . . . 7 Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑘𝐴 𝐶
8684, 85oveq12i 6806 . . . . . 6 𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) + Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚)) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶)
8782, 83, 863eqtr3g 2828 . . . . 5 ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)) → Σ𝑘𝐴 (𝐵 + 𝐶) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶))
8887expr 444 . . . 4 ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto𝐴 → Σ𝑘𝐴 (𝐵 + 𝐶) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶)))
8988exlimdv 2013 . . 3 ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴 → Σ𝑘𝐴 (𝐵 + 𝐶) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶)))
9089expimpd 441 . 2 (𝜑 → (((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴) → Σ𝑘𝐴 (𝐵 + 𝐶) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶)))
91 fsumadd.1 . . 3 (𝜑𝐴 ∈ Fin)
92 fz1f1o 14650 . . 3 (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)))
9391, 92syl 17 . 2 (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto𝐴)))
9412, 90, 93mpjaod 841 1 (𝜑 → Σ𝑘𝐴 (𝐵 + 𝐶) = (Σ𝑘𝐴 𝐵 + Σ𝑘𝐴 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wo 828   = wceq 1631  wex 1852  wcel 2145  wral 3061  Vcvv 3351  c0 4064  cmpt 4864  ccom 5254  wf 6028  1-1-ontowf1o 6031  cfv 6032  (class class class)co 6794  Fincfn 8110  cc 10137  0cc0 10139  1c1 10140   + caddc 10142  cn 11223  cuz 11889  ...cfz 12534  seqcseq 13009  chash 13322  Σcsu 14625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-inf2 8703  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-sup 8505  df-oi 8572  df-card 8966  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-n0 11496  df-z 11581  df-uz 11890  df-rp 12037  df-fz 12535  df-fzo 12675  df-seq 13010  df-exp 13069  df-hash 13323  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-clim 14428  df-sum 14626
This theorem is referenced by:  fsumsplit  14680  fsumsub  14728  binomlem  14769  binomfallfaclem2  14978  pwp1fsum  15323  pcbc  15812  csbren  23402  trirn  23403  ovollb2lem  23477  ovoliunlem1  23491  itg1addlem5  23688  itgsplit  23823  plyaddlem1  24190  basellem8  25036  logfaclbnd  25169  dchrvmasum2if  25408  mudivsum  25441  logsqvma  25453  selberglem1  25456  selberglem2  25457  selberg  25459  selberg2  25462  selberg3lem1  25468  selberg4  25472  pntsval2  25487  ax5seglem9  26039  finsumvtxdg2ssteplem4  26680  dvnmul  40677  dirkertrigeqlem2  40834  sge0xaddlem1  41168  sge0xaddlem2  41169  hoidmvlelem2  41331  altgsumbcALT  42660
  Copyright terms: Public domain W3C validator