rhmf1o

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

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

Proof

Step	Hyp	Ref	Expression
1		rhmf1o.b	$⊢ B = {Base}_{R}$
2		rhmf1o.c	$⊢ C = {Base}_{S}$
3		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
4		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
5	3 4	jca	$⊢ F \in (R RingHom S) \to (S \in Ring \land R \in Ring)$
6	5	adantr	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (S \in Ring \land R \in Ring)$
7		simpr	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F : B \underset{1-1 onto}{⟶} C$
8		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
9	8	adantr	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F \in (R GrpHom S)$
10	1 2	ghmf1o	$⊢ F \in (R GrpHom S) \to (F : B \underset{1-1 onto}{⟶} C \leftrightarrow F^{-1} \in (S GrpHom R))$
11	10	bicomd	$⊢ F \in (R GrpHom S) \to (F^{-1} \in (S GrpHom R) \leftrightarrow F : B \underset{1-1 onto}{⟶} C)$
12	9 11	syl	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (F^{-1} \in (S GrpHom R) \leftrightarrow F : B \underset{1-1 onto}{⟶} C)$
13	7 12	mpbird	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} \in (S GrpHom R)$
14		eqidd	$⊢ F \in (R RingHom S) \to F = F$
15		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
16	15 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
17	16	a1i	$⊢ F \in (R RingHom S) \to B = {Base}_{{mulGrp}_{R}}$
18		eqid	$⊢ {mulGrp}_{S} = {mulGrp}_{S}$
19	18 2	mgpbas	$⊢ C = {Base}_{{mulGrp}_{S}}$
20	19	a1i	$⊢ F \in (R RingHom S) \to C = {Base}_{{mulGrp}_{S}}$
21	14 17 20	f1oeq123d	$⊢ F \in (R RingHom S) \to (F : B \underset{1-1 onto}{⟶} C \leftrightarrow F : {Base}_{{mulGrp}_{R}} \underset{1-1 onto}{⟶} {Base}_{{mulGrp}_{S}})$
22	21	biimpa	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F : {Base}_{{mulGrp}_{R}} \underset{1-1 onto}{⟶} {Base}_{{mulGrp}_{S}}$
23	15 18	rhmmhm	$⊢ F \in (R RingHom S) \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})$
24	23	adantr	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F \in ({mulGrp}_{R} MndHom {mulGrp}_{S})$
25		eqid	$⊢ {Base}_{{mulGrp}_{R}} = {Base}_{{mulGrp}_{R}}$
26		eqid	$⊢ {Base}_{{mulGrp}_{S}} = {Base}_{{mulGrp}_{S}}$
27	25 26	mhmf1o	$⊢ F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}) \to (F : {Base}_{{mulGrp}_{R}} \underset{1-1 onto}{⟶} {Base}_{{mulGrp}_{S}} \leftrightarrow F^{-1} \in ({mulGrp}_{S} MndHom {mulGrp}_{R}))$
28	27	bicomd	$⊢ F \in ({mulGrp}_{R} MndHom {mulGrp}_{S}) \to (F^{-1} \in ({mulGrp}_{S} MndHom {mulGrp}_{R}) \leftrightarrow F : {Base}_{{mulGrp}_{R}} \underset{1-1 onto}{⟶} {Base}_{{mulGrp}_{S}})$
29	24 28	syl	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (F^{-1} \in ({mulGrp}_{S} MndHom {mulGrp}_{R}) \leftrightarrow F : {Base}_{{mulGrp}_{R}} \underset{1-1 onto}{⟶} {Base}_{{mulGrp}_{S}})$
30	22 29	mpbird	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} \in ({mulGrp}_{S} MndHom {mulGrp}_{R})$
31	13 30	jca	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to (F^{-1} \in (S GrpHom R) \land F^{-1} \in ({mulGrp}_{S} MndHom {mulGrp}_{R}))$
32	18 15	isrhm	$⊢ F^{-1} \in (S RingHom R) \leftrightarrow ((S \in Ring \land R \in Ring) \land (F^{-1} \in (S GrpHom R) \land F^{-1} \in ({mulGrp}_{S} MndHom {mulGrp}_{R})))$
33	6 31 32	sylanbrc	$⊢ (F \in (R RingHom S) \land F : B \underset{1-1 onto}{⟶} C) \to F^{-1} \in (S RingHom R)$
34	1 2	rhmf	$⊢ F \in (R RingHom S) \to F : B ⟶ C$
35	34	adantr	$⊢ (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)) \to F : B ⟶ C$
36	35	ffnd	$⊢ (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)) \to F Fn B$
37	2 1	rhmf	$⊢ F^{-1} \in (S RingHom R) \to F^{-1} : C ⟶ B$
38	37	adantl	$⊢ (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)) \to F^{-1} : C ⟶ B$
39	38	ffnd	$⊢ (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)) \to F^{-1} Fn C$
40		dff1o4	$⊢ F : B \underset{1-1 onto}{⟶} C \leftrightarrow (F Fn B \land F^{-1} Fn C)$
41	36 39 40	sylanbrc	$⊢ (F \in (R RingHom S) \land F^{-1} \in (S RingHom R)) \to F : B \underset{1-1 onto}{⟶} C$
42	33 41	impbida	$⊢ F \in (R RingHom S) \to (F : B \underset{1-1 onto}{⟶} C \leftrightarrow F^{-1} \in (S RingHom R))$

Metamath Proof Explorer

Theorem rhmf1o

Proof