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		simpr	$⊢ (φ \land g \in T) \to g \in T$
44		breq1	$⊢ x = g \to ({finSupp}_{W} (x) \leftrightarrow {finSupp}_{W} (g))$
45	44 2	elrab2	$⊢ g \in T \leftrightarrow (g \in (D^{C}) \land {finSupp}_{W} (g))$
46	43 45	sylib	$⊢ (φ \land g \in T) \to (g \in (D^{C}) \land {finSupp}_{W} (g))$
47	46	simpld	$⊢ (φ \land g \in T) \to g \in (D^{C})$
48		elmapi	$⊢ g \in (D^{C}) \to g : C ⟶ D$
49	47 48	syl	$⊢ (φ \land g \in T) \to g : C ⟶ D$
50	42 49	fcod	$⊢ (φ \land g \in T) \to (G^{-1} \circ g) : C ⟶ B$
51	50	adantrl	$⊢ (φ \land (f \in S \land g \in T)) \to (G^{-1} \circ g) : C ⟶ B$
52		fcoi1	$⊢ (G^{-1} \circ g) : C ⟶ B \to (G^{-1} \circ g) \circ ({I ↾}_{C}) = G^{-1} \circ g$
53	51 52	syl	$⊢ (φ \land (f \in S \land g \in T)) \to (G^{-1} \circ g) \circ ({I ↾}_{C}) = G^{-1} \circ g$
54	38 53	eqtrd	$⊢ (φ \land (f \in S \land g \in T)) \to (G^{-1} \circ g) \circ (F^{-1} \circ F) = G^{-1} \circ g$
55	34 54	syl5eq	$⊢ (φ \land (f \in S \land g \in T)) \to ((G^{-1} \circ g) \circ F^{-1}) \circ F = G^{-1} \circ g$
56	55	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)$
57		coass	$⊢ (G^{-1} \circ G) \circ (f \circ F) = G^{-1} \circ (G \circ (f \circ F))$
58	5	adantr	$⊢ (φ \land (f \in S \land g \in T)) \to G : B \underset{1-1 onto}{⟶} D$
59		f1ococnv1	$⊢ G : B \underset{1-1 onto}{⟶} D \to G^{-1} \circ G = {I ↾}_{B}$
60	58 59	syl	$⊢ (φ \land (f \in S \land g \in T)) \to G^{-1} \circ G = {I ↾}_{B}$
61	60	coeq1d	$⊢ (φ \land (f \in S \land g \in T)) \to (G^{-1} \circ G) \circ (f \circ F) = ({I ↾}_{B}) \circ (f \circ F)$
62	24	adantrr	$⊢ (φ \land (f \in S \land g \in T)) \to (f \circ F) : C ⟶ B$
63		fcoi2	$⊢ (f \circ F) : C ⟶ B \to ({I ↾}_{B}) \circ (f \circ F) = f \circ F$
64	62 63	syl	$⊢ (φ \land (f \in S \land g \in T)) \to ({I ↾}_{B}) \circ (f \circ F) = f \circ F$
65	61 64	eqtrd	$⊢ (φ \land (f \in S \land g \in T)) \to (G^{-1} \circ G) \circ (f \circ F) = f \circ F$
66	57 65	eqtr3id	$⊢ (φ \land (f \in S \land g \in T)) \to G^{-1} \circ (G \circ (f \circ F)) = f \circ F$
67	66	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)$
68		eqcom	$⊢ G^{-1} \circ g = f \circ F \leftrightarrow f \circ F = G^{-1} \circ g$
69	67 68	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)$
70	56 69	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)))$
71		f1ofo	$⊢ F : C \underset{1-1 onto}{⟶} A \to F : C \underset{onto}{⟶} A$
72	35 71	syl	$⊢ (φ \land (f \in S \land g \in T)) \to F : C \underset{onto}{⟶} A$
73		ffn	$⊢ f : A ⟶ B \to f Fn A$
74	18 19 73	3syl	$⊢ (φ \land f \in S) \to f Fn A$
75	74	adantrr	$⊢ (φ \land (f \in S \land g \in T)) \to f Fn A$
76		f1ocnv	$⊢ F : C \underset{1-1 onto}{⟶} A \to F^{-1} : A \underset{1-1 onto}{⟶} C$
77		f1of	$⊢ F^{-1} : A \underset{1-1 onto}{⟶} C \to F^{-1} : A ⟶ C$
78	4 76 77	3syl	$⊢ φ \to F^{-1} : A ⟶ C$
79	78	adantr	$⊢ (φ \land g \in T) \to F^{-1} : A ⟶ C$
80	50 79	fcod	$⊢ (φ \land g \in T) \to ((G^{-1} \circ g) \circ F^{-1}) : A ⟶ B$
81	80	ffnd	$⊢ (φ \land g \in T) \to ((G^{-1} \circ g) \circ F^{-1}) Fn A$
82	81	adantrl	$⊢ (φ \land (f \in S \land g \in T)) \to ((G^{-1} \circ g) \circ F^{-1}) Fn A$
83		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})$
84	72 75 82 83	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})$
85	5 39	syl	$⊢ φ \to G^{-1} : D \underset{1-1 onto}{⟶} B$
86	85	adantr	$⊢ (φ \land (f \in S \land g \in T)) \to G^{-1} : D \underset{1-1 onto}{⟶} B$
87		f1of1	$⊢ G^{-1} : D \underset{1-1 onto}{⟶} B \to G^{-1} : D \underset{1-1}{⟶} B$
88	86 87	syl	$⊢ (φ \land (f \in S \land g \in T)) \to G^{-1} : D \underset{1-1}{⟶} B$
89	49	adantrl	$⊢ (φ \land (f \in S \land g \in T)) \to g : C ⟶ D$
90	25	adantrr	$⊢ (φ \land (f \in S \land g \in T)) \to (G \circ (f \circ F)) : C ⟶ D$
91		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))$
92	88 89 90 91	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))$
93	70 84 92	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))$
94	11 32 33 93	f1o2d	$⊢ φ \to (f \in S ⟼ G \circ (f \circ F)) : S \underset{1-1 onto}{⟶} T$

Metamath Proof Explorer

Theorem mapfien

Proof