fisumss - Intuitionistic Logic Explorer

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

Theorem fisumss 12103

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 3554	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 = ∅) → 𝐴 = ∅)
3	1, 2	sylan 283	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ∅) → 𝐴 = ∅)
4	3	sumeq1d 12076	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ∅) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
5		simpr 110	. . . . 5 ⊢ ((𝜑 ∧ 𝐵 = ∅) → 𝐵 = ∅)
6	5	sumeq1d 12076	. . . 4 ⊢ ((𝜑 ∧ 𝐵 = ∅) → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ ∅ 𝐶)
7	4, 6	eqtr4d 2270	. . 3 ⊢ ((𝜑 ∧ 𝐵 = ∅) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
8	7	ex 115	. 2 ⊢ (𝜑 → (𝐵 = ∅ → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶))
9		cnvimass 5130	. . . . . . . . 9 ⊢ (^◡𝑓 “ 𝐴) ⊆ dom 𝑓
10		simprr 533	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)
11		f1of 5619	. . . . . . . . . 10 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))⟶𝐵)
12	10, 11	syl 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))⟶𝐵)
13	9, 12	fssdm 5529	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (^◡𝑓 “ 𝐴) ⊆ (1...(♯‘𝐵)))
14	12	ffnd 5514	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓 Fn (1...(♯‘𝐵)))
15		elpreima 5802	. . . . . . . . . . . 12 ⊢ (𝑓 Fn (1...(♯‘𝐵)) → (𝑛 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴)))
16	14, 15	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑛 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑛 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐴)))
17	12	ffvelcdmda 5817	. . . . . . . . . . . . 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 3223	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ (𝐵 ∖ 𝐴) ↔ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴))
26		fsumss.3	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 = 0)
27		0cn 8282	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℂ
28	26, 27	eqeltrdi 2325	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ ℂ)
29	25, 28	sylan2br 288	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐵 ∧ ¬ 𝑘 ∈ 𝐴)) → 𝐶 ∈ ℂ)
30	29	expr 375	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (¬ 𝑘 ∈ 𝐴 → 𝐶 ∈ ℂ))
31		eleq1w 2295	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
32	31	dcbid 846	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝑘 → (DECID 𝑗 ∈ 𝐴 ↔ DECID 𝑘 ∈ 𝐴))
33		fisumss.adc	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)
34	33	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴)
35		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
36	32, 34, 35	rspcdva 2928	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → DECID 𝑘 ∈ 𝐴)
37		exmiddc 844	. . . . . . . . . . . . . 14 ⊢ (DECID 𝑘 ∈ 𝐴 → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
38	36, 37	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑘 ∈ 𝐴 ∨ ¬ 𝑘 ∈ 𝐴))
39	24, 30, 38	mpjaod 726	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
40	39	fmpttd 5837	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ)
41	40	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑘 ∈ 𝐵 ↦ 𝐶):𝐵⟶ℂ)
42	41	ffvelcdmda 5817	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ (𝑓‘𝑛) ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) ∈ ℂ)
43	21, 42	syldan 282	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (^◡𝑓 “ 𝐴)) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) ∈ ℂ)
44		eldifi 3345	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴)) → 𝑛 ∈ (1...(♯‘𝐵)))
45	44, 17	sylan2 286	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → (𝑓‘𝑛) ∈ 𝐵)
46		eldifn 3346	. . . . . . . . . . . . 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 679	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ¬ (𝑓‘𝑛) ∈ 𝐴)
53	45, 52	eldifd 3224	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → (𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴))
54		difss 3349	. . . . . . . . . . . . 13 ⊢ (𝐵 ∖ 𝐴) ⊆ 𝐵
55		resmpt 5091	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∖ 𝐴) ⊆ 𝐵 → ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴)) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶))
56	54, 55	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴)) = (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)
57	56	fveq1i 5676	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴))‘(𝑓‘𝑛)) = ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛))
58		fvres 5699	. . . . . . . . . . 11 ⊢ ((𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ (𝐵 ∖ 𝐴))‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
59	57, 58	eqtr3id 2281	. . . . . . . . . 10 ⊢ ((𝑓‘𝑛) ∈ (𝐵 ∖ 𝐴) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
60	53, 59	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
61		c0ex 8284	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
62	61	elsn2 3728	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ {0} ↔ 𝐶 = 0)
63	26, 62	sylibr 134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ 𝐴)) → 𝐶 ∈ {0})
64	63	fmpttd 5837	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶):(𝐵 ∖ 𝐴)⟶{0})
65	64	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → (𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶):(𝐵 ∖ 𝐴)⟶{0})
66	65, 53	ffvelcdmd 5818	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) ∈ {0})
67		elsni 3712	. . . . . . . . . 10 ⊢ (((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) ∈ {0} → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = 0)
68	66, 67	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑘 ∈ (𝐵 ∖ 𝐴) ↦ 𝐶)‘(𝑓‘𝑛)) = 0)
69	60, 68	eqtr3d 2269	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ ((1...(♯‘𝐵)) ∖ (^◡𝑓 “ 𝐴))) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) = 0)
70		eleq1 2297	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑓‘𝑢) → (𝑗 ∈ 𝐴 ↔ (𝑓‘𝑢) ∈ 𝐴))
71	70	dcbid 846	. . . . . . . . . . . 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 5818	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → (𝑓‘𝑢) ∈ 𝐵)
76	71, 72, 75	rspcdva 2928	. . . . . . . . . . 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 5621	. . . . . . . . . . . . . 14 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → Fun 𝑓)
79	77, 78	syl 14	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → Fun 𝑓)
80		f1odm 5623	. . . . . . . . . . . . . . 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 2314	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → 𝑢 ∈ dom 𝑓)
83		fvimacnv 5798	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑓 ∧ 𝑢 ∈ dom 𝑓) → ((𝑓‘𝑢) ∈ 𝐴 ↔ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
84	79, 82, 83	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → ((𝑓‘𝑢) ∈ 𝐴 ↔ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
85	84	dcbid 846	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → (DECID (𝑓‘𝑢) ∈ 𝐴 ↔ DECID 𝑢 ∈ (^◡𝑓 “ 𝐴)))
86	76, 85	mpbid 147	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ 𝑢 ∈ (1...(♯‘𝐵))) → DECID 𝑢 ∈ (^◡𝑓 “ 𝐴))
87		elpreima 5802	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 Fn (1...(♯‘𝐵)) → (𝑢 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑢 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑢) ∈ 𝐴)))
88		simpl 109	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑢 ∈ (1...(♯‘𝐵)) ∧ (𝑓‘𝑢) ∈ 𝐴) → 𝑢 ∈ (1...(♯‘𝐵)))
89	87, 88	biimtrdi 163	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 Fn (1...(♯‘𝐵)) → (𝑢 ∈ (^◡𝑓 “ 𝐴) → 𝑢 ∈ (1...(♯‘𝐵))))
90	89	con3d 636	. . . . . . . . . . . . . . 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 742	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑢 ∈ (1...(♯‘𝐵))) → (𝑢 ∈ (^◡𝑓 “ 𝐴) ∨ ¬ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
95		df-dc 843	. . . . . . . . . . 11 ⊢ (DECID 𝑢 ∈ (^◡𝑓 “ 𝐴) ↔ (𝑢 ∈ (^◡𝑓 “ 𝐴) ∨ ¬ 𝑢 ∈ (^◡𝑓 “ 𝐴)))
96	94, 95	sylibr 134	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) ∧ ¬ 𝑢 ∈ (1...(♯‘𝐵))) → DECID 𝑢 ∈ (^◡𝑓 “ 𝐴))
97		eluzelz 9881	. . . . . . . . . . . . 13 ⊢ (𝑢 ∈ (ℤ_≥‘1) → 𝑢 ∈ ℤ)
98	97	adantl 277	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → 𝑢 ∈ ℤ)
99		1zzd 9621	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → 1 ∈ ℤ)
100		simplrl 537	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → (♯‘𝐵) ∈ ℕ)
101	100	nnzd 9717	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → (♯‘𝐵) ∈ ℤ)
102		fzdcel 10394	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ ℤ ∧ 1 ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → DECID 𝑢 ∈ (1...(♯‘𝐵)))
103	98, 99, 101, 102	syl3anc 1274	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → DECID 𝑢 ∈ (1...(♯‘𝐵)))
104		exmiddc 844	. . . . . . . . . . 11 ⊢ (DECID 𝑢 ∈ (1...(♯‘𝐵)) → (𝑢 ∈ (1...(♯‘𝐵)) ∨ ¬ 𝑢 ∈ (1...(♯‘𝐵))))
105	103, 104	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → (𝑢 ∈ (1...(♯‘𝐵)) ∨ ¬ 𝑢 ∈ (1...(♯‘𝐵))))
106	86, 96, 105	mpjaodan 806	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑢 ∈ (ℤ_≥‘1)) → DECID 𝑢 ∈ (^◡𝑓 “ 𝐴))
107	106	ralrimiva 2617	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∀𝑢 ∈ (ℤ_≥‘1)DECID 𝑢 ∈ (^◡𝑓 “ 𝐴))
108		1zzd 9621	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 1 ∈ ℤ)
109		fzssuz 10420	. . . . . . . . 9 ⊢ (1...(♯‘𝐵)) ⊆ (ℤ_≥‘1)
110	109	a1i 9	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (1...(♯‘𝐵)) ⊆ (ℤ_≥‘1))
111	103	ralrimiva 2617	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → ∀𝑢 ∈ (ℤ_≥‘1)DECID 𝑢 ∈ (1...(♯‘𝐵)))
112	13, 43, 69, 107, 108, 110, 111	isumss 12102	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑛 ∈ (^◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)) = Σ𝑛 ∈ (1...(♯‘𝐵))((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
113	1	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → 𝐴 ⊆ 𝐵)
114	113	resmptd 5094	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴) = (𝑘 ∈ 𝐴 ↦ 𝐶))
115	114	fveq1d 5677	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚))
116		fvres 5699	. . . . . . . . . . 11 ⊢ (𝑚 ∈ 𝐴 → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
117	116	adantl 277	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → (((𝑘 ∈ 𝐵 ↦ 𝐶) ↾ 𝐴)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
118	115, 117	eqtr3d 2269	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
119	118	sumeq2dv 12078	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
120		fveq2 5675	. . . . . . . . 9 ⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = ((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
121	1	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝐴 ⊆ 𝐵)
122		fsumss.4	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ Fin)
123		ssfidc 7211	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵 ∧ ∀𝑗 ∈ 𝐵 DECID 𝑗 ∈ 𝐴) → 𝐴 ∈ Fin)
124	122, 1, 33, 123	syl3anc 1274	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ Fin)
125	124	adantr 276	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝐴 ∈ Fin)
126	121, 10, 125	preimaf1ofi 7234	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (^◡𝑓 “ 𝐴) ∈ Fin)
127		f1of1 5618	. . . . . . . . . . . 12 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))–1-1→𝐵)
128	10, 127	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–1-1→𝐵)
129		f1ores 5634	. . . . . . . . . . 11 ⊢ ((𝑓:(1...(♯‘𝐵))–1-1→𝐵 ∧ (^◡𝑓 “ 𝐴) ⊆ (1...(♯‘𝐵))) → (𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (^◡𝑓 “ 𝐴)))
130	128, 13, 129	syl2anc 411	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑓 ↾ (^◡𝑓 “ 𝐴)):(^◡𝑓 “ 𝐴)–1-1-onto→(𝑓 “ (^◡𝑓 “ 𝐴)))
131		f1ofo 5626	. . . . . . . . . . . . 13 ⊢ (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → 𝑓:(1...(♯‘𝐵))–onto→𝐵)
132	10, 131	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → 𝑓:(1...(♯‘𝐵))–onto→𝐵)
133		foimacnv 5637	. . . . . . . . . . . 12 ⊢ ((𝑓:(1...(♯‘𝐵))–onto→𝐵 ∧ 𝐴 ⊆ 𝐵) → (𝑓 “ (^◡𝑓 “ 𝐴)) = 𝐴)
134	132, 121, 133	syl2anc 411	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (𝑓 “ (^◡𝑓 “ 𝐴)) = 𝐴)
135		f1oeq3 5609	. . . . . . . . . . 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 5699	. . . . . . . . . 10 ⊢ (𝑛 ∈ (^◡𝑓 “ 𝐴) → ((𝑓 ↾ (^◡𝑓 “ 𝐴))‘𝑛) = (𝑓‘𝑛))
139	138	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (^◡𝑓 “ 𝐴)) → ((𝑓 ↾ (^◡𝑓 “ 𝐴))‘𝑛) = (𝑓‘𝑛))
140	121	sselda 3242	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → 𝑚 ∈ 𝐵)
141	41	ffvelcdmda 5817	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐵) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ)
142	140, 141	syldan 282	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) ∈ ℂ)
143	120, 126, 137, 139, 142	fsumf1o 12101	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑛 ∈ (^◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
144	119, 143	eqtrd 2267	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑛 ∈ (^◡𝑓 “ 𝐴)((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
145		simprl 531	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (♯‘𝐵) ∈ ℕ)
146	145	nnzd 9717	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (♯‘𝐵) ∈ ℤ)
147	108, 146	fzfigd 10817	. . . . . . . 8 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → (1...(♯‘𝐵)) ∈ Fin)
148		eqidd 2235	. . . . . . . 8 ⊢ (((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) ∧ 𝑛 ∈ (1...(♯‘𝐵))) → (𝑓‘𝑛) = (𝑓‘𝑛))
149	120, 147, 10, 148, 141	fsumf1o 12101	. . . . . . 7 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑛 ∈ (1...(♯‘𝐵))((𝑘 ∈ 𝐵 ↦ 𝐶)‘(𝑓‘𝑛)))
150	112, 144, 149	3eqtr4d 2277	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐶)‘𝑚) = Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚))
151	22	ralrimiva 2617	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐶 ∈ ℂ)
152		sumfct 12084	. . . . . . . 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 529	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐵)
158		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ 𝐴)
159	157, 158	eldifd 3224	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝑘 ∈ (𝐵 ∖ 𝐴))
160	156, 159, 26	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝐶 = 0)
161		0cnd 8283	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 0 ∈ ℂ)
162	160, 161	eqeltrd 2311	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ ¬ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)
163	155, 162, 38	mpjaodan 806	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
164	163	ralrimiva 2617	. . . . . . . 8 ⊢ (𝜑 → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ)
165		sumfct 12084	. . . . . . . 8 ⊢ (∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐵 𝐶)
166	164, 165	syl 14	. . . . . . 7 ⊢ (𝜑 → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐵 𝐶)
167	166	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑚 ∈ 𝐵 ((𝑘 ∈ 𝐵 ↦ 𝐶)‘𝑚) = Σ𝑘 ∈ 𝐵 𝐶)
168	150, 154, 167	3eqtr3d 2275	. . . . 5 ⊢ ((𝜑 ∧ ((♯‘𝐵) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)
169	168	expr 375	. . . 4 ⊢ ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶))
170	169	exlimdv 1868	. . 3 ⊢ ((𝜑 ∧ (♯‘𝐵) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶))
171	170	expimpd 363	. 2 ⊢ (𝜑 → (((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵) → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶))
172		fz1f1o 12085	. . 3 ⊢ (𝐵 ∈ Fin → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)))
173	122, 172	syl 14	. 2 ⊢ (𝜑 → (𝐵 = ∅ ∨ ((♯‘𝐵) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐵))–1-1-onto→𝐵)))
174	8, 171, 173	mpjaod 726	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐶 = Σ𝑘 ∈ 𝐵 𝐶)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 716 DECID wdc 842 = wceq 1398 ∃wex 1541 ∈ wcel 2205 ∀wral 2522 ∖ cdif 3211 ⊆ wss 3214 ∅c0 3512 {csn 3694 ↦ cmpt 4176 ^◡ccnv 4753 dom cdm 4754 ↾ cres 4756 “ cima 4757 Fun wfun 5351 Fn wfn 5352 ⟶wf 5353 –1-1→wf1 5354 –onto→wfo 5355 –1-1-onto→wf1o 5356 ‘cfv 5357 (class class class)co 6058 Fincfn 6988 ℂcc 8141 0cc0 8143 1c1 8144 ℕcn 9254 ℤcz 9594 ℤ_≥cuz 9871 ...cfz 10361 ♯chash 11163 Σcsu 12063

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-coll 4230 ax-sep 4233 ax-nul 4241 ax-pow 4292 ax-pr 4327 ax-un 4559 ax-setind 4664 ax-iinf 4715 ax-cnex 8234 ax-resscn 8235 ax-1cn 8236 ax-1re 8237 ax-icn 8238 ax-addcl 8239 ax-addrcl 8240 ax-mulcl 8241 ax-mulrcl 8242 ax-addcom 8243 ax-mulcom 8244 ax-addass 8245 ax-mulass 8246 ax-distr 8247 ax-i2m1 8248 ax-0lt1 8249 ax-1rid 8250 ax-0id 8251 ax-rnegex 8252 ax-precex 8253 ax-cnre 8254 ax-pre-ltirr 8255 ax-pre-ltwlin 8256 ax-pre-lttrn 8257 ax-pre-apti 8258 ax-pre-ltadd 8259 ax-pre-mulgt0 8260 ax-pre-mulext 8261 ax-arch 8262 ax-caucvg 8263

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ne 2415 df-nel 2510 df-ral 2527 df-rex 2528 df-reu 2529 df-rmo 2530 df-rab 2531 df-v 2817 df-sbc 3046 df-csb 3142 df-dif 3216 df-un 3218 df-in 3220 df-ss 3227 df-nul 3513 df-if 3625 df-pw 3676 df-sn 3700 df-pr 3701 df-op 3703 df-uni 3920 df-int 3955 df-iun 3998 df-br 4115 df-opab 4177 df-mpt 4178 df-tr 4214 df-id 4419 df-po 4422 df-iso 4423 df-iord 4492 df-on 4494 df-ilim 4495 df-suc 4497 df-iom 4718 df-xp 4760 df-rel 4761 df-cnv 4762 df-co 4763 df-dm 4764 df-rn 4765 df-res 4766 df-ima 4767 df-iota 5317 df-fun 5359 df-fn 5360 df-f 5361 df-f1 5362 df-fo 5363 df-f1o 5364 df-fv 5365 df-isom 5366 df-riota 6011 df-ov 6061 df-oprab 6062 df-mpo 6063 df-1st 6347 df-2nd 6348 df-recs 6549 df-irdg 6614 df-frec 6635 df-1o 6660 df-oadd 6664 df-er 6780 df-en 6989 df-dom 6990 df-fin 6991 df-pnf 8326 df-mnf 8327 df-xr 8328 df-ltxr 8329 df-le 8330 df-sub 8462 df-neg 8463 df-reap 8866 df-ap 8873 df-div 8964 df-inn 9255 df-2 9313 df-3 9314 df-4 9315 df-n0 9514 df-z 9595 df-uz 9872 df-q 9970 df-rp 10005 df-fz 10362 df-fzo 10499 df-seqfrec 10834 df-exp 10925 df-ihash 11164 df-cj 11552 df-re 11553 df-im 11554 df-rsqrt 11708 df-abs 11709 df-clim 11989 df-sumdc 12064

This theorem is referenced by: isumss2 12104 ply1termlem 15719 plyaddlem1 15724 plymullem1 15725 plycoeid3 15734 dvply1 15742

W3C validator