fisumss - Intuitionistic Logic Explorer

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

Theorem fisumss 11753

Description: Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.)

**Hypotheses**
Ref	Expression
fsumss.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
fsumss.2	⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
fsumss.3	⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)
fisumss.adc	⊢ (𝜑 → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)
fsumss.4	⊢ (𝜑 → 𝐵 ∈ Fin)

**Assertion**
Ref	Expression
fisumss	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Distinct variable groups: 𝐴,𝑗,𝑘 𝐵,𝑗,𝑘 𝜑,𝑘 Allowed substitution hints: 𝜑(𝑗) 𝐶(𝑗,𝑘)

Proof of Theorem fisumss Dummy variables 𝑓 𝑢 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fsumss.1	. . . . . 6 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseq0 3504	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
3	1, 2	sylan 283	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ∅) → 𝐴 = ∅)
4	3	sumeq1d 11727	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ∅) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
5		simpr 110	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ∅) → 𝐵 = ∅)
6	5	sumeq1d 11727	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ∅) → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
7	4, 6	eqtr4d 2242	. . 3 ⊢ ((𝜑 ∧ 𝐵 = ∅) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
8	7	ex 115	. 2 ⊢ (𝜑 → (𝐵 = ∅ → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶))
9		cnvimass 5051	. . . . . . . . 9 ⊢ (^◡𝑓 “ 𝐴) ⊆ dom 𝑓
10		simprr 531	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)
11		f1of 5531	. . . . . . . . . 10 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))⟶𝐵)
12	10, 11	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))⟶𝐵)
13	9, 12	fssdm 5447	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (^◡𝑓 “ 𝐴) ⊆ (1...(♯‘𝐵)))
14	12	ffnd 5433	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓 Fn (1...(♯‘𝐵)))
15		elpreima 5709	. . . . . . . . . . . 12 ⊢ (𝑓 Fn (1...(♯‘𝐵)) → (𝑛 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴)))
16	14, 15	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴)))
17	12	ffvelcdmda 5725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓‘𝑛) ∈ 𝐵)
18	17	ex 115	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (1...(♯‘𝐵)) → (𝑓‘𝑛) ∈ 𝐵))
19	18	adantrd 279	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ((𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴) → (𝑓‘𝑛) ∈ 𝐵))
20	16, 19	sylbid 150	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (^◡𝑓 “ 𝐴) → (𝑓‘𝑛) ∈ 𝐵))
21	20	imp 124	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (^◡𝑓 “ 𝐴)) → (𝑓‘𝑛) ∈ 𝐵)
22		fsumss.2	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
23	22	ex 115	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ))
24	23	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ))
25		eldif 3177	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (𝐵 ∖ 𝐴) ↔ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴))
26		fsumss.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)
27		0cn 8077	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℂ
28	26, 27	eqeltrdi 2297	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ ℂ)
29	25, 28	sylan2br 288	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → 𝐶 ∈ ℂ)
30	29	expr 375	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (¬ 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ))
31		eleq1w 2267	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
32	31	dcbid 840	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴))
33		fisumss.adc	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)
34	33	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)
35		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
36	32, 34, 35	rspcdva 2884	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → DECID 𝑘 ∈ 𝐴)
37		exmiddc 838	. . . . . . . . . . . . . 14 ⊢ (DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
38	36, 37	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
39	24, 30, 38	mpjaod 720	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
40	39	fmpttd 5745	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ)
41	40	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ)
42	41	ffvelcdmda 5725	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) ∈ ℂ)
43	21, 42	syldan 282	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (^◡𝑓 “ 𝐴)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) ∈ ℂ)
44		eldifi 3297	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴)) → 𝑛 ∈ (1...(♯‘𝐵)))
45	44, 17	sylan2 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → (𝑓‘𝑛) ∈ 𝐵)
46		eldifn 3298	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴)) → ¬ 𝑛 ∈ (^◡𝑓 “ 𝐴))
47	46	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ¬ 𝑛 ∈ (^◡𝑓 “ 𝐴))
48	16	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → (𝑛 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴)))
49	44	adantl 277	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → 𝑛 ∈ (1...(♯‘𝐵)))
50	49	biantrurd 305	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑓‘𝑛) ∈ 𝐴 ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴)))
51	48, 50	bitr4d 191	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → (𝑛 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑓‘𝑛) ∈ 𝐴))
52	47, 51	mtbid 674	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ¬ (𝑓‘𝑛) ∈ 𝐴)
53	45, 52	eldifd 3178	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → (𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴))
54		difss 3301	. . . . . . . . . . . . 13 ⊢ (𝐵 ∖ 𝐴) ⊆ 𝐵
55		resmpt 5013	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∖ 𝐴) ⊆ 𝐵 → ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴)) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶))
56	54, 55	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴)) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)
57	56	fveq1i 5587	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴))‘(𝑓‘𝑛)) = ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛))
58		fvres 5610	. . . . . . . . . . 11 ⊢ ((𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴))‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
59	57, 58	eqtr3id 2253	. . . . . . . . . 10 ⊢ ((𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
60	53, 59	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
61		c0ex 8079	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
62	61	elsn2 3669	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ {0} ↔ 𝐶 = 0)
63	26, 62	sylibr 134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ {0})
64	63	fmpttd 5745	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶):(𝐵 ∖ 𝐴)⟶{0})
65	64	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶):(𝐵 ∖ 𝐴)⟶{0})
66	65, 53	ffvelcdmd 5726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) ∈ {0})
67		elsni 3653	. . . . . . . . . 10 ⊢ (((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) ∈ {0} → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = 0)
68	66, 67	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = 0)
69	60, 68	eqtr3d 2241	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) = 0)
70		eleq1 2269	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑓‘𝑢) → (𝑗 ∈ 𝐴 ↔ (𝑓‘𝑢) ∈ 𝐴))
71	70	dcbid 840	. . . . . . . . . . . 12 ⊢ (𝑗 = (𝑓‘𝑢) → (DECID 𝑗 ∈ 𝐴 ↔ DECID (𝑓‘𝑢) ∈ 𝐴))
72	33	ad3antrrr 492	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)
73	12	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑓:(1...(♯‘𝐵))⟶𝐵)
74		simpr 110	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑢 ∈ (1...(♯‘𝐵)))
75	73, 74	ffvelcdmd 5726	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → (𝑓‘𝑢) ∈ 𝐵)
76	71, 72, 75	rspcdva 2884	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → DECID (𝑓‘𝑢) ∈ 𝐴)
77	10	ad2antrr 488	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)
78		f1ofun 5533	. . . . . . . . . . . . . 14 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → Fun 𝑓)
79	77, 78	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → Fun 𝑓)
80		f1odm 5535	. . . . . . . . . . . . . . 15 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → dom 𝑓 = (1...(♯‘𝐵)))
81	77, 80	syl 14	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → dom 𝑓 = (1...(♯‘𝐵)))
82	74, 81	eleqtrrd 2286	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑢 ∈ dom 𝑓)
83		fvimacnv 5705	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑓 ∧ 𝑢 ∈ dom 𝑓) → ((𝑓‘𝑢) ∈ 𝐴 ↔ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
84	79, 82, 83	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → ((𝑓‘𝑢) ∈ 𝐴 ↔ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
85	84	dcbid 840	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → (DECID (𝑓‘𝑢) ∈ 𝐴 ↔ DECID 𝑢 ∈ (^◡𝑓 “ 𝐴)))
86	76, 85	mpbid 147	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → DECID 𝑢 ∈ (^◡𝑓 “ 𝐴))
87		elpreima 5709	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 Fn (1...(♯‘𝐵)) → (𝑢 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑢 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑢) ∈ 𝐴)))
88		simpl 109	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑢) ∈ 𝐴) → 𝑢 ∈ (1...(♯‘𝐵)))
89	87, 88	biimtrdi 163	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn (1...(♯‘𝐵)) → (𝑢 ∈ (^◡𝑓 “ 𝐴) → 𝑢 ∈ (1...(♯‘𝐵))))
90	89	con3d 632	. . . . . . . . . . . . . . 15 ⊢ (𝑓 Fn (1...(♯‘𝐵)) → (¬ 𝑢 ∈ (1...(♯‘𝐵)) → ¬ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
91	14, 90	syl 14	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (¬ 𝑢 ∈ (1...(♯‘𝐵)) → ¬ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
92	91	adantr 276	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → (¬ 𝑢 ∈ (1...(♯‘𝐵)) → ¬ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
93	92	imp 124	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑢 ∈ (1...(♯‘𝐵))) → ¬ 𝑢 ∈ (^◡𝑓 “ 𝐴))
94	93	olcd 736	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑢 ∈ (1...(♯‘𝐵))) → (𝑢 ∈ (^◡𝑓 “ 𝐴) ∨ ¬ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
95		df-dc 837	. . . . . . . . . . 11 ⊢ (DECID 𝑢 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑢 ∈ (^◡𝑓 “ 𝐴) ∨ ¬ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
96	94, 95	sylibr 134	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑢 ∈ (1...(♯‘𝐵))) → DECID 𝑢 ∈ (^◡𝑓 “ 𝐴))
97		eluzelz 9670	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (ℤ_≥‘1) → 𝑢 ∈ ℤ)
98	97	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → 𝑢 ∈ ℤ)
99		1zzd 9412	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → 1 ∈ ℤ)
100		simplrl 535	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → (♯‘𝐵) ∈ ℕ)
101	100	nnzd 9507	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → (♯‘𝐵) ∈ ℤ)
102		fzdcel 10175	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ℤ ∧ 1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → DECID 𝑢 ∈ (1...(♯‘𝐵)))
103	98, 99, 101, 102	syl3anc 1250	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → DECID 𝑢 ∈ (1...(♯‘𝐵)))
104		exmiddc 838	. . . . . . . . . . 11 ⊢ (DECID 𝑢 ∈ (1...(♯‘𝐵)) → (𝑢 ∈ (1...(♯‘𝐵)) ∨ ¬ 𝑢 ∈ (1...(♯‘𝐵))))
105	103, 104	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → (𝑢 ∈ (1...(♯‘𝐵)) ∨ ¬ 𝑢 ∈ (1...(♯‘𝐵))))
106	86, 96, 105	mpjaodan 800	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → DECID 𝑢 ∈ (^◡𝑓 “ 𝐴))
107	106	ralrimiva 2580	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∀𝑢 ∈ (ℤ_≥‘1)DECID 𝑢 ∈ (^◡𝑓 “ 𝐴))
108		1zzd 9412	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 1 ∈ ℤ)
109		fzssuz 10200	. . . . . . . . 9 ⊢ (1...(♯‘𝐵)) ⊆ (ℤ_≥‘1)
110	109	a1i 9	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (1...(♯‘𝐵)) ⊆ (ℤ_≥‘1))
111	103	ralrimiva 2580	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∀𝑢 ∈ (ℤ_≥‘1)DECID 𝑢 ∈ (1...(♯‘𝐵)))
112	13, 43, 69, 107, 108, 110, 111	isumss 11752	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑛 ∈ (^◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) = Σ𝑛 ∈ (1...(♯‘𝐵))((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
113	1	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
114	113	resmptd 5016	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴) = (𝑘 ∈ 𝐴 ↦ 𝐶))
115	114	fveq1d 5588	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚))
116		fvres 5610	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝐴 → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
117	116	adantl 277	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
118	115, 117	eqtr3d 2241	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
119	118	sumeq2dv 11729	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
120		fveq2 5586	. . . . . . . . 9 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
121	1	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝐴 ⊆ 𝐵)
122		fsumss.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ Fin)
123		ssfidc 7046	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴) → 𝐴 ∈ Fin)
124	122, 1, 33, 123	syl3anc 1250	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ Fin)
125	124	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝐴 ∈ Fin)
126	121, 10, 125	preimaf1ofi 7065	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (^◡𝑓 “ 𝐴) ∈ Fin)
127		f1of1 5530	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))–1-1→𝐵)
128	10, 127	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1→𝐵)
129		f1ores 5546	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(♯‘𝐵))–1-1→𝐵 ∧ (^◡𝑓 “ 𝐴) ⊆ (1...(♯‘𝐵))) → (𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (^◡𝑓 “ 𝐴)))
130	128, 13, 129	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (^◡𝑓 “ 𝐴)))
131		f1ofo 5538	. . . . . . . . . . . . 13 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))–onto→𝐵)
132	10, 131	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–onto→𝐵)
133		foimacnv 5549	. . . . . . . . . . . 12 ⊢ ((𝑓:(1...(♯‘𝐵))–onto→𝐵 ∧ 𝐴 ⊆ 𝐵) → (𝑓 “ (^◡𝑓 “ 𝐴)) = 𝐴)
134	132, 121, 133	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑓 “ (^◡𝑓 “ 𝐴)) = 𝐴)
135		f1oeq3 5521	. . . . . . . . . . 11 ⊢ ((𝑓 “ (^◡𝑓 “ 𝐴)) = 𝐴 → ((𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (^◡𝑓 “ 𝐴)) ↔ (𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→𝐴))
136	134, 135	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ((𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (^◡𝑓 “ 𝐴)) ↔ (𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→𝐴))
137	130, 136	mpbid 147	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→𝐴)
138		fvres 5610	. . . . . . . . . 10 ⊢ (𝑛 ∈ (^◡𝑓 “ 𝐴) → ((𝑓 ↾ (^◡𝑓 “ 𝐴))‘𝑛) = (𝑓‘𝑛))
139	138	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (^◡𝑓 “ 𝐴)) → ((𝑓 ↾ (^◡𝑓 “ 𝐴))‘𝑛) = (𝑓‘𝑛))
140	121	sselda 3195	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐵)
141	41	ffvelcdmda 5725	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ)
142	140, 141	syldan 282	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ)
143	120, 126, 137, 139, 142	fsumf1o 11751	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑛 ∈ (^◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
144	119, 143	eqtrd 2239	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑛 ∈ (^◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
145		simprl 529	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (♯‘𝐵) ∈ ℕ)
146	145	nnzd 9507	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (♯‘𝐵) ∈ ℤ)
147	108, 146	fzfigd 10589	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (1...(♯‘𝐵)) ∈ Fin)
148		eqidd 2207	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓‘𝑛) = (𝑓‘𝑛))
149	120, 147, 10, 148, 141	fsumf1o 11751	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑛 ∈ (1...(♯‘𝐵))((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
150	112, 144, 149	3eqtr4d 2249	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
151	22	ralrimiva 2580	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ)
152		sumfct 11735	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶)
153	151, 152	syl 14	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶)
154	153	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐶)
155	22	adantlr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
156		simpll 527	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝜑)
157		simplr 528	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐵)
158		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐴)
159	157, 158	eldifd 3178	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝑘 ∈ (𝐵 ∖ 𝐴))
160	156, 159, 26	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝐶 = 0)
161		0cnd 8078	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 0 ∈ ℂ)
162	160, 161	eqeltrd 2283	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
163	155, 162, 38	mpjaodan 800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
164	163	ralrimiva 2580	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
165		sumfct 11735	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐵 𝐶)
166	164, 165	syl 14	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐵 𝐶)
167	166	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐵 𝐶)
168	150, 154, 167	3eqtr3d 2247	. . . . 5 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
169	168	expr 375	. . . 4 ⊢ ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶))
170	169	exlimdv 1843	. . 3 ⊢ ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶))
171	170	expimpd 363	. 2 ⊢ (𝜑 → (((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶))
172		fz1f1o 11736	. . 3 ⊢ (𝐵 ∈ Fin → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)))
173	122, 172	syl 14	. 2 ⊢ (𝜑 → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)))
174	8, 171, 173	mpjaod 720	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 DECID wdc 836 = wceq 1373 ∃wex 1516 ∈ wcel 2177 ∀wral 2485 ∖ cdif 3165 ⊆ wss 3168 ∅c0 3462 {csn 3635 ↦ cmpt 4110 ^◡ccnv 4679 dom cdm 4680 ↾ cres 4682 “ cima 4683 Fun wfun 5271 Fn wfn 5272 ⟶wf 5273 –1-1→wf1 5274 –onto→wfo 5275 –1-1-onto→wf1o 5276 ‘cfv 5277 (class class class)co 5954 Fincfn 6837 ℂcc 7936 0cc0 7938 1c1 7939 ℕcn 9049 ℤcz 9385 ℤ_≥cuz 9661 ...cfz 10143 ♯chash 10933 Σcsu 11714

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4164 ax-sep 4167 ax-nul 4175 ax-pow 4223 ax-pr 4258 ax-un 4485 ax-setind 4590 ax-iinf 4641 ax-cnex 8029 ax-resscn 8030 ax-1cn 8031 ax-1re 8032 ax-icn 8033 ax-addcl 8034 ax-addrcl 8035 ax-mulcl 8036 ax-mulrcl 8037 ax-addcom 8038 ax-mulcom 8039 ax-addass 8040 ax-mulass 8041 ax-distr 8042 ax-i2m1 8043 ax-0lt1 8044 ax-1rid 8045 ax-0id 8046 ax-rnegex 8047 ax-precex 8048 ax-cnre 8049 ax-pre-ltirr 8050 ax-pre-ltwlin 8051 ax-pre-lttrn 8052 ax-pre-apti 8053 ax-pre-ltadd 8054 ax-pre-mulgt0 8055 ax-pre-mulext 8056 ax-arch 8057 ax-caucvg 8058

This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3001 df-csb 3096 df-dif 3170 df-un 3172 df-in 3174 df-ss 3181 df-nul 3463 df-if 3574 df-pw 3620 df-sn 3641 df-pr 3642 df-op 3644 df-uni 3854 df-int 3889 df-iun 3932 df-br 4049 df-opab 4111 df-mpt 4112 df-tr 4148 df-id 4345 df-po 4348 df-iso 4349 df-iord 4418 df-on 4420 df-ilim 4421 df-suc 4423 df-iom 4644 df-xp 4686 df-rel 4687 df-cnv 4688 df-co 4689 df-dm 4690 df-rn 4691 df-res 4692 df-ima 4693 df-iota 5238 df-fun 5279 df-fn 5280 df-f 5281 df-f1 5282 df-fo 5283 df-f1o 5284 df-fv 5285 df-isom 5286 df-riota 5909 df-ov 5957 df-oprab 5958 df-mpo 5959 df-1st 6236 df-2nd 6237 df-recs 6401 df-irdg 6466 df-frec 6487 df-1o 6512 df-oadd 6516 df-er 6630 df-en 6838 df-dom 6839 df-fin 6840 df-pnf 8122 df-mnf 8123 df-xr 8124 df-ltxr 8125 df-le 8126 df-sub 8258 df-neg 8259 df-reap 8661 df-ap 8668 df-div 8759 df-inn 9050 df-2 9108 df-3 9109 df-4 9110 df-n0 9309 df-z 9386 df-uz 9662 df-q 9754 df-rp 9789 df-fz 10144 df-fzo 10278 df-seqfrec 10606 df-exp 10697 df-ihash 10934 df-cj 11203 df-re 11204 df-im 11205 df-rsqrt 11359 df-abs 11360 df-clim 11640 df-sumdc 11715

This theorem is referenced by: isumss2 11754 ply1termlem 15264 plyaddlem1 15269 plymullem1 15270 plycoeid3 15279 dvply1 15287

W3C validator