fsumcnv

Description: Transform a region of summation by using the converse operation. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	fsumcnv.1	⊢ ( 𝑥 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐵 = 𝐷 )
	fsumcnv.2	⊢ ( 𝑦 = ⟨ 𝑘 , 𝑗 ⟩ → 𝐶 = 𝐷 )
	fsumcnv.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumcnv.4	⊢ ( 𝜑 → Rel 𝐴 )
	fsumcnv.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion	fsumcnv	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 𝐵 = Σ 𝑦 ∈ ^◡ 𝐴 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fsumcnv.1	⊢ ( 𝑥 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐵 = 𝐷 )
2		fsumcnv.2	⊢ ( 𝑦 = ⟨ 𝑘 , 𝑗 ⟩ → 𝐶 = 𝐷 )
3		fsumcnv.3	⊢ ( 𝜑 → 𝐴 ∈ Fin )
4		fsumcnv.4	⊢ ( 𝜑 → Rel 𝐴 )
5		fsumcnv.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
6		csbeq1a	⊢ ( 𝑥 = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ → 𝐵 = ⦋ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ / 𝑥 ⦌ 𝐵 )
7		fvex	⊢ ( 2^nd ‘ 𝑦 ) ∈ V
8		fvex	⊢ ( 1^st ‘ 𝑦 ) ∈ V
9		opex	⊢ ⟨ 𝑗 , 𝑘 ⟩ ∈ V
10	9 1	csbie	⊢ ⦋ ⟨ 𝑗 , 𝑘 ⟩ / 𝑥 ⦌ 𝐵 = 𝐷
11		opeq12	⊢ ( ( 𝑗 = ( 2^nd ‘ 𝑦 ) ∧ 𝑘 = ( 1^st ‘ 𝑦 ) ) → ⟨ 𝑗 , 𝑘 ⟩ = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
12	11	csbeq1d	⊢ ( ( 𝑗 = ( 2^nd ‘ 𝑦 ) ∧ 𝑘 = ( 1^st ‘ 𝑦 ) ) → ⦋ ⟨ 𝑗 , 𝑘 ⟩ / 𝑥 ⦌ 𝐵 = ⦋ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ / 𝑥 ⦌ 𝐵 )
13	10 12	eqtr3id	⊢ ( ( 𝑗 = ( 2^nd ‘ 𝑦 ) ∧ 𝑘 = ( 1^st ‘ 𝑦 ) ) → 𝐷 = ⦋ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ / 𝑥 ⦌ 𝐵 )
14	7 8 13	csbie2	⊢ ⦋ ( 2^nd ‘ 𝑦 ) / 𝑗 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑘 ⦌ 𝐷 = ⦋ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ / 𝑥 ⦌ 𝐵
15	6 14	eqtr4di	⊢ ( 𝑥 = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ → 𝐵 = ⦋ ( 2^nd ‘ 𝑦 ) / 𝑗 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑘 ⦌ 𝐷 )
16		cnvfi	⊢ ( 𝐴 ∈ Fin → ^◡ 𝐴 ∈ Fin )
17	3 16	syl	⊢ ( 𝜑 → ^◡ 𝐴 ∈ Fin )
18		relcnv	⊢ Rel ^◡ 𝐴
19		cnvf1o	⊢ ( Rel ^◡ 𝐴 → ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) : ^◡ 𝐴 –1-1-onto→ ^◡ ^◡ 𝐴 )
20	18 19	ax-mp	⊢ ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) : ^◡ 𝐴 –1-1-onto→ ^◡ ^◡ 𝐴
21		dfrel2	⊢ ( Rel 𝐴 ↔ ^◡ ^◡ 𝐴 = 𝐴 )
22	4 21	sylib	⊢ ( 𝜑 → ^◡ ^◡ 𝐴 = 𝐴 )
23	22	f1oeq3d	⊢ ( 𝜑 → ( ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) : ^◡ 𝐴 –1-1-onto→ ^◡ ^◡ 𝐴 ↔ ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) : ^◡ 𝐴 –1-1-onto→ 𝐴 ) )
24	20 23	mpbii	⊢ ( 𝜑 → ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) : ^◡ 𝐴 –1-1-onto→ 𝐴 )
25		1st2nd	⊢ ( ( Rel ^◡ 𝐴 ∧ 𝑦 ∈ ^◡ 𝐴 ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
26	18 25	mpan	⊢ ( 𝑦 ∈ ^◡ 𝐴 → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
27	26	fveq2d	⊢ ( 𝑦 ∈ ^◡ 𝐴 → ( ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) ‘ 𝑦 ) = ( ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) )
28		id	⊢ ( 𝑦 ∈ ^◡ 𝐴 → 𝑦 ∈ ^◡ 𝐴 )
29	26 28	eqeltrrd	⊢ ( 𝑦 ∈ ^◡ 𝐴 → ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ ^◡ 𝐴 )
30		sneq	⊢ ( 𝑧 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ → { 𝑧 } = { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } )
31	30	cnveqd	⊢ ( 𝑧 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ → ^◡ { 𝑧 } = ^◡ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } )
32	31	unieqd	⊢ ( 𝑧 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ → ∪ ^◡ { 𝑧 } = ∪ ^◡ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } )
33		opswap	⊢ ∪ ^◡ { ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ } = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩
34	32 33	eqtrdi	⊢ ( 𝑧 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ → ∪ ^◡ { 𝑧 } = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
35		eqid	⊢ ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) = ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } )
36		opex	⊢ ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ ∈ V
37	34 35 36	fvmpt	⊢ ( ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ ^◡ 𝐴 → ( ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
38	29 37	syl	⊢ ( 𝑦 ∈ ^◡ 𝐴 → ( ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) ‘ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ) = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
39	27 38	eqtrd	⊢ ( 𝑦 ∈ ^◡ 𝐴 → ( ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) ‘ 𝑦 ) = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
40	39	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ^◡ 𝐴 ) → ( ( 𝑧 ∈ ^◡ 𝐴 ↦ ∪ ^◡ { 𝑧 } ) ‘ 𝑦 ) = ⟨ ( 2^nd ‘ 𝑦 ) , ( 1^st ‘ 𝑦 ) ⟩ )
41	15 17 24 40 5	fsumf1o	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 𝐵 = Σ 𝑦 ∈ ^◡ 𝐴 ⦋ ( 2^nd ‘ 𝑦 ) / 𝑗 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑘 ⦌ 𝐷 )
42		csbeq1a	⊢ ( 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ → 𝐶 = ⦋ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ / 𝑦 ⦌ 𝐶 )
43	26 42	syl	⊢ ( 𝑦 ∈ ^◡ 𝐴 → 𝐶 = ⦋ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ / 𝑦 ⦌ 𝐶 )
44		opex	⊢ ⟨ 𝑘 , 𝑗 ⟩ ∈ V
45	44 2	csbie	⊢ ⦋ ⟨ 𝑘 , 𝑗 ⟩ / 𝑦 ⦌ 𝐶 = 𝐷
46		opeq12	⊢ ( ( 𝑘 = ( 1^st ‘ 𝑦 ) ∧ 𝑗 = ( 2^nd ‘ 𝑦 ) ) → ⟨ 𝑘 , 𝑗 ⟩ = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
47	46	ancoms	⊢ ( ( 𝑗 = ( 2^nd ‘ 𝑦 ) ∧ 𝑘 = ( 1^st ‘ 𝑦 ) ) → ⟨ 𝑘 , 𝑗 ⟩ = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
48	47	csbeq1d	⊢ ( ( 𝑗 = ( 2^nd ‘ 𝑦 ) ∧ 𝑘 = ( 1^st ‘ 𝑦 ) ) → ⦋ ⟨ 𝑘 , 𝑗 ⟩ / 𝑦 ⦌ 𝐶 = ⦋ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ / 𝑦 ⦌ 𝐶 )
49	45 48	eqtr3id	⊢ ( ( 𝑗 = ( 2^nd ‘ 𝑦 ) ∧ 𝑘 = ( 1^st ‘ 𝑦 ) ) → 𝐷 = ⦋ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ / 𝑦 ⦌ 𝐶 )
50	7 8 49	csbie2	⊢ ⦋ ( 2^nd ‘ 𝑦 ) / 𝑗 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑘 ⦌ 𝐷 = ⦋ ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ / 𝑦 ⦌ 𝐶
51	43 50	eqtr4di	⊢ ( 𝑦 ∈ ^◡ 𝐴 → 𝐶 = ⦋ ( 2^nd ‘ 𝑦 ) / 𝑗 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑘 ⦌ 𝐷 )
52	51	sumeq2i	⊢ Σ 𝑦 ∈ ^◡ 𝐴 𝐶 = Σ 𝑦 ∈ ^◡ 𝐴 ⦋ ( 2^nd ‘ 𝑦 ) / 𝑗 ⦌ ⦋ ( 1^st ‘ 𝑦 ) / 𝑘 ⦌ 𝐷
53	41 52	eqtr4di	⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 𝐵 = Σ 𝑦 ∈ ^◡ 𝐴 𝐶 )

Metamath Proof Explorer

Theorem fsumcnv

Proof