Metamath Proof Explorer


Theorem 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 ( 𝑥 = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ → 𝐵 = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ / 𝑥 𝐵 )
7 fvex ( 2nd𝑦 ) ∈ V
8 fvex ( 1st𝑦 ) ∈ V
9 opex 𝑗 , 𝑘 ⟩ ∈ V
10 9 1 csbie 𝑗 , 𝑘 ⟩ / 𝑥 𝐵 = 𝐷
11 opeq12 ( ( 𝑗 = ( 2nd𝑦 ) ∧ 𝑘 = ( 1st𝑦 ) ) → ⟨ 𝑗 , 𝑘 ⟩ = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ )
12 11 csbeq1d ( ( 𝑗 = ( 2nd𝑦 ) ∧ 𝑘 = ( 1st𝑦 ) ) → 𝑗 , 𝑘 ⟩ / 𝑥 𝐵 = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ / 𝑥 𝐵 )
13 10 12 eqtr3id ( ( 𝑗 = ( 2nd𝑦 ) ∧ 𝑘 = ( 1st𝑦 ) ) → 𝐷 = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ / 𝑥 𝐵 )
14 7 8 13 csbie2 ( 2nd𝑦 ) / 𝑗 ( 1st𝑦 ) / 𝑘 𝐷 = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ / 𝑥 𝐵
15 6 14 eqtr4di ( 𝑥 = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ → 𝐵 = ( 2nd𝑦 ) / 𝑗 ( 1st𝑦 ) / 𝑘 𝐷 )
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 𝐴𝑦 𝐴 ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
26 18 25 mpan ( 𝑦 𝐴𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
27 26 fveq2d ( 𝑦 𝐴 → ( ( 𝑧 𝐴 { 𝑧 } ) ‘ 𝑦 ) = ( ( 𝑧 𝐴 { 𝑧 } ) ‘ ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ) )
28 id ( 𝑦 𝐴𝑦 𝐴 )
29 26 28 eqeltrrd ( 𝑦 𝐴 → ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ∈ 𝐴 )
30 sneq ( 𝑧 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ → { 𝑧 } = { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } )
31 30 cnveqd ( 𝑧 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ → { 𝑧 } = { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } )
32 31 unieqd ( 𝑧 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ → { 𝑧 } = { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } )
33 opswap { ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ } = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩
34 32 33 eqtrdi ( 𝑧 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ → { 𝑧 } = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ )
35 eqid ( 𝑧 𝐴 { 𝑧 } ) = ( 𝑧 𝐴 { 𝑧 } )
36 opex ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ ∈ V
37 34 35 36 fvmpt ( ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ∈ 𝐴 → ( ( 𝑧 𝐴 { 𝑧 } ) ‘ ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ) = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ )
38 29 37 syl ( 𝑦 𝐴 → ( ( 𝑧 𝐴 { 𝑧 } ) ‘ ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ) = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ )
39 27 38 eqtrd ( 𝑦 𝐴 → ( ( 𝑧 𝐴 { 𝑧 } ) ‘ 𝑦 ) = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ )
40 39 adantl ( ( 𝜑𝑦 𝐴 ) → ( ( 𝑧 𝐴 { 𝑧 } ) ‘ 𝑦 ) = ⟨ ( 2nd𝑦 ) , ( 1st𝑦 ) ⟩ )
41 15 17 24 40 5 fsumf1o ( 𝜑 → Σ 𝑥𝐴 𝐵 = Σ 𝑦 𝐴 ( 2nd𝑦 ) / 𝑗 ( 1st𝑦 ) / 𝑘 𝐷 )
42 csbeq1a ( 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ → 𝐶 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ / 𝑦 𝐶 )
43 26 42 syl ( 𝑦 𝐴𝐶 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ / 𝑦 𝐶 )
44 opex 𝑘 , 𝑗 ⟩ ∈ V
45 44 2 csbie 𝑘 , 𝑗 ⟩ / 𝑦 𝐶 = 𝐷
46 opeq12 ( ( 𝑘 = ( 1st𝑦 ) ∧ 𝑗 = ( 2nd𝑦 ) ) → ⟨ 𝑘 , 𝑗 ⟩ = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
47 46 ancoms ( ( 𝑗 = ( 2nd𝑦 ) ∧ 𝑘 = ( 1st𝑦 ) ) → ⟨ 𝑘 , 𝑗 ⟩ = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
48 47 csbeq1d ( ( 𝑗 = ( 2nd𝑦 ) ∧ 𝑘 = ( 1st𝑦 ) ) → 𝑘 , 𝑗 ⟩ / 𝑦 𝐶 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ / 𝑦 𝐶 )
49 45 48 eqtr3id ( ( 𝑗 = ( 2nd𝑦 ) ∧ 𝑘 = ( 1st𝑦 ) ) → 𝐷 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ / 𝑦 𝐶 )
50 7 8 49 csbie2 ( 2nd𝑦 ) / 𝑗 ( 1st𝑦 ) / 𝑘 𝐷 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ / 𝑦 𝐶
51 43 50 eqtr4di ( 𝑦 𝐴𝐶 = ( 2nd𝑦 ) / 𝑗 ( 1st𝑦 ) / 𝑘 𝐷 )
52 51 sumeq2i Σ 𝑦 𝐴 𝐶 = Σ 𝑦 𝐴 ( 2nd𝑦 ) / 𝑗 ( 1st𝑦 ) / 𝑘 𝐷
53 41 52 eqtr4di ( 𝜑 → Σ 𝑥𝐴 𝐵 = Σ 𝑦 𝐴 𝐶 )