ringcinvALTV

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

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

Proof

Step	Hyp	Ref	Expression
1		ringcsectALTV.c	$⊢ C = RingCatALTV (U)$
2		ringcsectALTV.b	$⊢ B = {Base}_{C}$
3		ringcsectALTV.u	$⊢ φ \to U \in V$
4		ringcsectALTV.x	$⊢ φ \to X \in B$
5		ringcsectALTV.y	$⊢ φ \to Y \in B$
6		ringcinvALTV.n	$⊢ N = Inv (C)$
7	1	ringccatALTV	$⊢ 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	ringcsectALTV	$⊢ φ \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	ringcsectALTV	$⊢ φ \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	31 33	jca	$⊢ ((((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}} \land G \circ F = {I ↾}_{{Base}_{X}})$
35	29 34	jca	$⊢ ((((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	35	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}}))$
37		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)$
38		eqcom	$⊢ F^{-1} = G \leftrightarrow G = F^{-1}$
39	38	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})$
40	37 39	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})$
41	36 40	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})$
42		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}))$
43	25 41 42	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})$
44	4 5	jca	$⊢ φ \to (X \in B \land Y \in B)$
45	11 15	isrim	$⊢ (X \in B \land Y \in B) \to (F \in (X RingIso Y) \leftrightarrow (F \in (X RingHom Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}))$
46	44 45	syl	$⊢ φ \to (F \in (X RingIso Y) \leftrightarrow (F \in (X RingHom Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}))$
47	46	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}))$
48	47	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}))$
49	43 48	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})$
50	11 15	rimrhm	$⊢ F \in (X RingIso Y) \to F \in (X RingHom Y)$
51	50	ad2antrl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F \in (X RingHom Y)$
52		isrim0	$⊢ (X \in B \land Y \in B) \to (F \in (X RingIso Y) \leftrightarrow (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X)))$
53	44 52	syl	$⊢ φ \to (F \in (X RingIso Y) \leftrightarrow (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X)))$
54		eleq1	$⊢ F^{-1} = G \to (F^{-1} \in (Y RingHom X) \leftrightarrow G \in (Y RingHom X))$
55	54	eqcoms	$⊢ G = F^{-1} \to (F^{-1} \in (Y RingHom X) \leftrightarrow G \in (Y RingHom X))$
56	55	anbi2d	$⊢ G = F^{-1} \to ((F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X)) \leftrightarrow (F \in (X RingHom Y) \land G \in (Y RingHom X)))$
57	53 56	sylan9bbr	$⊢ (G = F^{-1} \land φ) \to (F \in (X RingIso Y) \leftrightarrow (F \in (X RingHom Y) \land G \in (Y RingHom X)))$
58		simpr	$⊢ (F \in (X RingHom Y) \land G \in (Y RingHom X)) \to G \in (Y RingHom X)$
59	57 58	syl6bi	$⊢ (G = F^{-1} \land φ) \to (F \in (X RingIso Y) \to G \in (Y RingHom X))$
60	59	com12	$⊢ F \in (X RingIso Y) \to ((G = F^{-1} \land φ) \to G \in (Y RingHom X))$
61	60	expdimp	$⊢ (F \in (X RingIso Y) \land G = F^{-1}) \to (φ \to G \in (Y RingHom X))$
62	61	impcom	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to G \in (Y RingHom X)$
63		coeq1	$⊢ G = F^{-1} \to G \circ F = F^{-1} \circ F$
64	63	ad2antll	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to G \circ F = F^{-1} \circ F$
65	11 15	rimf1o	$⊢ F \in (X RingIso Y) \to F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}$
66	65	ad2antrl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}$
67		f1ococnv1	$⊢ F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \to F^{-1} \circ F = {I ↾}_{{Base}_{X}}$
68	66 67	syl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F^{-1} \circ F = {I ↾}_{{Base}_{X}}$
69	64 68	eqtrd	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to G \circ F = {I ↾}_{{Base}_{X}}$
70	51 62 69	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}})$
71	53	biimpcd	$⊢ F \in (X RingIso Y) \to (φ \to (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X)))$
72	71	adantr	$⊢ (F \in (X RingIso Y) \land G = F^{-1}) \to (φ \to (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X)))$
73	72	impcom	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to (F \in (X RingHom Y) \land F^{-1} \in (Y RingHom X))$
74		eleq1	$⊢ G = F^{-1} \to (G \in (Y RingHom X) \leftrightarrow F^{-1} \in (Y RingHom X))$
75	74	ad2antll	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to (G \in (Y RingHom X) \leftrightarrow F^{-1} \in (Y RingHom X))$
76	75	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)))$
77	73 76	mpbird	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to (F \in (X RingHom Y) \land G \in (Y RingHom X))$
78		coeq2	$⊢ G = F^{-1} \to F \circ G = F \circ F^{-1}$
79	78	ad2antll	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F \circ G = F \circ F^{-1}$
80		f1ococnv2	$⊢ F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \to F \circ F^{-1} = {I ↾}_{{Base}_{Y}}$
81	66 80	syl	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F \circ F^{-1} = {I ↾}_{{Base}_{Y}}$
82	79 81	eqtrd	$⊢ (φ \land (F \in (X RingIso Y) \land G = F^{-1})) \to F \circ G = {I ↾}_{{Base}_{Y}}$
83	77 69 82	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}})$
84	70 77 83	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}}))$
85	49 84	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}))$
86	10 23 85	3bitrd	$⊢ φ \to (F (X N Y) G \leftrightarrow (F \in (X RingIso Y) \land G = F^{-1}))$

Metamath Proof Explorer

Theorem ringcinvALTV

Proof