mgmhmf1o

Description: A magma homomorphism is bijective iff its converse is also a magma homomorphism. (Contributed by AV, 25-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		mgmhmf1o.b	$⊢ B = {Base}_{R}$
2		mgmhmf1o.c	$⊢ C = {Base}_{S}$
3		mgmhmrcl	$⊢ F \in (R MgmHom S) \to (R \in Mgm \land S \in Mgm)$
4	3	ancomd	$⊢ F \in (R MgmHom S) \to (S \in Mgm \land R \in Mgm)$
5	4	adantr	$⊢ (F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (S \in Mgm \land R \in Mgm)$
6		f1ocnv	$⊢ F : B \underset{1-1 onto}{⟶} C \to F^{-1} : C \underset{1-1 onto}{⟶} B$
7	6	adantl	$⊢ (F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} : C \underset{1-1 onto}{⟶} B$
8		f1of	$⊢ F^{-1} : C \underset{1-1 onto}{⟶} B \to F^{-1} : C ⟶ B$
9	7 8	syl	$⊢ (F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} : C ⟶ B$
10		simpll	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F \in (R MgmHom S)$
11	9	adantr	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F^{-1} : C ⟶ B$
12		simprl	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to x \in C$
13	11 12	ffvelcdmd	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F^{-1} (x) \in B$
14		simprr	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to y \in C$
15	11 14	ffvelcdmd	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F^{-1} (y) \in B$
16		eqid	$⊢ +_{R} = +_{R}$
17		eqid	$⊢ +_{S} = +_{S}$
18	1 16 17	mgmhmlin	$⊢ (F \in (R MgmHom 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))$
19	10 13 15 18	syl3anc	$⊢ ((F \in (R MgmHom 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))$
20		simplr	$⊢ ((F \in (R MgmHom 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$
21		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} C \land x \in C) \to F (F^{-1} (x)) = x$
22	20 12 21	syl2anc	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F (F^{-1} (x)) = x$
23		f1ocnvfv2	$⊢ (F : B \underset{1-1 onto}{⟶} C \land y \in C) \to F (F^{-1} (y)) = y$
24	20 14 23	syl2anc	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to F (F^{-1} (y)) = y$
25	22 24	oveq12d	$⊢ ((F \in (R MgmHom 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$
26	19 25	eqtrd	$⊢ ((F \in (R MgmHom 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$
27	3	simpld	$⊢ F \in (R MgmHom S) \to R \in Mgm$
28	27	adantr	$⊢ (F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \to R \in Mgm$
29	28	adantr	$⊢ ((F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \land (x \in C \land y \in C)) \to R \in Mgm$
30	1 16	mgmcl	$⊢ (R \in Mgm \land F^{-1} (x) \in B \land F^{-1} (y) \in B) \to F^{-1} (x) +_{R} F^{-1} (y) \in B$
31	29 13 15 30	syl3anc	$⊢ ((F \in (R MgmHom 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$
32		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))$
33	20 31 32	syl2anc	$⊢ ((F \in (R MgmHom 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))$
34	26 33	mpd	$⊢ ((F \in (R MgmHom 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)$
35	34	ralrimivva	$⊢ (F \in (R MgmHom 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)$
36	9 35	jca	$⊢ (F \in (R MgmHom 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))$
37	2 1 17 16	ismgmhm	$⊢ F^{-1} \in (S MgmHom R) \leftrightarrow ((S \in Mgm \land R \in Mgm) \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)))$
38	5 36 37	sylanbrc	$⊢ (F \in (R MgmHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} \in (S MgmHom R)$
39	1 2	mgmhmf	$⊢ F \in (R MgmHom S) \to F : B ⟶ C$
40	39	adantr	$⊢ (F \in (R MgmHom S) \land F^{-1} \in (S MgmHom R)) \to F : B ⟶ C$
41	40	ffnd	$⊢ (F \in (R MgmHom S) \land F^{-1} \in (S MgmHom R)) \to F Fn B$
42	2 1	mgmhmf	$⊢ F^{-1} \in (S MgmHom R) \to F^{-1} : C ⟶ B$
43	42	adantl	$⊢ (F \in (R MgmHom S) \land F^{-1} \in (S MgmHom R)) \to F^{-1} : C ⟶ B$
44	43	ffnd	$⊢ (F \in (R MgmHom S) \land F^{-1} \in (S MgmHom R)) \to F^{-1} Fn C$
45		dff1o4	$⊢ F : B \underset{1-1 onto}{⟶} C \leftrightarrow (F Fn B \land F^{-1} Fn C)$
46	41 44 45	sylanbrc	$⊢ (F \in (R MgmHom S) \land F^{-1} \in (S MgmHom R)) \to F : B \underset{1-1 onto}{⟶} C$
47	38 46	impbida	$⊢ F \in (R MgmHom S) \to (F : B \underset{1-1 onto}{⟶} C \leftrightarrow F^{-1} \in (S MgmHom R))$

Metamath Proof Explorer

Theorem mgmhmf1o

Proof