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^{E}$
	fmptco1f1o.b	$⊢ B = R^{D}$
	fmptco1f1o.f	$⊢ F = (f \in A ⟼ f \circ T)$
	fmptco1f1o.d	$⊢ φ \to D \in V$
	fmptco1f1o.e	$⊢ φ \to E \in W$
	fmptco1f1o.r	$⊢ φ \to R \in X$
	fmptco1f1o.t	$⊢ φ \to T : D \underset{1-1 onto}{⟶} E$
Assertion	fmptco1f1o	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		fmptco1f1o.a	$⊢ A = R^{E}$
2		fmptco1f1o.b	$⊢ B = R^{D}$
3		fmptco1f1o.f	$⊢ F = (f \in A ⟼ f \circ T)$
4		fmptco1f1o.d	$⊢ φ \to D \in V$
5		fmptco1f1o.e	$⊢ φ \to E \in W$
6		fmptco1f1o.r	$⊢ φ \to R \in X$
7		fmptco1f1o.t	$⊢ φ \to T : D \underset{1-1 onto}{⟶} E$
8	3	a1i	$⊢ φ \to F = (f \in A ⟼ f \circ T)$
9	6	adantr	$⊢ (φ \land f \in A) \to R \in X$
10	4	adantr	$⊢ (φ \land f \in A) \to D \in V$
11		simpr	$⊢ (φ \land f \in A) \to f \in A$
12	11 1	eleqtrdi	$⊢ (φ \land f \in A) \to f \in (R^{E})$
13		elmapi	$⊢ f \in (R^{E}) \to f : E ⟶ R$
14	12 13	syl	$⊢ (φ \land f \in A) \to f : E ⟶ R$
15		f1of	$⊢ T : D \underset{1-1 onto}{⟶} E \to T : D ⟶ E$
16	7 15	syl	$⊢ φ \to T : D ⟶ E$
17	16	adantr	$⊢ (φ \land f \in A) \to T : D ⟶ E$
18		fco	$⊢ (f : E ⟶ R \land T : D ⟶ E) \to (f \circ T) : D ⟶ R$
19	14 17 18	syl2anc	$⊢ (φ \land f \in A) \to (f \circ T) : D ⟶ R$
20		elmapg	$⊢ (R \in X \land D \in V) \to (f \circ T \in (R^{D}) \leftrightarrow (f \circ T) : D ⟶ R)$
21	20	biimpar	$⊢ ((R \in X \land D \in V) \land (f \circ T) : D ⟶ R) \to f \circ T \in (R^{D})$
22	9 10 19 21	syl21anc	$⊢ (φ \land f \in A) \to f \circ T \in (R^{D})$
23	22 2	eleqtrrdi	$⊢ (φ \land f \in A) \to f \circ T \in B$
24	6	adantr	$⊢ (φ \land g \in B) \to R \in X$
25	5	adantr	$⊢ (φ \land g \in B) \to E \in W$
26		simpr	$⊢ (φ \land g \in B) \to g \in B$
27	26 2	eleqtrdi	$⊢ (φ \land g \in B) \to g \in (R^{D})$
28		elmapi	$⊢ g \in (R^{D}) \to g : D ⟶ R$
29	27 28	syl	$⊢ (φ \land g \in B) \to g : D ⟶ R$
30		f1ocnv	$⊢ T : D \underset{1-1 onto}{⟶} E \to T^{-1} : E \underset{1-1 onto}{⟶} D$
31		f1of	$⊢ T^{-1} : E \underset{1-1 onto}{⟶} D \to T^{-1} : E ⟶ D$
32	7 30 31	3syl	$⊢ φ \to T^{-1} : E ⟶ D$
33	32	adantr	$⊢ (φ \land g \in B) \to T^{-1} : E ⟶ D$
34		fco	$⊢ (g : D ⟶ R \land T^{-1} : E ⟶ D) \to (g \circ T^{-1}) : E ⟶ R$
35	29 33 34	syl2anc	$⊢ (φ \land g \in B) \to (g \circ T^{-1}) : E ⟶ R$
36		elmapg	$⊢ (R \in X \land E \in W) \to (g \circ T^{-1} \in (R^{E}) \leftrightarrow (g \circ T^{-1}) : E ⟶ R)$
37	36	biimpar	$⊢ ((R \in X \land E \in W) \land (g \circ T^{-1}) : E ⟶ R) \to g \circ T^{-1} \in (R^{E})$
38	24 25 35 37	syl21anc	$⊢ (φ \land g \in B) \to g \circ T^{-1} \in (R^{E})$
39	38 1	eleqtrrdi	$⊢ (φ \land g \in B) \to g \circ T^{-1} \in A$
40		coass	$⊢ (g \circ T^{-1}) \circ T = g \circ (T^{-1} \circ T)$
41	7	ad2antrr	$⊢ ((φ \land f \in A) \land g \in B) \to T : D \underset{1-1 onto}{⟶} E$
42		f1ococnv1	$⊢ T : D \underset{1-1 onto}{⟶} E \to T^{-1} \circ T = {I ↾}_{D}$
43	42	coeq2d	$⊢ T : D \underset{1-1 onto}{⟶} E \to g \circ (T^{-1} \circ T) = g \circ ({I ↾}_{D})$
44	41 43	syl	$⊢ ((φ \land f \in A) \land g \in B) \to g \circ (T^{-1} \circ T) = g \circ ({I ↾}_{D})$
45	29	adantlr	$⊢ ((φ \land f \in A) \land g \in B) \to g : D ⟶ R$
46		fcoi1	$⊢ g : D ⟶ R \to g \circ ({I ↾}_{D}) = g$
47	45 46	syl	$⊢ ((φ \land f \in A) \land g \in B) \to g \circ ({I ↾}_{D}) = g$
48	44 47	eqtrd	$⊢ ((φ \land f \in A) \land g \in B) \to g \circ (T^{-1} \circ T) = g$
49	40 48	eqtr2id	$⊢ ((φ \land f \in A) \land g \in B) \to g = (g \circ T^{-1}) \circ T$
50	49	eqeq1d	$⊢ ((φ \land f \in A) \land g \in B) \to (g = f \circ T \leftrightarrow (g \circ T^{-1}) \circ T = f \circ T)$
51		eqcom	$⊢ (g \circ T^{-1}) \circ T = f \circ T \leftrightarrow f \circ T = (g \circ T^{-1}) \circ T$
52	51	a1i	$⊢ ((φ \land f \in A) \land g \in B) \to ((g \circ T^{-1}) \circ T = f \circ T \leftrightarrow f \circ T = (g \circ T^{-1}) \circ T)$
53		f1ofo	$⊢ T : D \underset{1-1 onto}{⟶} E \to T : D \underset{onto}{⟶} E$
54	41 53	syl	$⊢ ((φ \land f \in A) \land g \in B) \to T : D \underset{onto}{⟶} E$
55		simplr	$⊢ ((φ \land f \in A) \land g \in B) \to f \in A$
56	55 1	eleqtrdi	$⊢ ((φ \land f \in A) \land g \in B) \to f \in (R^{E})$
57		elmapfn	$⊢ f \in (R^{E}) \to f Fn E$
58	56 57	syl	$⊢ ((φ \land f \in A) \land g \in B) \to f Fn E$
59		elmapfn	$⊢ g \circ T^{-1} \in (R^{E}) \to (g \circ T^{-1}) Fn E$
60	38 59	syl	$⊢ (φ \land g \in B) \to (g \circ T^{-1}) Fn E$
61	60	adantlr	$⊢ ((φ \land f \in A) \land g \in B) \to (g \circ T^{-1}) Fn E$
62		cocan2	$⊢ (T : D \underset{onto}{⟶} E \land f Fn E \land (g \circ T^{-1}) Fn E) \to (f \circ T = (g \circ T^{-1}) \circ T \leftrightarrow f = g \circ T^{-1})$
63	54 58 61 62	syl3anc	$⊢ ((φ \land f \in A) \land g \in B) \to (f \circ T = (g \circ T^{-1}) \circ T \leftrightarrow f = g \circ T^{-1})$
64	50 52 63	3bitrrd	$⊢ ((φ \land f \in A) \land g \in B) \to (f = g \circ T^{-1} \leftrightarrow g = f \circ T)$
65	64	anasss	$⊢ (φ \land (f \in A \land g \in B)) \to (f = g \circ T^{-1} \leftrightarrow g = f \circ T)$
66	8 23 39 65	f1o3d	$⊢ φ \to (F : A \underset{1-1 onto}{⟶} B \land F^{-1} = (g \in B ⟼ g \circ T^{-1}))$
67	66	simpld	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem fmptco1f1o

Proof