fsumadd - Intuitionistic Logic Explorer

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

Theorem fsumadd 11588

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 8184	. . . . 5 ⊢ (0 + 0) = 0
2		sum0 11570	. . . . . 6 ⊢ Σ𝑘 ∈ ∅ 𝐵 = 0
3		sum0 11570	. . . . . 6 ⊢ Σ𝑘 ∈ ∅ 𝐶 = 0
4	2, 3	oveq12i 5937	. . . . 5 ⊢ (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶) = (0 + 0)
5		sum0 11570	. . . . 5 ⊢ Σ𝑘 ∈ ∅ (𝐵 + 𝐶) = 0
6	1, 4, 5	3eqtr4ri 2228	. . . 4 ⊢ Σ𝑘 ∈ ∅ (𝐵 + 𝐶) = (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶)
7		sumeq1 11537	. . . 4 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = Σ𝑘 ∈ ∅ (𝐵 + 𝐶))
8		sumeq1 11537	. . . . 5 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵)
9		sumeq1 11537	. . . . 5 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
10	8, 9	oveq12d 5943	. . . 4 ⊢ (𝐴 = ∅ → (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶) = (Σ𝑘 ∈ ∅ 𝐵 + Σ𝑘 ∈ ∅ 𝐶))
11	6, 7, 10	3eqtr4a 2255	. . 3 ⊢ (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
12	11	a1i 9	. 2 ⊢ (𝜑 → (𝐴 = ∅ → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)))
13		simprl 529	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈ ℕ)
14		nnuz 9654	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
15	13, 14	eleqtrdi 2289	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (♯‘𝐴) ∈ (ℤ_≥‘1))
16		eqid 2196	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))
17		breq1 4037	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (𝑗 ≤ (♯‘𝐴) ↔ 𝑛 ≤ (♯‘𝐴)))
18		fveq2 5561	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛))
19	17, 18	ifbieq1d 3584	. . . . . . . . . 10 ⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0))
20		elnnuz 9655	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈ (ℤ_≥‘1))
21	20	biimpri 133	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ ℕ)
22	21	adantl 277	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → 𝑛 ∈ ℕ)
23		fsumadd.2	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
24	23	adantlr 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
25	24	fmpttd 5720	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ)
26		simprr 531	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)
27		f1of 5507	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑓:(1...(♯‘𝐴))⟶𝐴)
28	26, 27	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
29		fco 5426	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
30	25, 28, 29	syl2anc 411	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
31	30	ad2antrr 488	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
32		1zzd 9370	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 1 ∈ ℤ)
33	13	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (♯‘𝐴) ∈ ℕ)
34	33	nnzd 9464	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (♯‘𝐴) ∈ ℤ)
35		eluzelz 9627	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 𝑛 ∈ ℤ)
36	35	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 𝑛 ∈ ℤ)
37	32, 34, 36	3jca 1179	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑛 ∈ ℤ))
38		eluzle 9630	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ (ℤ_≥‘1) → 1 ≤ 𝑛)
39	38	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 1 ≤ 𝑛)
40		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 𝑛 ≤ (♯‘𝐴))
41	39, 40	jca 306	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (1 ≤ 𝑛 ∧ 𝑛 ≤ (♯‘𝐴)))
42		elfz2 10107	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (1...(♯‘𝐴)) ↔ ((1 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (1 ≤ 𝑛 ∧ 𝑛 ≤ (♯‘𝐴))))
43	37, 41, 42	sylanbrc 417	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 𝑛 ∈ (1...(♯‘𝐴)))
44	31, 43	ffvelcdmd 5701	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) ∈ ℂ)
45		0cnd 8036	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → 0 ∈ ℂ)
46	22	nnzd 9464	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → 𝑛 ∈ ℤ)
47	13	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℕ)
48	47	nnzd 9464	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → (♯‘𝐴) ∈ ℤ)
49		zdcle 9419	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝑛 ≤ (♯‘𝐴))
50	46, 48, 49	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → DECID 𝑛 ≤ (♯‘𝐴))
51	44, 45, 50	ifcldadc 3591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) ∈ ℂ)
52	16, 19, 22, 51	fvmptd3 5658	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0))
53	52, 51	eqeltrd 2273	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) ∈ ℂ)
54		eqid 2196	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))
55		fveq2 5561	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛))
56	17, 55	ifbieq1d 3584	. . . . . . . . . 10 ⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))
57		fsumadd.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
58	57	adantlr 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
59	58	fmpttd 5720	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ)
60	59	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ)
61	28	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → 𝑓:(1...(♯‘𝐴))⟶𝐴)
62		fco 5426	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ 𝐴 ↦ 𝐶):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
63	60, 61, 62	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
64	63, 43	ffvelcdmd 5701	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) ∈ ℂ)
65	64, 45, 50	ifcldadc 3591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) ∈ ℂ)
66	54, 56, 22, 65	fvmptd3 5658	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0))
67	66, 65	eqeltrd 2273	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛) ∈ ℂ)
68		simpll 527	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
69	28	ffvelcdmda 5700	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝑓‘𝑛) ∈ 𝐴)
70		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴)
71	23, 57	addcld 8063	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℂ)
72		eqid 2196	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) = (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))
73	72	fvmpt2 5648	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ 𝐴 ∧ (𝐵 + 𝐶) ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶))
74	70, 71, 73	syl2anc 411	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (𝐵 + 𝐶))
75		eqid 2196	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
76	75	fvmpt2 5648	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝐴 ∧ 𝐵 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = 𝐵)
77	70, 23, 76	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = 𝐵)
78		eqid 2196	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐶) = (𝑘 ∈ 𝐴 ↦ 𝐶)
79	78	fvmpt2 5648	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ 𝐴 ∧ 𝐶 ∈ ℂ) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = 𝐶)
80	70, 57, 79	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = 𝐶)
81	77, 80	oveq12d 5943	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) = (𝐵 + 𝐶))
82	74, 81	eqtr4d 2232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)))
83	82	ralrimiva 2570	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)))
84	83	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)))
85		nffvmpt1 5572	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛))
86		nffvmpt1 5572	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛))
87		nfcv 2339	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘 +
88		nffvmpt1 5572	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))
89	86, 87, 88	nfov 5955	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑘(((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
90	85, 89	nfeq 2347	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
91		fveq2 5561	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)))
92		fveq2 5561	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
93		fveq2 5561	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
94	92, 93	oveq12d 5943	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = (𝑓‘𝑛) → (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))))
95	91, 94	eqeq12d 2211	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = (𝑓‘𝑛) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) ↔ ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))))
96	90, 95	rspc 2862	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑛) ∈ 𝐴 → (∀𝑘 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑘) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑘) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑘)) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))))
97	69, 84, 96	sylc 62	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))))
98		fvco3 5635	. . . . . . . . . . . . . 14 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)))
99	28, 98	sylan 283	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)))
100		fvco3 5635	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
101	28, 100	sylan 283	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
102		fvco3 5635	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:(1...(♯‘𝐴))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
103	28, 102	sylan 283	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
104	101, 103	oveq12d 5943	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)) = (((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)) + ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛))))
105	97, 99, 104	3eqtr4d 2239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)))
106	68, 43, 105	syl2anc 411	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)))
107	40	iftrued 3569	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛))
108	40	iftrued 3569	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛))
109	40	iftrued 3569	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛))
110	108, 109	oveq12d 5943	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = ((((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) + (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛)))
111	106, 107, 110	3eqtr4d 2239	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))
112	1	eqcomi 2200	. . . . . . . . . . 11 ⊢ 0 = (0 + 0)
113		simpr 110	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → ¬ 𝑛 ≤ (♯‘𝐴))
114	113	iffalsed 3572	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = 0)
115	113	iffalsed 3572	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = 0)
116	113	iffalsed 3572	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = 0)
117	115, 116	oveq12d 5943	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = (0 + 0))
118	112, 114, 117	3eqtr4a 2255	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑛 ≤ (♯‘𝐴)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))
119		exmiddc 837	. . . . . . . . . . 11 ⊢ (DECID 𝑛 ≤ (♯‘𝐴) → (𝑛 ≤ (♯‘𝐴) ∨ ¬ 𝑛 ≤ (♯‘𝐴)))
120	50, 119	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → (𝑛 ≤ (♯‘𝐴) ∨ ¬ 𝑛 ≤ (♯‘𝐴)))
121	111, 118, 120	mpjaodan 799	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))
122		eqid 2196	. . . . . . . . . 10 ⊢ (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))
123		fveq2 5561	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑛 → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛))
124	17, 123	ifbieq1d 3584	. . . . . . . . . 10 ⊢ (𝑗 = 𝑛 → if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0))
125	71	fmpttd 5720	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ)
126	125	ad3antrrr 492	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ)
127		fco 5426	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ ∧ 𝑓:(1...(♯‘𝐴))⟶𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
128	126, 61, 127	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓):(1...(♯‘𝐴))⟶ℂ)
129	128, 43	ffvelcdmd 5701	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) ∧ 𝑛 ≤ (♯‘𝐴)) → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) ∈ ℂ)
130	129, 45, 50	ifcldadc 3591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) ∈ ℂ)
131	122, 124, 22, 130	fvmptd3 5658	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))‘𝑛) = if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0))
132	52, 66	oveq12d 5943	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → (((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) + ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛)) = (if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) + if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))
133	121, 131, 132	3eqtr4d 2239	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑛 ∈ (ℤ_≥‘1)) → ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))‘𝑛) = (((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))‘𝑛) + ((𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))‘𝑛)))
134	15, 53, 67, 133	ser3add 10631	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) = ((seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) + (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))))
135		fveq2 5561	. . . . . . . . 9 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘(𝑓‘𝑛)))
136	24, 58	addcld 8063	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑘 ∈ 𝐴) → (𝐵 + 𝐶) ∈ ℂ)
137	136	fmpttd 5720	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)):𝐴⟶ℂ)
138	137	ffvelcdmda 5700	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) ∈ ℂ)
139	135, 13, 26, 138, 99	fsum3 11569	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)))
140		breq1 4037	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → (𝑛 ≤ (♯‘𝐴) ↔ 𝑗 ≤ (♯‘𝐴)))
141		fveq2 5561	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗))
142	140, 141	ifbieq1d 3584	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))
143	142	cbvmptv 4130	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0))
144		seqeq3 10561	. . . . . . . . . 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 5562	. . . . . . . 8 ⊢ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))
147	139, 146	eqtrdi 2245	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶)) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)))
148		fveq2 5561	. . . . . . . . . 10 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝑓‘𝑛)))
149	25	ffvelcdmda 5700	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ)
150	148, 13, 26, 149, 101	fsum3 11569	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)))
151		fveq2 5561	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗))
152	140, 151	ifbieq1d 3584	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))
153	152	cbvmptv 4130	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0))
154		seqeq3 10561	. . . . . . . . . . 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 5562	. . . . . . . . 9 ⊢ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))
157	150, 156	eqtrdi 2245	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)))
158		fveq2 5561	. . . . . . . . . 10 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘(𝑓‘𝑛)))
159	59	ffvelcdmda 5700	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) ∈ ℂ)
160	158, 13, 26, 159, 103	fsum3 11569	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)))
161		fveq2 5561	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑗 → (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛) = (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗))
162	140, 161	ifbieq1d 3584	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑗 → if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0) = if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))
163	162	cbvmptv 4130	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)) = (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0))
164		seqeq3 10561	. . . . . . . . . . 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 5562	. . . . . . . . 9 ⊢ (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑛), 0)))‘(♯‘𝐴)) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))
167	160, 166	eqtrdi 2245	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)))
168	157, 167	oveq12d 5943	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = ((seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴)) + (seq1( + , (𝑗 ∈ ℕ ↦ if(𝑗 ≤ (♯‘𝐴), (((𝑘 ∈ 𝐴 ↦ 𝐶) ∘ 𝑓)‘𝑗), 0)))‘(♯‘𝐴))))
169	134, 147, 168	3eqtr4d 2239	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)))
170	71	ralrimiva 2570	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 (𝐵 + 𝐶) ∈ ℂ)
171		sumfct 11556	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐴 (𝐵 + 𝐶) ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶))
172	170, 171	syl 14	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶))
173	172	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ (𝐵 + 𝐶))‘𝑚) = Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶))
174	23	ralrimiva 2570	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
175		sumfct 11556	. . . . . . . . 9 ⊢ (∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵)
176	174, 175	syl 14	. . . . . . . 8 ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵)
177	57	ralrimiva 2570	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ)
178		sumfct 11556	. . . . . . . . 9 ⊢ (∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶)
179	177, 178	syl 14	. . . . . . . 8 ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶)
180	176, 179	oveq12d 5943	. . . . . . 7 ⊢ (𝜑 → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
181	180	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → (Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) + Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚)) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
182	169, 173, 181	3eqtr3d 2237	. . . . 5 ⊢ ((𝜑 ∧ ((♯‘𝐴) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)) → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))
183	182	expr 375	. . . 4 ⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)))
184	183	exlimdv 1833	. . 3 ⊢ ((𝜑 ∧ (♯‘𝐴) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)))
185	184	expimpd 363	. 2 ⊢ (𝜑 → (((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴) → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶)))
186		fsumadd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ Fin)
187		fz1f1o 11557	. . 3 ⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
188	186, 187	syl 14	. 2 ⊢ (𝜑 → (𝐴 = ∅ ∨ ((♯‘𝐴) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐴))–1-1-onto→𝐴)))
189	12, 185, 188	mpjaod 719	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 (𝐵 + 𝐶) = (Σ𝑘 ∈ 𝐴 𝐵 + Σ𝑘 ∈ 𝐴 𝐶))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ∨ wo 709 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∃wex 1506 ∈ wcel 2167 ∀wral 2475 ∅c0 3451 ifcif 3562 class class class wbr 4034 ↦ cmpt 4095 ∘ ccom 4668 ⟶wf 5255 –1-1-onto→wf1o 5258 ‘cfv 5259 (class class class)co 5925 Fincfn 6808 ℂcc 7894 0cc0 7896 1c1 7897 + caddc 7899 ≤ cle 8079 ℕcn 9007 ℤcz 9343 ℤ_≥cuz 9618 ...cfz 10100 seqcseq 10556 ♯chash 10884 Σcsu 11535

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4149 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-iinf 4625 ax-cnex 7987 ax-resscn 7988 ax-1cn 7989 ax-1re 7990 ax-icn 7991 ax-addcl 7992 ax-addrcl 7993 ax-mulcl 7994 ax-mulrcl 7995 ax-addcom 7996 ax-mulcom 7997 ax-addass 7998 ax-mulass 7999 ax-distr 8000 ax-i2m1 8001 ax-0lt1 8002 ax-1rid 8003 ax-0id 8004 ax-rnegex 8005 ax-precex 8006 ax-cnre 8007 ax-pre-ltirr 8008 ax-pre-ltwlin 8009 ax-pre-lttrn 8010 ax-pre-apti 8011 ax-pre-ltadd 8012 ax-pre-mulgt0 8013 ax-pre-mulext 8014 ax-arch 8015 ax-caucvg 8016

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-if 3563 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-iun 3919 df-br 4035 df-opab 4096 df-mpt 4097 df-tr 4133 df-id 4329 df-po 4332 df-iso 4333 df-iord 4402 df-on 4404 df-ilim 4405 df-suc 4407 df-iom 4628 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-rn 4675 df-res 4676 df-ima 4677 df-iota 5220 df-fun 5261 df-fn 5262 df-f 5263 df-f1 5264 df-fo 5265 df-f1o 5266 df-fv 5267 df-isom 5268 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-1st 6207 df-2nd 6208 df-recs 6372 df-irdg 6437 df-frec 6458 df-1o 6483 df-oadd 6487 df-er 6601 df-en 6809 df-dom 6810 df-fin 6811 df-pnf 8080 df-mnf 8081 df-xr 8082 df-ltxr 8083 df-le 8084 df-sub 8216 df-neg 8217 df-reap 8619 df-ap 8626 df-div 8717 df-inn 9008 df-2 9066 df-3 9067 df-4 9068 df-n0 9267 df-z 9344 df-uz 9619 df-q 9711 df-rp 9746 df-fz 10101 df-fzo 10235 df-seqfrec 10557 df-exp 10648 df-ihash 10885 df-cj 11024 df-re 11025 df-im 11026 df-rsqrt 11180 df-abs 11181 df-clim 11461 df-sumdc 11536

This theorem is referenced by: fsumsplit 11589 fsumsub 11634 binomlem 11665 pcbc 12545 plyaddlem1 15067

W3C validator