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 \in (B^{A}) \| {finSupp}_{Z} (x)\}$
	mapfien.t	$⊢ T = \{x \in (D^{C}) \| {finSupp}_{W} (x)\}$
	mapfien.w	$⊢ W = G (Z)$
	mapfien.f	$⊢ φ \to F : C \underset{1-1 onto}{⟶} A$
	mapfien.g	$⊢ φ \to G : B \underset{1-1 onto}{⟶} D$
	mapfien.a	$⊢ φ \to A \in U$
	mapfien.b	$⊢ φ \to B \in V$
	mapfien.c	$⊢ φ \to C \in X$
	mapfien.d	$⊢ φ \to D \in Y$
	mapfien.z	$⊢ φ \to Z \in B$
Assertion	mapfien	$⊢ φ \to (f \in S ⟼ G \circ (f \circ F)) : S \underset{1-1 onto}{⟶} T$

Proof

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

Metamath Proof Explorer

Theorem mapfien

Proof