rngcinv

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

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

Proof

Step	Hyp	Ref	Expression
1		rngcsect.c	$⊢ C = RngCat (U)$
2		rngcsect.b	$⊢ B = {Base}_{C}$
3		rngcsect.u	$⊢ φ \to U \in V$
4		rngcsect.x	$⊢ φ \to X \in B$
5		rngcsect.y	$⊢ φ \to Y \in B$
6		rngcinv.n	$⊢ N = Inv (C)$
7	1	rngccat	$⊢ 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	rngcsect	$⊢ φ \to (F (X Sect (C) Y) G \leftrightarrow (F \in (X RngHomo Y) \land G \in (Y RngHomo X) \land G \circ F = {I ↾}_{{Base}_{X}}))$
13		df-3an	$⊢ (F \in (X RngHomo Y) \land G \in (Y RngHomo X) \land G \circ F = {I ↾}_{{Base}_{X}}) \leftrightarrow ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}})$
14	12 13	bitrdi	$⊢ φ \to (F (X Sect (C) Y) G \leftrightarrow ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}))$
15		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
16	1 2 3 5 4 15 9	rngcsect	$⊢ φ \to (G (Y Sect (C) X) F \leftrightarrow (G \in (Y RngHomo X) \land F \in (X RngHomo Y) \land F \circ G = {I ↾}_{{Base}_{Y}}))$
17		3ancoma	$⊢ (G \in (Y RngHomo X) \land F \in (X RngHomo Y) \land F \circ G = {I ↾}_{{Base}_{Y}}) \leftrightarrow (F \in (X RngHomo Y) \land G \in (Y RngHomo X) \land F \circ G = {I ↾}_{{Base}_{Y}})$
18		df-3an	$⊢ (F \in (X RngHomo Y) \land G \in (Y RngHomo X) \land F \circ G = {I ↾}_{{Base}_{Y}}) \leftrightarrow ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land F \circ G = {I ↾}_{{Base}_{Y}})$
19	17 18	bitri	$⊢ (G \in (Y RngHomo X) \land F \in (X RngHomo Y) \land F \circ G = {I ↾}_{{Base}_{Y}}) \leftrightarrow ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land F \circ G = {I ↾}_{{Base}_{Y}})$
20	16 19	bitrdi	$⊢ φ \to (G (Y Sect (C) X) F \leftrightarrow ((F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land F \circ G = {I ↾}_{{Base}_{Y}})))$
22		anandi	$⊢ (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land F \circ G = {I ↾}_{{Base}_{Y}})) \leftrightarrow ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})))$
24		simplrl	$⊢ ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})) \to F \in (X RngHomo Y)$
25	24	adantl	$⊢ (φ \land ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to F \in (X RngHomo Y)$
26	11 15	rnghmf	$⊢ F \in (X RngHomo Y) \to F : {Base}_{X} ⟶ {Base}_{Y}$
27	15 11	rnghmf	$⊢ G \in (Y RngHomo X) \to G : {Base}_{Y} ⟶ {Base}_{X}$
28	26 27	anim12i	$⊢ (F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \to (F : {Base}_{X} ⟶ {Base}_{Y} \land G : {Base}_{Y} ⟶ {Base}_{X})$
29	28	ad2antlr	$⊢ ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \to G \circ F = {I ↾}_{{Base}_{X}}$
33	32	ad2antrl	$⊢ ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}) \land G = F^{-1}) \leftrightarrow (F \in (X RngHomo Y) \land (F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \land G = F^{-1}))$
42	25 40 41	sylanbrc	$⊢ (φ \land ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to ((F \in (X RngHomo Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}) \land G = F^{-1})$
43	11 15	isrngim	$⊢ (X \in B \land Y \in B) \to (F \in (X RngIsom Y) \leftrightarrow (F \in (X RngHomo Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}))$
44	4 5 43	syl2anc	$⊢ φ \to (F \in (X RngIsom Y) \leftrightarrow (F \in (X RngHomo Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}))$
45	44	anbi1d	$⊢ φ \to ((F \in (X RngIsom Y) \land G = F^{-1}) \leftrightarrow ((F \in (X RngHomo Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}) \land G = F^{-1}))$
46	45	adantr	$⊢ (φ \land ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to ((F \in (X RngIsom Y) \land G = F^{-1}) \leftrightarrow ((F \in (X RngHomo Y) \land F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}) \land G = F^{-1}))$
47	42 46	mpbird	$⊢ (φ \land ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))) \to (F \in (X RngIsom Y) \land G = F^{-1})$
48	11 15	rngimrnghm	$⊢ F \in (X RngIsom Y) \to F \in (X RngHomo Y)$
49	48	ad2antrl	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to F \in (X RngHomo Y)$
50		isrngisom	$⊢ (X \in B \land Y \in B) \to (F \in (X RngIsom Y) \leftrightarrow (F \in (X RngHomo Y) \land F^{-1} \in (Y RngHomo X)))$
51	4 5 50	syl2anc	$⊢ φ \to (F \in (X RngIsom Y) \leftrightarrow (F \in (X RngHomo Y) \land F^{-1} \in (Y RngHomo X)))$
52		eleq1	$⊢ F^{-1} = G \to (F^{-1} \in (Y RngHomo X) \leftrightarrow G \in (Y RngHomo X))$
53	52	eqcoms	$⊢ G = F^{-1} \to (F^{-1} \in (Y RngHomo X) \leftrightarrow G \in (Y RngHomo X))$
54	53	anbi2d	$⊢ G = F^{-1} \to ((F \in (X RngHomo Y) \land F^{-1} \in (Y RngHomo X)) \leftrightarrow (F \in (X RngHomo Y) \land G \in (Y RngHomo X)))$
55	51 54	sylan9bbr	$⊢ (G = F^{-1} \land φ) \to (F \in (X RngIsom Y) \leftrightarrow (F \in (X RngHomo Y) \land G \in (Y RngHomo X)))$
56		simpr	$⊢ (F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \to G \in (Y RngHomo X)$
57	55 56	syl6bi	$⊢ (G = F^{-1} \land φ) \to (F \in (X RngIsom Y) \to G \in (Y RngHomo X))$
58	57	com12	$⊢ F \in (X RngIsom Y) \to ((G = F^{-1} \land φ) \to G \in (Y RngHomo X))$
59	58	expdimp	$⊢ (F \in (X RngIsom Y) \land G = F^{-1}) \to (φ \to G \in (Y RngHomo X))$
60	59	impcom	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to G \in (Y RngHomo X)$
61		coeq1	$⊢ G = F^{-1} \to G \circ F = F^{-1} \circ F$
62	61	ad2antll	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to G \circ F = F^{-1} \circ F$
63	11 15	rngimf1o	$⊢ F \in (X RngIsom Y) \to F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}$
64	63	ad2antrl	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y}$
65		f1ococnv1	$⊢ F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \to F^{-1} \circ F = {I ↾}_{{Base}_{X}}$
66	64 65	syl	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to F^{-1} \circ F = {I ↾}_{{Base}_{X}}$
67	62 66	eqtrd	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to G \circ F = {I ↾}_{{Base}_{X}}$
68	49 60 67	jca31	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}})$
69	51	biimpcd	$⊢ F \in (X RngIsom Y) \to (φ \to (F \in (X RngHomo Y) \land F^{-1} \in (Y RngHomo X)))$
70	69	adantr	$⊢ (F \in (X RngIsom Y) \land G = F^{-1}) \to (φ \to (F \in (X RngHomo Y) \land F^{-1} \in (Y RngHomo X)))$
71	70	impcom	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to (F \in (X RngHomo Y) \land F^{-1} \in (Y RngHomo X))$
72		eleq1	$⊢ G = F^{-1} \to (G \in (Y RngHomo X) \leftrightarrow F^{-1} \in (Y RngHomo X))$
73	72	ad2antll	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to (G \in (Y RngHomo X) \leftrightarrow F^{-1} \in (Y RngHomo X))$
74	73	anbi2d	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \leftrightarrow (F \in (X RngHomo Y) \land F^{-1} \in (Y RngHomo X)))$
75	71 74	mpbird	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to (F \in (X RngHomo Y) \land G \in (Y RngHomo X))$
76		coeq2	$⊢ G = F^{-1} \to F \circ G = F \circ F^{-1}$
77	76	ad2antll	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to F \circ G = F \circ F^{-1}$
78		f1ococnv2	$⊢ F : {Base}_{X} \underset{1-1 onto}{⟶} {Base}_{Y} \to F \circ F^{-1} = {I ↾}_{{Base}_{Y}}$
79	64 78	syl	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to F \circ F^{-1} = {I ↾}_{{Base}_{Y}}$
80	77 79	eqtrd	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to F \circ G = {I ↾}_{{Base}_{Y}}$
81	75 67 80	jca31	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})$
82	68 75 81	jca31	$⊢ (φ \land (F \in (X RngIsom Y) \land G = F^{-1})) \to ((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}}))$
83	47 82	impbida	$⊢ φ \to (((((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \land (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{{Base}_{X}}) \land F \circ G = {I ↾}_{{Base}_{Y}})) \leftrightarrow (F \in (X RngIsom Y) \land G = F^{-1}))$
84	10 23 83	3bitrd	$⊢ φ \to (F (X N Y) G \leftrightarrow (F \in (X RngIsom Y) \land G = F^{-1}))$

Metamath Proof Explorer

Theorem rngcinv

Proof