This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )