Metamath Proof Explorer


Theorem mapfien

Description: A bijection of the base sets induces a bijection on the set of finitely supported functions. (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-Jul-2019) (Revised by AV, 28-Jul-2024)

Ref Expression
Hypotheses mapfien.s S = x B A | finSupp Z x
mapfien.t T = x D C | finSupp W x
mapfien.w W = G Z
mapfien.f φ F : C 1-1 onto A
mapfien.g φ G : B 1-1 onto D
mapfien.a φ A U
mapfien.b φ B V
mapfien.c φ C X
mapfien.d φ D Y
mapfien.z φ Z B
Assertion mapfien φ f S G f F : S 1-1 onto T

Proof

Step Hyp Ref Expression
1 mapfien.s S = x B A | finSupp Z x
2 mapfien.t T = x D C | finSupp W x
3 mapfien.w W = G Z
4 mapfien.f φ F : C 1-1 onto A
5 mapfien.g φ G : B 1-1 onto D
6 mapfien.a φ A U
7 mapfien.b φ B V
8 mapfien.c φ C X
9 mapfien.d φ D Y
10 mapfien.z φ Z B
11 eqid f S G f F = f S G f F
12 f1of G : B 1-1 onto D G : B D
13 5 12 syl φ G : B D
14 13 adantr φ f S G : B D
15 breq1 x = f finSupp Z x finSupp Z f
16 15 1 elrab2 f S f B A finSupp Z f
17 16 simplbi f S f B A
18 17 adantl φ f S f B A
19 elmapi f B A f : A B
20 18 19 syl φ f S f : A B
21 f1of F : C 1-1 onto A F : C A
22 4 21 syl φ F : C A
23 22 adantr φ f S F : C A
24 20 23 fcod φ f S f F : C B
25 14 24 fcod φ f S G f F : C D
26 9 8 elmapd φ G f F D C G f F : C D
27 26 adantr φ f S G f F D C G f F : C D
28 25 27 mpbird φ f S G f F D C
29 1 2 3 4 5 6 7 8 9 10 mapfienlem1 φ f S finSupp W G f F
30 breq1 x = G f F finSupp W x finSupp W G f F
31 30 2 elrab2 G f F T G f F D C finSupp W G f F
32 28 29 31 sylanbrc φ f S G f F T
33 1 2 3 4 5 6 7 8 9 10 mapfienlem3 φ g T G -1 g F -1 S
34 coass G -1 g F -1 F = G -1 g F -1 F
35 4 adantr φ f S g T F : C 1-1 onto A
36 f1ococnv1 F : C 1-1 onto A F -1 F = I C
37 35 36 syl φ f S g T F -1 F = I C
38 37 coeq2d φ f S g T G -1 g F -1 F = G -1 g I C
39 f1ocnv G : B 1-1 onto D G -1 : D 1-1 onto B
40 f1of G -1 : D 1-1 onto B G -1 : D B
41 5 39 40 3syl φ G -1 : D B
42 41 adantr φ g T G -1 : D B
43 simpr φ g T g T
44 breq1 x = g finSupp W x finSupp W g
45 44 2 elrab2 g T g D C finSupp W g
46 43 45 sylib φ g T g D C finSupp W g
47 46 simpld φ g T g D C
48 elmapi g D C g : C D
49 47 48 syl φ g T g : C D
50 42 49 fcod φ g T G -1 g : C B
51 50 adantrl φ f S g T G -1 g : C B
52 fcoi1 G -1 g : C B G -1 g I C = G -1 g
53 51 52 syl φ f S g T G -1 g I C = G -1 g
54 38 53 eqtrd φ f S g T G -1 g F -1 F = G -1 g
55 34 54 eqtrid φ f S g T G -1 g F -1 F = G -1 g
56 55 eqeq2d φ f S g T f F = G -1 g F -1 F f F = G -1 g
57 coass G -1 G f F = G -1 G f F
58 5 adantr φ f S g T G : B 1-1 onto D
59 f1ococnv1 G : B 1-1 onto D G -1 G = I B
60 58 59 syl φ f S g T G -1 G = I B
61 60 coeq1d φ f S g T G -1 G f F = I B f F
62 24 adantrr φ f S g T f F : C B
63 fcoi2 f F : C B I B f F = f F
64 62 63 syl φ f S g T I B f F = f F
65 61 64 eqtrd φ f S g T G -1 G f F = f F
66 57 65 eqtr3id φ f S g T G -1 G f F = f F
67 66 eqeq2d φ f S g T G -1 g = G -1 G f F G -1 g = f F
68 eqcom G -1 g = f F f F = G -1 g
69 67 68 bitrdi φ f S g T G -1 g = G -1 G f F f F = G -1 g
70 56 69 bitr4d φ f S g T f F = G -1 g F -1 F G -1 g = G -1 G f F
71 f1ofo F : C 1-1 onto A F : C onto A
72 35 71 syl φ f S g T F : C onto A
73 ffn f : A B f Fn A
74 18 19 73 3syl φ f S f Fn A
75 74 adantrr φ f S g T f Fn A
76 f1ocnv F : C 1-1 onto A F -1 : A 1-1 onto C
77 f1of F -1 : A 1-1 onto C F -1 : A C
78 4 76 77 3syl φ F -1 : A C
79 78 adantr φ g T F -1 : A C
80 50 79 fcod φ g T G -1 g F -1 : A B
81 80 ffnd φ g T G -1 g F -1 Fn A
82 81 adantrl φ f S g T G -1 g F -1 Fn A
83 cocan2 F : C onto A f Fn A G -1 g F -1 Fn A f F = G -1 g F -1 F f = G -1 g F -1
84 72 75 82 83 syl3anc φ f S g T f F = G -1 g F -1 F f = G -1 g F -1
85 5 39 syl φ G -1 : D 1-1 onto B
86 85 adantr φ f S g T G -1 : D 1-1 onto B
87 f1of1 G -1 : D 1-1 onto B G -1 : D 1-1 B
88 86 87 syl φ f S g T G -1 : D 1-1 B
89 49 adantrl φ f S g T g : C D
90 25 adantrr φ f S g T G f F : C D
91 cocan1 G -1 : D 1-1 B g : C D G f F : C D G -1 g = G -1 G f F g = G f F
92 88 89 90 91 syl3anc φ f S g T G -1 g = G -1 G f F g = G f F
93 70 84 92 3bitr3d φ f S g T f = G -1 g F -1 g = G f F
94 11 32 33 93 f1o2d φ f S G f F : S 1-1 onto T