Metamath Proof Explorer


Theorem fmptco1f1o

Description: The action of composing (to the right) with a bijection is itself a bijection of functions. (Contributed by Thierry Arnoux, 3-Jan-2021)

Ref Expression
Hypotheses fmptco1f1o.a
|- A = ( R ^m E )
fmptco1f1o.b
|- B = ( R ^m D )
fmptco1f1o.f
|- F = ( f e. A |-> ( f o. T ) )
fmptco1f1o.d
|- ( ph -> D e. V )
fmptco1f1o.e
|- ( ph -> E e. W )
fmptco1f1o.r
|- ( ph -> R e. X )
fmptco1f1o.t
|- ( ph -> T : D -1-1-onto-> E )
Assertion fmptco1f1o
|- ( ph -> F : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 fmptco1f1o.a
 |-  A = ( R ^m E )
2 fmptco1f1o.b
 |-  B = ( R ^m D )
3 fmptco1f1o.f
 |-  F = ( f e. A |-> ( f o. T ) )
4 fmptco1f1o.d
 |-  ( ph -> D e. V )
5 fmptco1f1o.e
 |-  ( ph -> E e. W )
6 fmptco1f1o.r
 |-  ( ph -> R e. X )
7 fmptco1f1o.t
 |-  ( ph -> T : D -1-1-onto-> E )
8 3 a1i
 |-  ( ph -> F = ( f e. A |-> ( f o. T ) ) )
9 6 adantr
 |-  ( ( ph /\ f e. A ) -> R e. X )
10 4 adantr
 |-  ( ( ph /\ f e. A ) -> D e. V )
11 simpr
 |-  ( ( ph /\ f e. A ) -> f e. A )
12 11 1 eleqtrdi
 |-  ( ( ph /\ f e. A ) -> f e. ( R ^m E ) )
13 elmapi
 |-  ( f e. ( R ^m E ) -> f : E --> R )
14 12 13 syl
 |-  ( ( ph /\ f e. A ) -> f : E --> R )
15 f1of
 |-  ( T : D -1-1-onto-> E -> T : D --> E )
16 7 15 syl
 |-  ( ph -> T : D --> E )
17 16 adantr
 |-  ( ( ph /\ f e. A ) -> T : D --> E )
18 fco
 |-  ( ( f : E --> R /\ T : D --> E ) -> ( f o. T ) : D --> R )
19 14 17 18 syl2anc
 |-  ( ( ph /\ f e. A ) -> ( f o. T ) : D --> R )
20 elmapg
 |-  ( ( R e. X /\ D e. V ) -> ( ( f o. T ) e. ( R ^m D ) <-> ( f o. T ) : D --> R ) )
21 20 biimpar
 |-  ( ( ( R e. X /\ D e. V ) /\ ( f o. T ) : D --> R ) -> ( f o. T ) e. ( R ^m D ) )
22 9 10 19 21 syl21anc
 |-  ( ( ph /\ f e. A ) -> ( f o. T ) e. ( R ^m D ) )
23 22 2 eleqtrrdi
 |-  ( ( ph /\ f e. A ) -> ( f o. T ) e. B )
24 6 adantr
 |-  ( ( ph /\ g e. B ) -> R e. X )
25 5 adantr
 |-  ( ( ph /\ g e. B ) -> E e. W )
26 simpr
 |-  ( ( ph /\ g e. B ) -> g e. B )
27 26 2 eleqtrdi
 |-  ( ( ph /\ g e. B ) -> g e. ( R ^m D ) )
28 elmapi
 |-  ( g e. ( R ^m D ) -> g : D --> R )
29 27 28 syl
 |-  ( ( ph /\ g e. B ) -> g : D --> R )
30 f1ocnv
 |-  ( T : D -1-1-onto-> E -> `' T : E -1-1-onto-> D )
31 f1of
 |-  ( `' T : E -1-1-onto-> D -> `' T : E --> D )
32 7 30 31 3syl
 |-  ( ph -> `' T : E --> D )
33 32 adantr
 |-  ( ( ph /\ g e. B ) -> `' T : E --> D )
34 fco
 |-  ( ( g : D --> R /\ `' T : E --> D ) -> ( g o. `' T ) : E --> R )
35 29 33 34 syl2anc
 |-  ( ( ph /\ g e. B ) -> ( g o. `' T ) : E --> R )
36 elmapg
 |-  ( ( R e. X /\ E e. W ) -> ( ( g o. `' T ) e. ( R ^m E ) <-> ( g o. `' T ) : E --> R ) )
37 36 biimpar
 |-  ( ( ( R e. X /\ E e. W ) /\ ( g o. `' T ) : E --> R ) -> ( g o. `' T ) e. ( R ^m E ) )
38 24 25 35 37 syl21anc
 |-  ( ( ph /\ g e. B ) -> ( g o. `' T ) e. ( R ^m E ) )
39 38 1 eleqtrrdi
 |-  ( ( ph /\ g e. B ) -> ( g o. `' T ) e. A )
40 coass
 |-  ( ( g o. `' T ) o. T ) = ( g o. ( `' T o. T ) )
41 7 ad2antrr
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> T : D -1-1-onto-> E )
42 f1ococnv1
 |-  ( T : D -1-1-onto-> E -> ( `' T o. T ) = ( _I |` D ) )
43 42 coeq2d
 |-  ( T : D -1-1-onto-> E -> ( g o. ( `' T o. T ) ) = ( g o. ( _I |` D ) ) )
44 41 43 syl
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> ( g o. ( `' T o. T ) ) = ( g o. ( _I |` D ) ) )
45 29 adantlr
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> g : D --> R )
46 fcoi1
 |-  ( g : D --> R -> ( g o. ( _I |` D ) ) = g )
47 45 46 syl
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> ( g o. ( _I |` D ) ) = g )
48 44 47 eqtrd
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> ( g o. ( `' T o. T ) ) = g )
49 40 48 eqtr2id
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> g = ( ( g o. `' T ) o. T ) )
50 49 eqeq1d
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> ( g = ( f o. T ) <-> ( ( g o. `' T ) o. T ) = ( f o. T ) ) )
51 eqcom
 |-  ( ( ( g o. `' T ) o. T ) = ( f o. T ) <-> ( f o. T ) = ( ( g o. `' T ) o. T ) )
52 51 a1i
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> ( ( ( g o. `' T ) o. T ) = ( f o. T ) <-> ( f o. T ) = ( ( g o. `' T ) o. T ) ) )
53 f1ofo
 |-  ( T : D -1-1-onto-> E -> T : D -onto-> E )
54 41 53 syl
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> T : D -onto-> E )
55 simplr
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> f e. A )
56 55 1 eleqtrdi
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> f e. ( R ^m E ) )
57 elmapfn
 |-  ( f e. ( R ^m E ) -> f Fn E )
58 56 57 syl
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> f Fn E )
59 elmapfn
 |-  ( ( g o. `' T ) e. ( R ^m E ) -> ( g o. `' T ) Fn E )
60 38 59 syl
 |-  ( ( ph /\ g e. B ) -> ( g o. `' T ) Fn E )
61 60 adantlr
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> ( g o. `' T ) Fn E )
62 cocan2
 |-  ( ( T : D -onto-> E /\ f Fn E /\ ( g o. `' T ) Fn E ) -> ( ( f o. T ) = ( ( g o. `' T ) o. T ) <-> f = ( g o. `' T ) ) )
63 54 58 61 62 syl3anc
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> ( ( f o. T ) = ( ( g o. `' T ) o. T ) <-> f = ( g o. `' T ) ) )
64 50 52 63 3bitrrd
 |-  ( ( ( ph /\ f e. A ) /\ g e. B ) -> ( f = ( g o. `' T ) <-> g = ( f o. T ) ) )
65 64 anasss
 |-  ( ( ph /\ ( f e. A /\ g e. B ) ) -> ( f = ( g o. `' T ) <-> g = ( f o. T ) ) )
66 8 23 39 65 f1o3d
 |-  ( ph -> ( F : A -1-1-onto-> B /\ `' F = ( g e. B |-> ( g o. `' T ) ) ) )
67 66 simpld
 |-  ( ph -> F : A -1-1-onto-> B )