Metamath Proof Explorer

Theorem fsum2cn

Description: Version of fsumcn for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014)

Ref Expression
Hypotheses fsumcn.3 
|- K = ( TopOpen ` CCfld )
fsumcn.4 
|- ( ph -> J e. ( TopOn ` X ) )
fsumcn.5 
|- ( ph -> A e. Fin )
fsum2cn.7 
|- ( ph -> L e. ( TopOn ` Y ) )
fsum2cn.8 
|- ( ( ph /\ k e. A ) -> ( x e. X , y e. Y |-> B ) e. ( ( J tX L ) Cn K ) )
Assertion fsum2cn 
|- ( ph -> ( x e. X , y e. Y |-> sum_ k e. A B ) e. ( ( J tX L ) Cn K ) )

Proof

Step Hyp Ref Expression
1 fsumcn.3 
 |-  K = ( TopOpen ` CCfld )
2 fsumcn.4 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 fsumcn.5 
 |-  ( ph -> A e. Fin )
4 fsum2cn.7 
 |-  ( ph -> L e. ( TopOn ` Y ) )
5 fsum2cn.8 
 |-  ( ( ph /\ k e. A ) -> ( x e. X , y e. Y |-> B ) e. ( ( J tX L ) Cn K ) )
6 nfcv 
 |-  F/_ u sum_ k e. A B
7 nfcv 
 |-  F/_ v sum_ k e. A B
8 nfcv 
 |-  F/_ x A
9 nfcv 
 |-  F/_ x v
10 nfcsb1v 
 |-  F/_ x [_ u / x ]_ B
11 9 10 nfcsbw 
 |-  F/_ x [_ v / y ]_ [_ u / x ]_ B
12 8 11 nfsum 
 |-  F/_ x sum_ k e. A [_ v / y ]_ [_ u / x ]_ B
13 nfcv 
 |-  F/_ y A
14 nfcsb1v 
 |-  F/_ y [_ v / y ]_ [_ u / x ]_ B
15 13 14 nfsum 
 |-  F/_ y sum_ k e. A [_ v / y ]_ [_ u / x ]_ B
16 csbeq1a 
 |-  ( x = u -> B = [_ u / x ]_ B )
17 csbeq1a 
 |-  ( y = v -> [_ u / x ]_ B = [_ v / y ]_ [_ u / x ]_ B )
18 16 17 sylan9eq 
 |-  ( ( x = u /\ y = v ) -> B = [_ v / y ]_ [_ u / x ]_ B )
19 18 sumeq2sdv 
 |-  ( ( x = u /\ y = v ) -> sum_ k e. A B = sum_ k e. A [_ v / y ]_ [_ u / x ]_ B )
20 6 7 12 15 19 cbvmpo 
 |-  ( x e. X , y e. Y |-> sum_ k e. A B ) = ( u e. X , v e. Y |-> sum_ k e. A [_ v / y ]_ [_ u / x ]_ B )
21 vex 
 |-  u e. _V
22 vex 
 |-  v e. _V
23 21 22 op2ndd 
 |-  ( z = <. u , v >. -> ( 2nd ` z ) = v )
24 23 csbeq1d 
 |-  ( z = <. u , v >. -> [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B = [_ v / y ]_ [_ ( 1st ` z ) / x ]_ B )
25 21 22 op1std 
 |-  ( z = <. u , v >. -> ( 1st ` z ) = u )
26 25 csbeq1d 
 |-  ( z = <. u , v >. -> [_ ( 1st ` z ) / x ]_ B = [_ u / x ]_ B )
27 26 csbeq2dv 
 |-  ( z = <. u , v >. -> [_ v / y ]_ [_ ( 1st ` z ) / x ]_ B = [_ v / y ]_ [_ u / x ]_ B )
28 24 27 eqtrd 
 |-  ( z = <. u , v >. -> [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B = [_ v / y ]_ [_ u / x ]_ B )
29 28 sumeq2sdv 
 |-  ( z = <. u , v >. -> sum_ k e. A [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B = sum_ k e. A [_ v / y ]_ [_ u / x ]_ B )
30 29 mpompt 
 |-  ( z e. ( X X. Y ) |-> sum_ k e. A [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B ) = ( u e. X , v e. Y |-> sum_ k e. A [_ v / y ]_ [_ u / x ]_ B )
31 20 30 eqtr4i 
 |-  ( x e. X , y e. Y |-> sum_ k e. A B ) = ( z e. ( X X. Y ) |-> sum_ k e. A [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B )
32 txtopon 
 |-  ( ( J e. ( TopOn ` X ) /\ L e. ( TopOn ` Y ) ) -> ( J tX L ) e. ( TopOn ` ( X X. Y ) ) )
33 2 4 32 syl2anc 
 |-  ( ph -> ( J tX L ) e. ( TopOn ` ( X X. Y ) ) )
34 nfcv 
 |-  F/_ u B
35 nfcv 
 |-  F/_ v B
36 34 35 11 14 18 cbvmpo 
 |-  ( x e. X , y e. Y |-> B ) = ( u e. X , v e. Y |-> [_ v / y ]_ [_ u / x ]_ B )
37 28 mpompt 
 |-  ( z e. ( X X. Y ) |-> [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B ) = ( u e. X , v e. Y |-> [_ v / y ]_ [_ u / x ]_ B )
38 36 37 eqtr4i 
 |-  ( x e. X , y e. Y |-> B ) = ( z e. ( X X. Y ) |-> [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B )
39 38 5 eqeltrrid 
 |-  ( ( ph /\ k e. A ) -> ( z e. ( X X. Y ) |-> [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B ) e. ( ( J tX L ) Cn K ) )
40 1 33 3 39 fsumcn 
 |-  ( ph -> ( z e. ( X X. Y ) |-> sum_ k e. A [_ ( 2nd ` z ) / y ]_ [_ ( 1st ` z ) / x ]_ B ) e. ( ( J tX L ) Cn K ) )
41 31 40 eqeltrid 
 |-  ( ph -> ( x e. X , y e. Y |-> sum_ k e. A B ) e. ( ( J tX L ) Cn K ) )