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

Theorem fsumss 15076
 Description: Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.)
Hypotheses
Ref Expression
sumss.1 (𝜑𝐴𝐵)
sumss.2 ((𝜑𝑘𝐴) → 𝐶 ∈ ℂ)
sumss.3 ((𝜑𝑘 ∈ (𝐵𝐴)) → 𝐶 = 0)
fsumss.4 (𝜑𝐵 ∈ Fin)
Assertion
Ref Expression
fsumss (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
Distinct variable groups:   𝐴,𝑘   𝐵,𝑘   𝜑,𝑘
Allowed substitution hint:   𝐶(𝑘)

Proof of Theorem fsumss
Dummy variables 𝑓 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sumss.1 . . . . 5 (𝜑𝐴𝐵)
21adantr 484 . . . 4 ((𝜑𝐵 = ∅) → 𝐴𝐵)
3 sumss.2 . . . . 5 ((𝜑𝑘𝐴) → 𝐶 ∈ ℂ)
43adantlr 714 . . . 4 (((𝜑𝐵 = ∅) ∧ 𝑘𝐴) → 𝐶 ∈ ℂ)
5 sumss.3 . . . . 5 ((𝜑𝑘 ∈ (𝐵𝐴)) → 𝐶 = 0)
65adantlr 714 . . . 4 (((𝜑𝐵 = ∅) ∧ 𝑘 ∈ (𝐵𝐴)) → 𝐶 = 0)
7 simpr 488 . . . . 5 ((𝜑𝐵 = ∅) → 𝐵 = ∅)
8 0ss 4304 . . . . 5 ∅ ⊆ (ℤ‘0)
97, 8eqsstrdi 3969 . . . 4 ((𝜑𝐵 = ∅) → 𝐵 ⊆ (ℤ‘0))
102, 4, 6, 9sumss 15075 . . 3 ((𝜑𝐵 = ∅) → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
1110ex 416 . 2 (𝜑 → (𝐵 = ∅ → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶))
12 cnvimass 5916 . . . . . . . . 9 (𝑓𝐴) ⊆ dom 𝑓
13 simprr 772 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)
14 f1of 6590 . . . . . . . . . 10 (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑓:(1...(♯‘𝐵))⟶𝐵)
1513, 14syl 17 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓:(1...(♯‘𝐵))⟶𝐵)
1612, 15fssdm 6504 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓𝐴) ⊆ (1...(♯‘𝐵)))
1715ffnd 6488 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓 Fn (1...(♯‘𝐵)))
18 elpreima 6805 . . . . . . . . . . . 12 (𝑓 Fn (1...(♯‘𝐵)) → (𝑛 ∈ (𝑓𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴)))
1917, 18syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑛 ∈ (𝑓𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴)))
2015ffvelrnda 6828 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓𝑛) ∈ 𝐵)
2120ex 416 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑛 ∈ (1...(♯‘𝐵)) → (𝑓𝑛) ∈ 𝐵))
2221adantrd 495 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → ((𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴) → (𝑓𝑛) ∈ 𝐵))
2319, 22sylbid 243 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑛 ∈ (𝑓𝐴) → (𝑓𝑛) ∈ 𝐵))
2423imp 410 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (𝑓𝐴)) → (𝑓𝑛) ∈ 𝐵)
253ex 416 . . . . . . . . . . . . . 14 (𝜑 → (𝑘𝐴𝐶 ∈ ℂ))
2625adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑘𝐵) → (𝑘𝐴𝐶 ∈ ℂ))
27 eldif 3891 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐵𝐴) ↔ (𝑘𝐵 ∧ ¬ 𝑘𝐴))
28 0cn 10624 . . . . . . . . . . . . . . . 16 0 ∈ ℂ
295, 28eqeltrdi 2898 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵𝐴)) → 𝐶 ∈ ℂ)
3027, 29sylan2br 597 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑘𝐵 ∧ ¬ 𝑘𝐴)) → 𝐶 ∈ ℂ)
3130expr 460 . . . . . . . . . . . . 13 ((𝜑𝑘𝐵) → (¬ 𝑘𝐴𝐶 ∈ ℂ))
3226, 31pm2.61d 182 . . . . . . . . . . . 12 ((𝜑𝑘𝐵) → 𝐶 ∈ ℂ)
3332fmpttd 6856 . . . . . . . . . . 11 (𝜑 → (𝑘𝐵𝐶):𝐵⟶ℂ)
3433adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑘𝐵𝐶):𝐵⟶ℂ)
3534ffvelrnda 6828 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ (𝑓𝑛) ∈ 𝐵) → ((𝑘𝐵𝐶)‘(𝑓𝑛)) ∈ ℂ)
3624, 35syldan 594 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (𝑓𝐴)) → ((𝑘𝐵𝐶)‘(𝑓𝑛)) ∈ ℂ)
37 eldifi 4054 . . . . . . . . . . . 12 (𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴)) → 𝑛 ∈ (1...(♯‘𝐵)))
3837, 20sylan2 595 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑓𝑛) ∈ 𝐵)
39 eldifn 4055 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴)) → ¬ 𝑛 ∈ (𝑓𝐴))
4039adantl 485 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ¬ 𝑛 ∈ (𝑓𝐴))
4137adantl 485 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → 𝑛 ∈ (1...(♯‘𝐵)))
4219adantr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑛 ∈ (𝑓𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓𝑛) ∈ 𝐴)))
4341, 42mpbirand 706 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑛 ∈ (𝑓𝐴) ↔ (𝑓𝑛) ∈ 𝐴))
4440, 43mtbid 327 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ¬ (𝑓𝑛) ∈ 𝐴)
4538, 44eldifd 3892 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑓𝑛) ∈ (𝐵𝐴))
46 difss 4059 . . . . . . . . . . . . 13 (𝐵𝐴) ⊆ 𝐵
47 resmpt 5872 . . . . . . . . . . . . 13 ((𝐵𝐴) ⊆ 𝐵 → ((𝑘𝐵𝐶) ↾ (𝐵𝐴)) = (𝑘 ∈ (𝐵𝐴) ↦ 𝐶))
4846, 47ax-mp 5 . . . . . . . . . . . 12 ((𝑘𝐵𝐶) ↾ (𝐵𝐴)) = (𝑘 ∈ (𝐵𝐴) ↦ 𝐶)
4948fveq1i 6646 . . . . . . . . . . 11 (((𝑘𝐵𝐶) ↾ (𝐵𝐴))‘(𝑓𝑛)) = ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛))
50 fvres 6664 . . . . . . . . . . 11 ((𝑓𝑛) ∈ (𝐵𝐴) → (((𝑘𝐵𝐶) ↾ (𝐵𝐴))‘(𝑓𝑛)) = ((𝑘𝐵𝐶)‘(𝑓𝑛)))
5149, 50syl5eqr 2847 . . . . . . . . . 10 ((𝑓𝑛) ∈ (𝐵𝐴) → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) = ((𝑘𝐵𝐶)‘(𝑓𝑛)))
5245, 51syl 17 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) = ((𝑘𝐵𝐶)‘(𝑓𝑛)))
53 c0ex 10626 . . . . . . . . . . . . . . 15 0 ∈ V
5453elsn2 4564 . . . . . . . . . . . . . 14 (𝐶 ∈ {0} ↔ 𝐶 = 0)
555, 54sylibr 237 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵𝐴)) → 𝐶 ∈ {0})
5655fmpttd 6856 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (𝐵𝐴) ↦ 𝐶):(𝐵𝐴)⟶{0})
5756ad2antrr 725 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → (𝑘 ∈ (𝐵𝐴) ↦ 𝐶):(𝐵𝐴)⟶{0})
5857, 45ffvelrnd 6829 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) ∈ {0})
59 elsni 4542 . . . . . . . . . 10 (((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) ∈ {0} → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) = 0)
6058, 59syl 17 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑘 ∈ (𝐵𝐴) ↦ 𝐶)‘(𝑓𝑛)) = 0)
6152, 60eqtr3d 2835 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (𝑓𝐴))) → ((𝑘𝐵𝐶)‘(𝑓𝑛)) = 0)
62 fzssuz 12945 . . . . . . . . 9 (1...(♯‘𝐵)) ⊆ (ℤ‘1)
6362a1i 11 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (1...(♯‘𝐵)) ⊆ (ℤ‘1))
6416, 36, 61, 63sumss 15075 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑛 ∈ (𝑓𝐴)((𝑘𝐵𝐶)‘(𝑓𝑛)) = Σ𝑛 ∈ (1...(♯‘𝐵))((𝑘𝐵𝐶)‘(𝑓𝑛)))
651ad2antrr 725 . . . . . . . . . . . 12 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → 𝐴𝐵)
6665resmptd 5875 . . . . . . . . . . 11 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → ((𝑘𝐵𝐶) ↾ 𝐴) = (𝑘𝐴𝐶))
6766fveq1d 6647 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → (((𝑘𝐵𝐶) ↾ 𝐴)‘𝑚) = ((𝑘𝐴𝐶)‘𝑚))
68 fvres 6664 . . . . . . . . . . 11 (𝑚𝐴 → (((𝑘𝐵𝐶) ↾ 𝐴)‘𝑚) = ((𝑘𝐵𝐶)‘𝑚))
6968adantl 485 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → (((𝑘𝐵𝐶) ↾ 𝐴)‘𝑚) = ((𝑘𝐵𝐶)‘𝑚))
7067, 69eqtr3d 2835 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → ((𝑘𝐴𝐶)‘𝑚) = ((𝑘𝐵𝐶)‘𝑚))
7170sumeq2dv 15054 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑚𝐴 ((𝑘𝐵𝐶)‘𝑚))
72 fveq2 6645 . . . . . . . . 9 (𝑚 = (𝑓𝑛) → ((𝑘𝐵𝐶)‘𝑚) = ((𝑘𝐵𝐶)‘(𝑓𝑛)))
73 fzfid 13338 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (1...(♯‘𝐵)) ∈ Fin)
7473, 15fisuppfi 8827 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓𝐴) ∈ Fin)
75 f1of1 6589 . . . . . . . . . . . 12 (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑓:(1...(♯‘𝐵))–1-1𝐵)
7613, 75syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1𝐵)
77 f1ores 6604 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝐵))–1-1𝐵 ∧ (𝑓𝐴) ⊆ (1...(♯‘𝐵))) → (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto→(𝑓 “ (𝑓𝐴)))
7876, 16, 77syl2anc 587 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto→(𝑓 “ (𝑓𝐴)))
79 f1ofo 6597 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵𝑓:(1...(♯‘𝐵))–onto𝐵)
8013, 79syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝑓:(1...(♯‘𝐵))–onto𝐵)
811adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → 𝐴𝐵)
82 foimacnv 6607 . . . . . . . . . . . 12 ((𝑓:(1...(♯‘𝐵))–onto𝐵𝐴𝐵) → (𝑓 “ (𝑓𝐴)) = 𝐴)
8380, 81, 82syl2anc 587 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓 “ (𝑓𝐴)) = 𝐴)
8483f1oeq3d 6587 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → ((𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto→(𝑓 “ (𝑓𝐴)) ↔ (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto𝐴))
8578, 84mpbid 235 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → (𝑓 ↾ (𝑓𝐴)):(𝑓𝐴)–1-1-onto𝐴)
86 fvres 6664 . . . . . . . . . 10 (𝑛 ∈ (𝑓𝐴) → ((𝑓 ↾ (𝑓𝐴))‘𝑛) = (𝑓𝑛))
8786adantl 485 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (𝑓𝐴)) → ((𝑓 ↾ (𝑓𝐴))‘𝑛) = (𝑓𝑛))
8881sselda 3915 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → 𝑚𝐵)
8934ffvelrnda 6828 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐵) → ((𝑘𝐵𝐶)‘𝑚) ∈ ℂ)
9088, 89syldan 594 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑚𝐴) → ((𝑘𝐵𝐶)‘𝑚) ∈ ℂ)
9172, 74, 85, 87, 90fsumf1o 15074 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐵𝐶)‘𝑚) = Σ𝑛 ∈ (𝑓𝐴)((𝑘𝐵𝐶)‘(𝑓𝑛)))
9271, 91eqtrd 2833 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑛 ∈ (𝑓𝐴)((𝑘𝐵𝐶)‘(𝑓𝑛)))
93 eqidd 2799 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓𝑛) = (𝑓𝑛))
9472, 73, 13, 93, 89fsumf1o 15074 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐵 ((𝑘𝐵𝐶)‘𝑚) = Σ𝑛 ∈ (1...(♯‘𝐵))((𝑘𝐵𝐶)‘(𝑓𝑛)))
9564, 92, 943eqtr4d 2843 . . . . . 6 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑚𝐵 ((𝑘𝐵𝐶)‘𝑚))
96 sumfc 15060 . . . . . 6 Σ𝑚𝐴 ((𝑘𝐴𝐶)‘𝑚) = Σ𝑘𝐴 𝐶
97 sumfc 15060 . . . . . 6 Σ𝑚𝐵 ((𝑘𝐵𝐶)‘𝑚) = Σ𝑘𝐵 𝐶
9895, 96, 973eqtr3g 2856 . . . . 5 ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)) → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
9998expr 460 . . . 4 ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (𝑓:(1...(♯‘𝐵))–1-1-onto𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶))
10099exlimdv 1934 . . 3 ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶))
101100expimpd 457 . 2 (𝜑 → (((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵) → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶))
102 fsumss.4 . . 3 (𝜑𝐵 ∈ Fin)
103 fz1f1o 15061 . . 3 (𝐵 ∈ Fin → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)))
104102, 103syl 17 . 2 (𝜑 → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto𝐵)))
10511, 101, 104mpjaod 857 1 (𝜑 → Σ𝑘𝐴 𝐶 = Σ𝑘𝐵 𝐶)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ∖ cdif 3878   ⊆ wss 3881  ∅c0 4243  {csn 4525   ↦ cmpt 5110  ◡ccnv 5518   ↾ cres 5521   “ cima 5522   Fn wfn 6319  ⟶wf 6320  –1-1→wf1 6321  –onto→wfo 6322  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135  Fincfn 8494  ℂcc 10526  0cc0 10528  1c1 10529  ℕcn 11627  ℤ≥cuz 12233  ...cfz 12887  ♯chash 13688  Σcsu 15036 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7443  ax-inf2 9090  ax-cnex 10584  ax-resscn 10585  ax-1cn 10586  ax-icn 10587  ax-addcl 10588  ax-addrcl 10589  ax-mulcl 10590  ax-mulrcl 10591  ax-mulcom 10592  ax-addass 10593  ax-mulass 10594  ax-distr 10595  ax-i2m1 10596  ax-1ne0 10597  ax-1rid 10598  ax-rnegex 10599  ax-rrecex 10600  ax-cnre 10601  ax-pre-lttri 10602  ax-pre-lttrn 10603  ax-pre-ltadd 10604  ax-pre-mulgt0 10605  ax-pre-sup 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7563  df-1st 7673  df-2nd 7674  df-wrecs 7932  df-recs 7993  df-rdg 8031  df-1o 8087  df-oadd 8091  df-er 8274  df-en 8495  df-dom 8496  df-sdom 8497  df-fin 8498  df-sup 8892  df-oi 8960  df-card 9354  df-pnf 10668  df-mnf 10669  df-xr 10670  df-ltxr 10671  df-le 10672  df-sub 10863  df-neg 10864  df-div 11289  df-nn 11628  df-2 11690  df-3 11691  df-n0 11888  df-z 11972  df-uz 12234  df-rp 12380  df-fz 12888  df-fzo 13031  df-seq 13367  df-exp 13428  df-hash 13689  df-cj 14452  df-re 14453  df-im 14454  df-sqrt 14588  df-abs 14589  df-clim 14839  df-sum 15037 This theorem is referenced by:  sumss2  15077  rrxmval  24016  rrxmetlem  24018  itg1val2  24295  itg1addlem4  24310  itg1addlem5  24311  ply1termlem  24807  plyaddlem1  24817  plymullem1  24818  coeeulem  24828  coeidlem  24841  coeid3  24844  coefv0  24852  coemulhi  24858  coemulc  24859  dvply1  24887  vieta1lem2  24914  dvtaylp  24972  pserdvlem2  25030  basellem3  25675  musum  25783  muinv  25785  fsumvma  25804  chpub  25811  logexprlim  25816  dchrsum  25860  chebbnd1lem1  26060  rpvmasumlem  26078  dchrisum0fno1  26102  rplogsum  26118  indsum  31402  eulerpartlemgs2  31760  flcidc  40133  fsumsupp0  42235  elaa2lem  42890
 Copyright terms: Public domain W3C validator