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 𝐴 = ( 𝑅m 𝐸 )
fmptco1f1o.b 𝐵 = ( 𝑅m 𝐷 )
fmptco1f1o.f 𝐹 = ( 𝑓𝐴 ↦ ( 𝑓𝑇 ) )
fmptco1f1o.d ( 𝜑𝐷𝑉 )
fmptco1f1o.e ( 𝜑𝐸𝑊 )
fmptco1f1o.r ( 𝜑𝑅𝑋 )
fmptco1f1o.t ( 𝜑𝑇 : 𝐷1-1-onto𝐸 )
Assertion fmptco1f1o ( 𝜑𝐹 : 𝐴1-1-onto𝐵 )

Proof

Step Hyp Ref Expression
1 fmptco1f1o.a 𝐴 = ( 𝑅m 𝐸 )
2 fmptco1f1o.b 𝐵 = ( 𝑅m 𝐷 )
3 fmptco1f1o.f 𝐹 = ( 𝑓𝐴 ↦ ( 𝑓𝑇 ) )
4 fmptco1f1o.d ( 𝜑𝐷𝑉 )
5 fmptco1f1o.e ( 𝜑𝐸𝑊 )
6 fmptco1f1o.r ( 𝜑𝑅𝑋 )
7 fmptco1f1o.t ( 𝜑𝑇 : 𝐷1-1-onto𝐸 )
8 3 a1i ( 𝜑𝐹 = ( 𝑓𝐴 ↦ ( 𝑓𝑇 ) ) )
9 6 adantr ( ( 𝜑𝑓𝐴 ) → 𝑅𝑋 )
10 4 adantr ( ( 𝜑𝑓𝐴 ) → 𝐷𝑉 )
11 simpr ( ( 𝜑𝑓𝐴 ) → 𝑓𝐴 )
12 11 1 eleqtrdi ( ( 𝜑𝑓𝐴 ) → 𝑓 ∈ ( 𝑅m 𝐸 ) )
13 elmapi ( 𝑓 ∈ ( 𝑅m 𝐸 ) → 𝑓 : 𝐸𝑅 )
14 12 13 syl ( ( 𝜑𝑓𝐴 ) → 𝑓 : 𝐸𝑅 )
15 f1of ( 𝑇 : 𝐷1-1-onto𝐸𝑇 : 𝐷𝐸 )
16 7 15 syl ( 𝜑𝑇 : 𝐷𝐸 )
17 16 adantr ( ( 𝜑𝑓𝐴 ) → 𝑇 : 𝐷𝐸 )
18 fco ( ( 𝑓 : 𝐸𝑅𝑇 : 𝐷𝐸 ) → ( 𝑓𝑇 ) : 𝐷𝑅 )
19 14 17 18 syl2anc ( ( 𝜑𝑓𝐴 ) → ( 𝑓𝑇 ) : 𝐷𝑅 )
20 elmapg ( ( 𝑅𝑋𝐷𝑉 ) → ( ( 𝑓𝑇 ) ∈ ( 𝑅m 𝐷 ) ↔ ( 𝑓𝑇 ) : 𝐷𝑅 ) )
21 20 biimpar ( ( ( 𝑅𝑋𝐷𝑉 ) ∧ ( 𝑓𝑇 ) : 𝐷𝑅 ) → ( 𝑓𝑇 ) ∈ ( 𝑅m 𝐷 ) )
22 9 10 19 21 syl21anc ( ( 𝜑𝑓𝐴 ) → ( 𝑓𝑇 ) ∈ ( 𝑅m 𝐷 ) )
23 22 2 eleqtrrdi ( ( 𝜑𝑓𝐴 ) → ( 𝑓𝑇 ) ∈ 𝐵 )
24 6 adantr ( ( 𝜑𝑔𝐵 ) → 𝑅𝑋 )
25 5 adantr ( ( 𝜑𝑔𝐵 ) → 𝐸𝑊 )
26 simpr ( ( 𝜑𝑔𝐵 ) → 𝑔𝐵 )
27 26 2 eleqtrdi ( ( 𝜑𝑔𝐵 ) → 𝑔 ∈ ( 𝑅m 𝐷 ) )
28 elmapi ( 𝑔 ∈ ( 𝑅m 𝐷 ) → 𝑔 : 𝐷𝑅 )
29 27 28 syl ( ( 𝜑𝑔𝐵 ) → 𝑔 : 𝐷𝑅 )
30 f1ocnv ( 𝑇 : 𝐷1-1-onto𝐸 𝑇 : 𝐸1-1-onto𝐷 )
31 f1of ( 𝑇 : 𝐸1-1-onto𝐷 𝑇 : 𝐸𝐷 )
32 7 30 31 3syl ( 𝜑 𝑇 : 𝐸𝐷 )
33 32 adantr ( ( 𝜑𝑔𝐵 ) → 𝑇 : 𝐸𝐷 )
34 fco ( ( 𝑔 : 𝐷𝑅 𝑇 : 𝐸𝐷 ) → ( 𝑔 𝑇 ) : 𝐸𝑅 )
35 29 33 34 syl2anc ( ( 𝜑𝑔𝐵 ) → ( 𝑔 𝑇 ) : 𝐸𝑅 )
36 elmapg ( ( 𝑅𝑋𝐸𝑊 ) → ( ( 𝑔 𝑇 ) ∈ ( 𝑅m 𝐸 ) ↔ ( 𝑔 𝑇 ) : 𝐸𝑅 ) )
37 36 biimpar ( ( ( 𝑅𝑋𝐸𝑊 ) ∧ ( 𝑔 𝑇 ) : 𝐸𝑅 ) → ( 𝑔 𝑇 ) ∈ ( 𝑅m 𝐸 ) )
38 24 25 35 37 syl21anc ( ( 𝜑𝑔𝐵 ) → ( 𝑔 𝑇 ) ∈ ( 𝑅m 𝐸 ) )
39 38 1 eleqtrrdi ( ( 𝜑𝑔𝐵 ) → ( 𝑔 𝑇 ) ∈ 𝐴 )
40 coass ( ( 𝑔 𝑇 ) ∘ 𝑇 ) = ( 𝑔 ∘ ( 𝑇𝑇 ) )
41 7 ad2antrr ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → 𝑇 : 𝐷1-1-onto𝐸 )
42 f1ococnv1 ( 𝑇 : 𝐷1-1-onto𝐸 → ( 𝑇𝑇 ) = ( I ↾ 𝐷 ) )
43 42 coeq2d ( 𝑇 : 𝐷1-1-onto𝐸 → ( 𝑔 ∘ ( 𝑇𝑇 ) ) = ( 𝑔 ∘ ( I ↾ 𝐷 ) ) )
44 41 43 syl ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → ( 𝑔 ∘ ( 𝑇𝑇 ) ) = ( 𝑔 ∘ ( I ↾ 𝐷 ) ) )
45 29 adantlr ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → 𝑔 : 𝐷𝑅 )
46 fcoi1 ( 𝑔 : 𝐷𝑅 → ( 𝑔 ∘ ( I ↾ 𝐷 ) ) = 𝑔 )
47 45 46 syl ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → ( 𝑔 ∘ ( I ↾ 𝐷 ) ) = 𝑔 )
48 44 47 eqtrd ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → ( 𝑔 ∘ ( 𝑇𝑇 ) ) = 𝑔 )
49 40 48 eqtr2id ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → 𝑔 = ( ( 𝑔 𝑇 ) ∘ 𝑇 ) )
50 49 eqeq1d ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → ( 𝑔 = ( 𝑓𝑇 ) ↔ ( ( 𝑔 𝑇 ) ∘ 𝑇 ) = ( 𝑓𝑇 ) ) )
51 eqcom ( ( ( 𝑔 𝑇 ) ∘ 𝑇 ) = ( 𝑓𝑇 ) ↔ ( 𝑓𝑇 ) = ( ( 𝑔 𝑇 ) ∘ 𝑇 ) )
52 51 a1i ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → ( ( ( 𝑔 𝑇 ) ∘ 𝑇 ) = ( 𝑓𝑇 ) ↔ ( 𝑓𝑇 ) = ( ( 𝑔 𝑇 ) ∘ 𝑇 ) ) )
53 f1ofo ( 𝑇 : 𝐷1-1-onto𝐸𝑇 : 𝐷onto𝐸 )
54 41 53 syl ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → 𝑇 : 𝐷onto𝐸 )
55 simplr ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → 𝑓𝐴 )
56 55 1 eleqtrdi ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → 𝑓 ∈ ( 𝑅m 𝐸 ) )
57 elmapfn ( 𝑓 ∈ ( 𝑅m 𝐸 ) → 𝑓 Fn 𝐸 )
58 56 57 syl ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → 𝑓 Fn 𝐸 )
59 elmapfn ( ( 𝑔 𝑇 ) ∈ ( 𝑅m 𝐸 ) → ( 𝑔 𝑇 ) Fn 𝐸 )
60 38 59 syl ( ( 𝜑𝑔𝐵 ) → ( 𝑔 𝑇 ) Fn 𝐸 )
61 60 adantlr ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → ( 𝑔 𝑇 ) Fn 𝐸 )
62 cocan2 ( ( 𝑇 : 𝐷onto𝐸𝑓 Fn 𝐸 ∧ ( 𝑔 𝑇 ) Fn 𝐸 ) → ( ( 𝑓𝑇 ) = ( ( 𝑔 𝑇 ) ∘ 𝑇 ) ↔ 𝑓 = ( 𝑔 𝑇 ) ) )
63 54 58 61 62 syl3anc ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → ( ( 𝑓𝑇 ) = ( ( 𝑔 𝑇 ) ∘ 𝑇 ) ↔ 𝑓 = ( 𝑔 𝑇 ) ) )
64 50 52 63 3bitrrd ( ( ( 𝜑𝑓𝐴 ) ∧ 𝑔𝐵 ) → ( 𝑓 = ( 𝑔 𝑇 ) ↔ 𝑔 = ( 𝑓𝑇 ) ) )
65 64 anasss ( ( 𝜑 ∧ ( 𝑓𝐴𝑔𝐵 ) ) → ( 𝑓 = ( 𝑔 𝑇 ) ↔ 𝑔 = ( 𝑓𝑇 ) ) )
66 8 23 39 65 f1o3d ( 𝜑 → ( 𝐹 : 𝐴1-1-onto𝐵 𝐹 = ( 𝑔𝐵 ↦ ( 𝑔 𝑇 ) ) ) )
67 66 simpld ( 𝜑𝐹 : 𝐴1-1-onto𝐵 )