fsumadd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > fsumadd		GIF version

Theorem fsumadd 11347

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.

Step	Hyp	Ref	Expression
1		00id 8039	. . . . 5 ⊢ (0 + 0) = 0
2		sum0 11329	. . . . . 6 ⊢ Σ𝑘 ∈ ∅ 𝐵 = 0
3		sum0 11329	. . . . . 6 ⊢ Σ𝑘 ∈ ∅ 𝐶 = 0
4	2, 3	oveq12i 5854	. . . . 5 ⊢ (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶) = (0 + 0)
5		sum0 11329	. . . . 5 ⊢ Σ𝑘 ∈ ∅ (𝐵 + 𝐶) = 0
6	1, 4, 5	3eqtr4ri 2197	. . . 4 ⊢ Σ𝑘 ∈ ∅ (𝐵 + 𝐶) = (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶)
7		sumeq1 11296	. . . 4 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = Σ𝑘 ∈ ∅ (𝐵 + 𝐶))
8		sumeq1 11296	. . . . 5 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵)
9		sumeq1 11296	. . . . 5 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
10	8, 9	oveq12d 5860	. . . 4 ⊢ (𝐴 = ∅ → (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶) = (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶))
11	6, 7, 10	3eqtr4a 2225	. . 3 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
12	11	a1i 9	. 2 ⊢ (𝜑 → (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)))
13		simprl 521	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈ ℕ)
14		nnuz 9501	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
15	13, 14	eleqtrdi 2259	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘1))
16		eqid 2165	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))
17		breq1 3985	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑛 ≤ (♯‘𝐴)))
18		fveq2 5486	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛))
19	17, 18	ifbieq1d 3542	. . . . . . . . . 10 ⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0))
20		elnnuz 9502	. . . . . . . . . . . 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 469	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
25	24	fmpttd 5640	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ)
26		simprr 522	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
27		f1of 5432	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴)
28	26, 27	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
29		fco 5353	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
30	25, 28, 29	syl2anc 409	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
31	30	ad2antrr 480	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
32		1zzd 9218	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 1 ∈ ℤ)
33	13	ad2antrr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (♯‘𝐴) ∈ ℕ)
34	33	nnzd 9312	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (♯‘𝐴) ∈ ℤ)
35		eluzelz 9475	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ ℤ)
36	35	ad2antlr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 𝑛 ∈ ℤ)
37	32, 34, 36	3jca 1167	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑛 ∈ ℤ))
38		eluzle 9478	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 1 ≤ 𝑛)
39	38	ad2antlr 481	. . . . . . . . . . . . . 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 9951	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...(♯‘𝐴)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ (♯‘𝐴))))
43	37, 41, 42	sylanbrc 414	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 𝑛 ∈ (1...(♯‘𝐴)))
44	31, 43	ffvelrnd 5621	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) ∈ ℂ)
45		0cnd 7892	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → 0 ∈ ℂ)
46	22	nnzd 9312	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → 𝑛 ∈ ℤ)
47	13	adantr 274	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℕ)
48	47	nnzd 9312	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℤ)
49		zdcle 9267	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑛 ≤ (♯‘𝐴))
50	46, 48, 49	syl2anc 409	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → DECID 𝑛 ≤ (♯‘𝐴))
51	44, 45, 50	ifcldadc 3549	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) ∈ ℂ)
52	16, 19, 22, 51	fvmptd3 5579	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0))
53	52, 51	eqeltrd 2243	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) ∈ ℂ)
54		eqid 2165	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))
55		fveq2 5486	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛))
56	17, 55	ifbieq1d 3542	. . . . . . . . . 10 ⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))
57		fsumadd.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
58	57	adantlr 469	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
59	58	fmpttd 5640	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ)
60	59	ad2antrr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ)
61	28	ad2antrr 480	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
62		fco 5353	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
63	60, 61, 62	syl2anc 409	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
64	63, 43	ffvelrnd 5621	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) ∈ ℂ)
65	64, 45, 50	ifcldadc 3549	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) ∈ ℂ)
66	54, 56, 22, 65	fvmptd3 5579	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))
67	66, 65	eqeltrd 2243	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛) ∈ ℂ)
68		simpll 519	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
69	28	ffvelrnda 5620	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝑓‘𝑛) ∈ 𝐴)
70		simpr 109	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴)
71	23, 57	addcld 7918	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℂ)
72		eqid 2165	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) = (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))
73	72	fvmpt2 5569	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ 𝐴 ∧ (𝐵 + 𝐶) ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶))
74	70, 71, 73	syl2anc 409	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶))
75		eqid 2165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
76	75	fvmpt2 5569	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = 𝐵)
77	70, 23, 76	syl2anc 409	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = 𝐵)
78		eqid 2165	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐶) = (𝑘 ∈ 𝐴 ↦ 𝐶)
79	78	fvmpt2 5569	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝐴 ∧ 𝐶 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = 𝐶)
80	70, 57, 79	syl2anc 409	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = 𝐶)
81	77, 80	oveq12d 5860	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) = (𝐵 + 𝐶))
82	74, 81	eqtr4d 2201	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)))
83	82	ralrimiva 2539	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)))
84	83	ad2antrr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)))
85		nffvmpt1 5497	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛))
86		nffvmpt1 5497	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))
87		nfcv 2308	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘 +
88		nffvmpt1 5497	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))
89	86, 87, 88	nfov 5872	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
90	85, 89	nfeq 2316	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
91		fveq2 5486	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)))
92		fveq2 5486	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
93		fveq2 5486	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
94	92, 93	oveq12d 5860	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑓‘𝑛) → (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))))
95	91, 94	eqeq12d 2180	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑓‘𝑛) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) ↔ ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))))
96	90, 95	rspc 2824	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))))
97	69, 84, 96	sylc 62	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))))
98		fvco3 5557	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)))
99	28, 98	sylan 281	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)))
100		fvco3 5557	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
101	28, 100	sylan 281	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
102		fvco3 5557	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
103	28, 102	sylan 281	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
104	101, 103	oveq12d 5860	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))))
105	97, 99, 104	3eqtr4d 2208	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)))
106	68, 43, 105	syl2anc 409	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)))
107	40	iftrued 3527	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛))
108	40	iftrued 3527	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛))
109	40	iftrued 3527	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛))
110	108, 109	oveq12d 5860	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)))
111	106, 107, 110	3eqtr4d 2208	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))
112	1	eqcomi 2169	. . . . . . . . . . 11 ⊢ 0 = (0 + 0)
113		simpr 109	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → ¬ 𝑛 ≤ (♯‘𝐴))
114	113	iffalsed 3530	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = 0)
115	113	iffalsed 3530	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = 0)
116	113	iffalsed 3530	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = 0)
117	115, 116	oveq12d 5860	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = (0 + 0))
118	112, 114, 117	3eqtr4a 2225	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))
119		exmiddc 826	. . . . . . . . . . 11 ⊢ (DECID 𝑛 ≤ (♯‘𝐴) → (𝑛 ≤ (♯‘𝐴) ∨ ¬ 𝑛 ≤ (♯‘𝐴)))
120	50, 119	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → (𝑛 ≤ (♯‘𝐴) ∨ ¬ 𝑛 ≤ (♯‘𝐴)))
121	111, 118, 120	mpjaodan 788	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))
122		eqid 2165	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))
123		fveq2 5486	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛))
124	17, 123	ifbieq1d 3542	. . . . . . . . . 10 ⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0))
125	71	fmpttd 5640	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ)
126	125	ad3antrrr 484	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ)
127		fco 5353	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
128	126, 61, 127	syl2anc 409	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
129	128, 43	ffvelrnd 5621	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) ∈ ℂ)
130	129, 45, 50	ifcldadc 3549	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) ∈ ℂ)
131	122, 124, 22, 130	fvmptd3 5579	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0))
132	52, 66	oveq12d 5860	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → (((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) + ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛)) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))
133	121, 131, 132	3eqtr4d 2208	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))‘𝑛) = (((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) + ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛)))
134	15, 53, 67, 133	ser3add 10440	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) = ((seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) + (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))))
135		fveq2 5486	. . . . . . . . 9 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)))
136	24, 58	addcld 7918	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℂ)
137	136	fmpttd 5640	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ)
138	137	ffvelrnda 5620	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) ∈ ℂ)
139	135, 13, 26, 138, 99	fsum3 11328	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)))
140		breq1 3985	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
141		fveq2 5486	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗))
142	140, 141	ifbieq1d 3542	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))
143	142	cbvmptv 4078	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))
144		seqeq3 10385	. . . . . . . . . 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 5487	. . . . . . . 8 ⊢ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))
147	139, 146	eqtrdi 2215	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)))
148		fveq2 5486	. . . . . . . . . 10 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
149	25	ffvelrnda 5620	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ)
150	148, 13, 26, 149, 101	fsum3 11328	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)))
151		fveq2 5486	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗))
152	140, 151	ifbieq1d 3542	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))
153	152	cbvmptv 4078	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))
154		seqeq3 10385	. . . . . . . . . . 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 5487	. . . . . . . . 9 ⊢ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))
157	150, 156	eqtrdi 2215	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)))
158		fveq2 5486	. . . . . . . . . 10 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
159	59	ffvelrnda 5620	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) ∈ ℂ)
160	158, 13, 26, 159, 103	fsum3 11328	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)))
161		fveq2 5486	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗))
162	140, 161	ifbieq1d 3542	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))
163	162	cbvmptv 4078	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))
164		seqeq3 10385	. . . . . . . . . . 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 5487	. . . . . . . . 9 ⊢ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))
167	160, 166	eqtrdi 2215	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)))
168	157, 167	oveq12d 5860	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = ((seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) + (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))))
169	134, 147, 168	3eqtr4d 2208	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)))
170	71	ralrimiva 2539	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 (𝐵 + 𝐶) ∈ ℂ)
171		sumfct 11315	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐴 (𝐵 + 𝐶) ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶))
172	170, 171	syl 14	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶))
173	172	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶))
174	23	ralrimiva 2539	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
175		sumfct 11315	. . . . . . . . 9 ⊢ (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵)
176	174, 175	syl 14	. . . . . . . 8 ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵)
177	57	ralrimiva 2539	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ)
178		sumfct 11315	. . . . . . . . 9 ⊢ (∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶)
179	177, 178	syl 14	. . . . . . . 8 ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶)
180	176, 179	oveq12d 5860	. . . . . . 7 ⊢ (𝜑 → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
181	180	adantr 274	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
182	169, 173, 181	3eqtr3d 2206	. . . . 5 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
183	182	expr 373	. . . 4 ⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)))
184	183	exlimdv 1807	. . 3 ⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)))
185	184	expimpd 361	. 2 ⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)))
186		fsumadd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
187		fz1f1o 11316	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
188	186, 187	syl 14	. 2 ⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
189	12, 185, 188	mpjaod 708	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ∨ wo 698 DECID wdc 824 ∧ w3a 968 = wceq 1343 ∃wex 1480 ∈ wcel 2136 ∀wral 2444 ∅c0 3409 ifcif 3520 class class class wbr 3982 ↦ cmpt 4043 ∘ ccom 4608 ⟶wf 5184 –1-1-onto→wf1o 5187 ‘cfv 5188 (class class class)co 5842 Fincfn 6706 ℂcc 7751 0cc0 7753 1c1 7754 + caddc 7756 ≤ cle 7934 ℕcn 8857 ℤcz 9191 ℤ_≥cuz 9466 ...cfz 9944 seqcseq 10380 ♯chash 10688 Σcsu 11294

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-coll 4097 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565 ax-cnex 7844 ax-resscn 7845 ax-1cn 7846 ax-1re 7847 ax-icn 7848 ax-addcl 7849 ax-addrcl 7850 ax-mulcl 7851 ax-mulrcl 7852 ax-addcom 7853 ax-mulcom 7854 ax-addass 7855 ax-mulass 7856 ax-distr 7857 ax-i2m1 7858 ax-0lt1 7859 ax-1rid 7860 ax-0id 7861 ax-rnegex 7862 ax-precex 7863 ax-cnre 7864 ax-pre-ltirr 7865 ax-pre-ltwlin 7866 ax-pre-lttrn 7867 ax-pre-apti 7868 ax-pre-ltadd 7869 ax-pre-mulgt0 7870 ax-pre-mulext 7871 ax-arch 7872 ax-caucvg 7873

This theorem depends on definitions: df-bi 116 df-dc 825 df-3or 969 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-nel 2432 df-ral 2449 df-rex 2450 df-reu 2451 df-rmo 2452 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-if 3521 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-po 4274 df-iso 4275 df-iord 4344 df-on 4346 df-ilim 4347 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-res 4616 df-ima 4617 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-f1 5193 df-fo 5194 df-f1o 5195 df-fv 5196 df-isom 5197 df-riota 5798 df-ov 5845 df-oprab 5846 df-mpo 5847 df-1st 6108 df-2nd 6109 df-recs 6273 df-irdg 6338 df-frec 6359 df-1o 6384 df-oadd 6388 df-er 6501 df-en 6707 df-dom 6708 df-fin 6709 df-pnf 7935 df-mnf 7936 df-xr 7937 df-ltxr 7938 df-le 7939 df-sub 8071 df-neg 8072 df-reap 8473 df-ap 8480 df-div 8569 df-inn 8858 df-2 8916 df-3 8917 df-4 8918 df-n0 9115 df-z 9192 df-uz 9467 df-q 9558 df-rp 9590 df-fz 9945 df-fzo 10078 df-seqfrec 10381 df-exp 10455 df-ihash 10689 df-cj 10784 df-re 10785 df-im 10786 df-rsqrt 10940 df-abs 10941 df-clim 11220 df-sumdc 11295

This theorem is referenced by: fsumsplit 11348 fsumsub 11393 binomlem 11424 pcbc 12281

W3C validator