mhmf1o

Description: A monoid homomorphism is bijective iff its converse is also a monoid homomorphism. (Contributed by AV, 22-Oct-2019)

	Ref	Expression
Hypotheses	mhmf1o.b	$⊢ B = {Base}_{R}$
	mhmf1o.c	$⊢ C = {Base}_{S}$
Assertion	mhmf1o	$⊢ F \in (R MndHom S) \to (F : B \underset{1-1 onto}{⟶} C \leftrightarrow F^{-1} \in (S MndHom R))$

Proof

Step	Hyp	Ref	Expression
1		mhmf1o.b	$⊢ B = {Base}_{R}$
2		mhmf1o.c	$⊢ C = {Base}_{S}$
3		mhmrcl2	$⊢ F \in (R MndHom S) \to S \in Mnd$
4		mhmrcl1	$⊢ F \in (R MndHom S) \to R \in Mnd$
5	3 4	jca	$⊢ F \in (R MndHom S) \to (S \in Mnd \land R \in Mnd)$
6	5	adantr	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (S \in Mnd \land R \in Mnd)$
7		f1ocnv	$⊢ F : B \underset{1-1 onto}{⟶} C \to F^{-1} : C \underset{1-1 onto}{⟶} B$
8	7	adantl	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} : C \underset{1-1 onto}{⟶} B$
9		f1of	$⊢ F^{-1} : C \underset{1-1 onto}{⟶} B \to F^{-1} : C ⟶ B$
10	8 9	syl	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} : C ⟶ B$
11		simpll	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F \in (R MndHom S)$
12	10	adantr	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F^{-1} : C ⟶ B$
13		simprl	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to x \in C$
14	12 13	ffvelcdmd	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F^{-1} (x) \in B$
15		simprr	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to y \in C$
16	12 15	ffvelcdmd	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F^{-1} (y) \in B$
17		eqid	$⊢ +_{R} = +_{R}$
18		eqid	$⊢ +_{S} = +_{S}$
19	1 17 18	mhmlin	$⊢ (F \in (R MndHom S) \land F^{-1} (x) \in B \land F^{-1} (y) \in B) \to F (F^{-1} (x) +_{R} F^{-1} (y)) = F (F^{-1} (x)) +_{S} F (F^{-1} (y))$
20	11 14 16 19	syl3anc	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F (F^{-1} (x) +_{R} F^{-1} (y)) = F (F^{-1} (x)) +_{S} F (F^{-1} (y))$
21		simpr	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F : B \underset{1-1 onto}{⟶} C$
22	21	adantr	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F : B \underset{1-1 onto}{⟶} C$
23		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} C \land x \in C) \to F (F^{-1} (x)) = x$
24	22 13 23	syl2anc	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F (F^{-1} (x)) = x$
25		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} C \land y \in C) \to F (F^{-1} (y)) = y$
26	22 15 25	syl2anc	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F (F^{-1} (y)) = y$
27	24 26	oveq12d	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F (F^{-1} (x)) +_{S} F (F^{-1} (y)) = x +_{S} y$
28	20 27	eqtrd	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F (F^{-1} (x) +_{R} F^{-1} (y)) = x +_{S} y$
29	4	adantr	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to R \in Mnd$
30	29	adantr	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to R \in Mnd$
31	1 17	mndcl	$⊢ (R \in Mnd \land F^{-1} (x) \in B \land F^{-1} (y) \in B) \to F^{-1} (x) +_{R} F^{-1} (y) \in B$
32	30 14 16 31	syl3anc	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F^{-1} (x) +_{R} F^{-1} (y) \in B$
33		f1ocnvfv	$⊢ (F : B \underset{1-1 onto}{⟶} C \land F^{-1} (x) +_{R} F^{-1} (y) \in B) \to (F (F^{-1} (x) +_{R} F^{-1} (y)) = x +_{S} y \to F^{-1} (x +_{S} y) = F^{-1} (x) +_{R} F^{-1} (y))$
34	22 32 33	syl2anc	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to (F (F^{-1} (x) +_{R} F^{-1} (y)) = x +_{S} y \to F^{-1} (x +_{S} y) = F^{-1} (x) +_{R} F^{-1} (y))$
35	28 34	mpd	$⊢ ((F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F^{-1} (x +_{S} y) = F^{-1} (x) +_{R} F^{-1} (y)$
36	35	ralrimivva	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to \forall x \in C \forall y \in C F^{-1} (x +_{S} y) = F^{-1} (x) +_{R} F^{-1} (y)$
37		eqid	$⊢ 0_{R} = 0_{R}$
38		eqid	$⊢ 0_{S} = 0_{S}$
39	37 38	mhm0	$⊢ F \in (R MndHom S) \to F (0_{R}) = 0_{S}$
40	39	adantr	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F (0_{R}) = 0_{S}$
41	40	eqcomd	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to 0_{S} = F (0_{R})$
42	41	fveq2d	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} (0_{S}) = F^{-1} (F (0_{R}))$
43	1 37	mndidcl	$⊢ R \in Mnd \to 0_{R} \in B$
44	4 43	syl	$⊢ F \in (R MndHom S) \to 0_{R} \in B$
45	44	adantr	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to 0_{R} \in B$
46		f1ocnvfv1	$⊢ (F : B \underset{1-1 onto}{⟶} C \land 0_{R} \in B) \to F^{-1} (F (0_{R})) = 0_{R}$
47	21 45 46	syl2anc	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} (F (0_{R})) = 0_{R}$
48	42 47	eqtrd	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} (0_{S}) = 0_{R}$
49	10 36 48	3jca	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (F^{-1} : C ⟶ B \land \forall x \in C \forall y \in C F^{-1} (x +_{S} y) = F^{-1} (x) +_{R} F^{-1} (y) \land F^{-1} (0_{S}) = 0_{R})$
50	2 1 18 17 38 37	ismhm	$⊢ F^{-1} \in (S MndHom R) \leftrightarrow ((S \in Mnd \land R \in Mnd) \land (F^{-1} : C ⟶ B \land \forall x \in C \forall y \in C F^{-1} (x +_{S} y) = F^{-1} (x) +_{R} F^{-1} (y) \land F^{-1} (0_{S}) = 0_{R}))$
51	6 49 50	sylanbrc	$⊢ (F \in (R MndHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} \in (S MndHom R)$
52	1 2	mhmf	$⊢ F \in (R MndHom S) \to F : B ⟶ C$
53	52	adantr	$⊢ (F \in (R MndHom S) \land F^{-1} \in (S MndHom R)) \to F : B ⟶ C$
54	53	ffnd	$⊢ (F \in (R MndHom S) \land F^{-1} \in (S MndHom R)) \to F Fn B$
55	2 1	mhmf	$⊢ F^{-1} \in (S MndHom R) \to F^{-1} : C ⟶ B$
56	55	adantl	$⊢ (F \in (R MndHom S) \land F^{-1} \in (S MndHom R)) \to F^{-1} : C ⟶ B$
57	56	ffnd	$⊢ (F \in (R MndHom S) \land F^{-1} \in (S MndHom R)) \to F^{-1} Fn C$
58		dff1o4	$⊢ F : B \underset{1-1 onto}{⟶} C \leftrightarrow (F Fn B \land F^{-1} Fn C)$
59	54 57 58	sylanbrc	$⊢ (F \in (R MndHom S) \land F^{-1} \in (S MndHom R)) \to F : B \underset{1-1 onto}{⟶} C$
60	51 59	impbida	$⊢ F \in (R MndHom S) \to (F : B \underset{1-1 onto}{⟶} C \leftrightarrow F^{-1} \in (S MndHom R))$

Metamath Proof Explorer

Theorem mhmf1o

Proof