Theorem esumc

Description: Convert from the collection form to the class-variable form of a sum. (Contributed by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypotheses	esumc.0	⊢ Ⅎ 𝑘 𝐷
	esumc.1	⊢ Ⅎ 𝑘 𝜑
	esumc.2	⊢ Ⅎ 𝑘 𝐴
	esumc.3	⊢ ( 𝑦 = 𝐶 → 𝐷 = 𝐵 )
	esumc.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	esumc.5	⊢ ( 𝜑 → Fun ◡ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
	esumc.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	esumc.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 )
Assertion	esumc	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ* 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		esumc.0	⊢ Ⅎ 𝑘 𝐷
2		esumc.1	⊢ Ⅎ 𝑘 𝜑
3		esumc.2	⊢ Ⅎ 𝑘 𝐴
4		esumc.3	⊢ ( 𝑦 = 𝐶 → 𝐷 = 𝐵 )
5		esumc.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		esumc.5	⊢ ( 𝜑 → Fun ◡ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) )
7		esumc.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
8		esumc.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 )
9		nfcv	⊢ Ⅎ 𝑦 𝐵
10		nfre1	⊢ Ⅎ 𝑘 ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶
11	10	nfab	⊢ Ⅎ 𝑘 { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 }
12		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
13		elex	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
14	5 13	syl	⊢ ( 𝜑 → 𝐴 ∈ V )
15	3 14	abrexexd	⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } ∈ V )
16	8	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → 𝐶 ∈ 𝑊 ) )
17	2 16	ralrimi	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐶 ∈ 𝑊 )
18	3	fnmptf	⊢ ( ∀ 𝑘 ∈ 𝐴 𝐶 ∈ 𝑊 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
19	17 18	syl	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
20		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐶 )
21	20	rnmpt	⊢ ran ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 }
22	21	a1i	⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } )
23		dff1o2	⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1-onto→ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } ↔ ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ∧ Fun ◡ ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ∧ ran ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) = { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } ) )
24	19 6 22 23	syl3anbrc	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) : 𝐴 –1-1-onto→ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
26	3	fvmpt2f	⊢ ( ( 𝑘 ∈ 𝐴 ∧ 𝐶 ∈ 𝑊 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
27	25 8 26	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑘 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑘 ) = 𝐶 )
28		vex	⊢ 𝑦 ∈ V
29		eqeq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 = 𝐶 ↔ 𝑦 = 𝐶 ) )
30	29	rexbidv	⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 ↔ ∃ 𝑘 ∈ 𝐴 𝑦 = 𝐶 ) )
31	28 30	elab	⊢ ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } ↔ ∃ 𝑘 ∈ 𝐴 𝑦 = 𝐶 )
32	4	reximi	⊢ ( ∃ 𝑘 ∈ 𝐴 𝑦 = 𝐶 → ∃ 𝑘 ∈ 𝐴 𝐷 = 𝐵 )
33	31 32	sylbi	⊢ ( 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } → ∃ 𝑘 ∈ 𝐴 𝐷 = 𝐵 )
34		nfcv	⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
35	1 34	nfel	⊢ Ⅎ 𝑘 𝐷 ∈ ( 0 [,] +∞ )
36		eleq1	⊢ ( 𝐷 = 𝐵 → ( 𝐷 ∈ ( 0 [,] +∞ ) ↔ 𝐵 ∈ ( 0 [,] +∞ ) ) )
37	7 36	syl5ibrcom	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐷 = 𝐵 → 𝐷 ∈ ( 0 [,] +∞ ) ) )
38	37	ex	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 → ( 𝐷 = 𝐵 → 𝐷 ∈ ( 0 [,] +∞ ) ) ) )
39	2 35 38	rexlimd	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ 𝐴 𝐷 = 𝐵 → 𝐷 ∈ ( 0 [,] +∞ ) ) )
40	39	imp	⊢ ( ( 𝜑 ∧ ∃ 𝑘 ∈ 𝐴 𝐷 = 𝐵 ) → 𝐷 ∈ ( 0 [,] +∞ ) )
41	33 40	sylan2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } ) → 𝐷 ∈ ( 0 [,] +∞ ) )
42	2 1 9 11 3 12 4 15 24 27 41	esumf1o	⊢ ( 𝜑 → Σ* 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } 𝐷 = Σ* 𝑘 ∈ 𝐴 𝐵 )
43	42	eqcomd	⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐵 = Σ* 𝑦 ∈ { 𝑧 ∣ ∃ 𝑘 ∈ 𝐴 𝑧 = 𝐶 } 𝐷 )