Metamath Proof Explorer


Theorem fprodcnv

Description: Transform a product region using the converse operation. (Contributed by Scott Fenton, 1-Feb-2018)

Ref Expression
Hypotheses fprodcnv.1
|- ( x = <. j , k >. -> B = D )
fprodcnv.2
|- ( y = <. k , j >. -> C = D )
fprodcnv.3
|- ( ph -> A e. Fin )
fprodcnv.4
|- ( ph -> Rel A )
fprodcnv.5
|- ( ( ph /\ x e. A ) -> B e. CC )
Assertion fprodcnv
|- ( ph -> prod_ x e. A B = prod_ y e. `' A C )

Proof

Step Hyp Ref Expression
1 fprodcnv.1
 |-  ( x = <. j , k >. -> B = D )
2 fprodcnv.2
 |-  ( y = <. k , j >. -> C = D )
3 fprodcnv.3
 |-  ( ph -> A e. Fin )
4 fprodcnv.4
 |-  ( ph -> Rel A )
5 fprodcnv.5
 |-  ( ( ph /\ x e. A ) -> B e. CC )
6 csbeq1a
 |-  ( x = <. ( 2nd ` y ) , ( 1st ` y ) >. -> B = [_ <. ( 2nd ` y ) , ( 1st ` y ) >. / x ]_ B )
7 fvex
 |-  ( 2nd ` y ) e. _V
8 fvex
 |-  ( 1st ` y ) e. _V
9 opex
 |-  <. j , k >. e. _V
10 9 1 csbie
 |-  [_ <. j , k >. / x ]_ B = D
11 opeq12
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> <. j , k >. = <. ( 2nd ` y ) , ( 1st ` y ) >. )
12 11 csbeq1d
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> [_ <. j , k >. / x ]_ B = [_ <. ( 2nd ` y ) , ( 1st ` y ) >. / x ]_ B )
13 10 12 eqtr3id
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> D = [_ <. ( 2nd ` y ) , ( 1st ` y ) >. / x ]_ B )
14 7 8 13 csbie2
 |-  [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D = [_ <. ( 2nd ` y ) , ( 1st ` y ) >. / x ]_ B
15 6 14 eqtr4di
 |-  ( x = <. ( 2nd ` y ) , ( 1st ` y ) >. -> B = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D )
16 cnvfi
 |-  ( A e. Fin -> `' A e. Fin )
17 3 16 syl
 |-  ( ph -> `' A e. Fin )
18 relcnv
 |-  Rel `' A
19 cnvf1o
 |-  ( Rel `' A -> ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> `' `' A )
20 18 19 ax-mp
 |-  ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> `' `' A
21 dfrel2
 |-  ( Rel A <-> `' `' A = A )
22 4 21 sylib
 |-  ( ph -> `' `' A = A )
23 22 f1oeq3d
 |-  ( ph -> ( ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> `' `' A <-> ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> A ) )
24 20 23 mpbii
 |-  ( ph -> ( z e. `' A |-> U. `' { z } ) : `' A -1-1-onto-> A )
25 1st2nd
 |-  ( ( Rel `' A /\ y e. `' A ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
26 18 25 mpan
 |-  ( y e. `' A -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
27 26 fveq2d
 |-  ( y e. `' A -> ( ( z e. `' A |-> U. `' { z } ) ` y ) = ( ( z e. `' A |-> U. `' { z } ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) )
28 26 eleq1d
 |-  ( y e. `' A -> ( y e. `' A <-> <. ( 1st ` y ) , ( 2nd ` y ) >. e. `' A ) )
29 28 ibi
 |-  ( y e. `' A -> <. ( 1st ` y ) , ( 2nd ` y ) >. e. `' A )
30 sneq
 |-  ( z = <. ( 1st ` y ) , ( 2nd ` y ) >. -> { z } = { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
31 30 cnveqd
 |-  ( z = <. ( 1st ` y ) , ( 2nd ` y ) >. -> `' { z } = `' { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
32 31 unieqd
 |-  ( z = <. ( 1st ` y ) , ( 2nd ` y ) >. -> U. `' { z } = U. `' { <. ( 1st ` y ) , ( 2nd ` y ) >. } )
33 opswap
 |-  U. `' { <. ( 1st ` y ) , ( 2nd ` y ) >. } = <. ( 2nd ` y ) , ( 1st ` y ) >.
34 32 33 eqtrdi
 |-  ( z = <. ( 1st ` y ) , ( 2nd ` y ) >. -> U. `' { z } = <. ( 2nd ` y ) , ( 1st ` y ) >. )
35 eqid
 |-  ( z e. `' A |-> U. `' { z } ) = ( z e. `' A |-> U. `' { z } )
36 opex
 |-  <. ( 2nd ` y ) , ( 1st ` y ) >. e. _V
37 34 35 36 fvmpt
 |-  ( <. ( 1st ` y ) , ( 2nd ` y ) >. e. `' A -> ( ( z e. `' A |-> U. `' { z } ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
38 29 37 syl
 |-  ( y e. `' A -> ( ( z e. `' A |-> U. `' { z } ) ` <. ( 1st ` y ) , ( 2nd ` y ) >. ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
39 27 38 eqtrd
 |-  ( y e. `' A -> ( ( z e. `' A |-> U. `' { z } ) ` y ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
40 39 adantl
 |-  ( ( ph /\ y e. `' A ) -> ( ( z e. `' A |-> U. `' { z } ) ` y ) = <. ( 2nd ` y ) , ( 1st ` y ) >. )
41 15 17 24 40 5 fprodf1o
 |-  ( ph -> prod_ x e. A B = prod_ y e. `' A [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D )
42 csbeq1a
 |-  ( y = <. ( 1st ` y ) , ( 2nd ` y ) >. -> C = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C )
43 26 42 syl
 |-  ( y e. `' A -> C = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C )
44 opex
 |-  <. k , j >. e. _V
45 44 2 csbie
 |-  [_ <. k , j >. / y ]_ C = D
46 opeq12
 |-  ( ( k = ( 1st ` y ) /\ j = ( 2nd ` y ) ) -> <. k , j >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
47 46 ancoms
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> <. k , j >. = <. ( 1st ` y ) , ( 2nd ` y ) >. )
48 47 csbeq1d
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> [_ <. k , j >. / y ]_ C = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C )
49 45 48 eqtr3id
 |-  ( ( j = ( 2nd ` y ) /\ k = ( 1st ` y ) ) -> D = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C )
50 7 8 49 csbie2
 |-  [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D = [_ <. ( 1st ` y ) , ( 2nd ` y ) >. / y ]_ C
51 43 50 eqtr4di
 |-  ( y e. `' A -> C = [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D )
52 51 prodeq2i
 |-  prod_ y e. `' A C = prod_ y e. `' A [_ ( 2nd ` y ) / j ]_ [_ ( 1st ` y ) / k ]_ D
53 41 52 eqtr4di
 |-  ( ph -> prod_ x e. A B = prod_ y e. `' A C )