ringcinv

Description: An inverse in the category of unital rings is the converse operation. (Contributed by AV, 14-Feb-2020)

	Ref	Expression
Hypotheses	ringcsect.c	$⊢ C = RingCat (U)$
	ringcsect.b	$⊢ B = {Base}_{C}$
	ringcsect.u	$⊢ φ \to U \in V$
	ringcsect.x	$⊢ φ \to X \in B$
	ringcsect.y	$⊢ φ \to Y \in B$
	ringcinv.n	$⊢ N = Inv (C)$
Assertion	ringcinv	$⊢ φ \to (F (X N Y) G \leftrightarrow (F \in (X RingIso Y) \land G = F^{-1}))$

Proof

Step	Hyp	Ref	Expression
1		ringcsect.c	$⊢ C = RingCat (U)$
2		ringcsect.b	$⊢ B = {Base}_{C}$
3		ringcsect.u	$⊢ φ \to U \in V$
4		ringcsect.x	$⊢ φ \to X \in B$
5		ringcsect.y	$⊢ φ \to Y \in B$
6		ringcinv.n	$⊢ N = Inv (C)$
7	1	ringccat	$⊢ U \in V \to C \in Cat$
8	3 7	syl	$⊢ φ \to C \in Cat$
9		eqid	$⊢ Sect (C) = Sect (C)$
10	2 6 8 4 5 9	isinv	$⊢ φ \to (F (X N Y) G \leftrightarrow (F (X Sect (C) Y) G \land G (Y Sect (C) X) F))$
11		eqid	$⊢ {Base}_{X} = {Base}_{X}$
12	1 2 3 4 5 11 9	ringcsect	$⊢ φ \to (F (X Sect (C) Y) G \leftrightarrow (F \in (X RingHom Y) \land G \in (Y RingHom X) \land G \circ F = {I ↾}_{{Base}_{X}}))$
13		df-3an	$⊢ (F \in (X RingHom Y) \land G \in (Y RingHom X) \land G \circ F = {I ↾}_{{Base}_{X}}) \leftrightarrow ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}})$
14	12 13	bitrdi	$⊢ φ \to (F (X Sect (C) Y) G \leftrightarrow ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}))$
15		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
16	1 2 3 5 4 15 9	ringcsect	$⊢ φ \to (G (Y Sect (C) X) F \leftrightarrow (G \in (Y RingHom X) \land F \in (X RingHom Y) \land F \circ G = {I ↾}_{{Base}_{Y}}))$
17		3ancoma	$⊢ (G \in (Y RingHom X) \land F \in (X RingHom Y) \land F \circ G = {I ↾}_{{Base}_{Y}}) \leftrightarrow (F \in (X RingHom Y) \land G \in (Y RingHom X) \land F \circ G = {I ↾}_{{Base}_{Y}})$
18		df-3an	$⊢ (F \in (X RingHom Y) \land G \in (Y RingHom X) \land F \circ G = {I ↾}_{{Base}_{Y}}) \leftrightarrow ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land F \circ G = {I ↾}_{{Base}_{Y}})$
19	17 18	bitri	$⊢ (G \in (Y RingHom X) \land F \in (X RingHom Y) \land F \circ G = {I ↾}_{{Base}_{Y}}) \leftrightarrow ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land F \circ G = {I ↾}_{{Base}_{Y}})$
20	16 19	bitrdi	$⊢ φ \to (G (Y Sect (C) X) F \leftrightarrow ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land F \circ G = {I ↾}_{{Base}_{Y}}))$
21	14 20	anbi12d	$⊢ φ \to ((F (X Sect (C) Y) G \land G (Y Sect (C) X) F) \leftrightarrow (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land F \circ G = {I ↾}_{{Base}_{Y}})))$
22		anandi	$⊢ (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land F \circ G = {I ↾}_{{Base}_{Y}})) \leftrightarrow ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))$
23	21 22	bitrdi	$⊢ φ \to ((F (X Sect (C) Y) G \land G (Y Sect (C) X) F) \leftrightarrow ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})))$
24		simplrl	$⊢ ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})) \to F \in (X RingHom Y)$
25	24	adantl	$⊢ (φ \land ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to F \in (X RingHom Y)$
26	11 15	rhmf	$⊢ F \in (X RingHom Y) \to F : {Base}_{X} ⟶ {Base}_{Y}$
27	15 11	rhmf	$⊢ G \in (Y RingHom X) \to G : {Base}_{Y} ⟶ {Base}_{X}$
28	26 27	anim12i	$⊢ (F \in (X RingHom Y) \land G \in (Y RingHom X)) \to (F : {Base}_{X} ⟶ {Base}_{Y} \land G : {Base}_{Y} ⟶ {Base}_{X})$
29	28	ad2antlr	$⊢ ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})) \to (F : {Base}_{X} ⟶ {Base}_{Y} \land G : {Base}_{Y} ⟶ {Base}_{X})$
30		simpr	$⊢ (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}) \to F \circ G = {I ↾}_{{Base}_{Y}}$
31	30	adantl	$⊢ ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})) \to F \circ G = {I ↾}_{{Base}_{Y}}$
32		simpr	$⊢ ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \to G \circ F = {I ↾}_{{Base}_{X}}$
33	32	ad2antrl	$⊢ ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})) \to G \circ F = {I ↾}_{{Base}_{X}}$
34	29 31 33	jca32	$⊢ ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})) \to ((F : {Base}_{X} ⟶ {Base}_{Y} \land G : {Base}_{Y} ⟶ {Base}_{X}) \land (F \circ G = {I ↾}_{{Base}_{Y}} \land G \circ F = {I ↾}_{{Base}_{X}}))$
35	34	adantl	$⊢ (φ \land ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to ((F : {Base}_{X} ⟶ {Base}_{Y} \land G : {Base}_{Y} ⟶ {Base}_{X}) \land (F \circ G = {I ↾}_{{Base}_{Y}} \land G \circ F = {I ↾}_{{Base}_{X}}))$
36		fcof1o	$⊢ ((F : {Base}_{X} ⟶ {Base}_{Y} \land G : {Base}_{Y} ⟶ {Base}_{X}) \land (F \circ G = {I ↾}_{{Base}_{Y}} \land G \circ F = {I ↾}_{{Base}_{X}})) \to (F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \land F^{-1} = G)$
37		eqcom	$⊢ F^{-1} = G \leftrightarrow G = F^{-1}$
38	37	anbi2i	$⊢ (F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \land F^{-1} = G) \leftrightarrow (F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \land G = F^{-1})$
39	36 38	sylib	$⊢ ((F : {Base}_{X} ⟶ {Base}_{Y} \land G : {Base}_{Y} ⟶ {Base}_{X}) \land (F \circ G = {I ↾}_{{Base}_{Y}} \land G \circ F = {I ↾}_{{Base}_{X}})) \to (F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \land G = F^{-1})$
40	35 39	syl	$⊢ (φ \land ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to (F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \land G = F^{-1})$
41		anass	$⊢ ((F \in (X RingHom Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}) \land G = F^{-1}) \leftrightarrow (F \in (X RingHom Y) \land (F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \land G = F^{-1}))$
42	25 40 41	sylanbrc	$⊢ (φ \land ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to ((F \in (X RingHom Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}) \land G = F^{-1})$
43	11 15	isrim	$⊢ F \in (X RingIso Y) \leftrightarrow (F \in (X RingHom Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y})$
44	43	a1i	$⊢ φ \to (F \in (X RingIso Y) \leftrightarrow (F \in (X RingHom Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}))$
45	44	anbi1d	$⊢ φ \to ((F \in (X RingIso Y) \land G = F^{-1}) \leftrightarrow ((F \in (X RingHom Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}) \land G = F^{-1}))$
46	45	adantr	$⊢ (φ \land ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to ((F \in (X RingIso Y) \land G = F^{-1}) \leftrightarrow ((F \in (X RingHom Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}) \land G = F^{-1}))$
47	42 46	mpbird	$⊢ (φ \land ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to (F \in (X RingIso Y) \land G = F^{-1})$
48		rimrhm	$⊢ F \in (X RingIso Y) \to F \in (X RingHom Y)$
49	48	ad2antrl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F \in (X RingHom Y)$
50		isrim0	$⊢ F \in (X RingIso Y) \leftrightarrow (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X))$
51	50	simprbi	$⊢ F \in (X RingIso Y) \to F^{-1} \in (Y RingHom X)$
52		eleq1	$⊢ G = F^{-1} \to (G \in (Y RingHom X) \leftrightarrow F^{-1} \in (Y RingHom X))$
53	51 52	syl5ibrcom	$⊢ F \in (X RingIso Y) \to (G = F^{-1} \to G \in (Y RingHom X))$
54	53	imp	$⊢ (F \in (X RingIso Y) \land G = F^{-1}) \to G \in (Y RingHom X)$
55	54	adantl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to G \in (Y RingHom X)$
56		coeq1	$⊢ G = F^{-1} \to G \circ F = F^{-1} \circ F$
57	56	ad2antll	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to G \circ F = F^{-1} \circ F$
58	11 15	rimf1o	$⊢ F \in (X RingIso Y) \to F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}$
59	58	ad2antrl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}$
60		f1ococnv1	$⊢ F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \to F^{-1} \circ F = {I ↾}_{{Base}_{X}}$
61	59 60	syl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F^{-1} \circ F = {I ↾}_{{Base}_{X}}$
62	57 61	eqtrd	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to G \circ F = {I ↾}_{{Base}_{X}}$
63	49 55 62	jca31	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}})$
64	50	biimpi	$⊢ F \in (X RingIso Y) \to (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X))$
65	64	ad2antrl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X))$
66	52	ad2antll	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to (G \in (Y RingHom X) \leftrightarrow F^{-1} \in (Y RingHom X))$
67	66	anbi2d	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to ((F \in (X RingHom Y) \land G \in (Y RingHom X)) \leftrightarrow (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X)))$
68	65 67	mpbird	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to (F \in (X RingHom Y) \land G \in (Y RingHom X))$
69		coeq2	$⊢ G = F^{-1} \to F \circ G = F \circ F^{-1}$
70	69	ad2antll	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F \circ G = F \circ F^{-1}$
71		f1ococnv2	$⊢ F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \to F \circ F^{-1} = {I ↾}_{{Base}_{Y}}$
72	59 71	syl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F \circ F^{-1} = {I ↾}_{{Base}_{Y}}$
73	70 72	eqtrd	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F \circ G = {I ↾}_{{Base}_{Y}}$
74	68 62 73	jca31	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})$
75	63 68 74	jca31	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to ((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))$
76	47 75	impbida	$⊢ φ \to (((((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \land (((F \in (X RingHom Y) \land G \in (Y RingHom X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})) \leftrightarrow (F \in (X RingIso Y) \land G = F^{-1}))$
77	10 23 76	3bitrd	$⊢ φ \to (F (X N Y) G \leftrightarrow (F \in (X RingIso Y) \land G = F^{-1}))$

Metamath Proof Explorer

Theorem ringcinv

Proof