rngcisoALTV

Description: An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngcsectALTV.c	$⊢ C = RngCatALTV (U)$
	rngcsectALTV.b	$⊢ B = {Base}_{C}$
	rngcsectALTV.u	$⊢ φ \to U \in V$
	rngcsectALTV.x	$⊢ φ \to X \in B$
	rngcsectALTV.y	$⊢ φ \to Y \in B$
	rngcisoALTV.n	$⊢ I = Iso (C)$
Assertion	rngcisoALTV	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in (X RngIsom Y))$

Proof

Step	Hyp	Ref	Expression
1		rngcsectALTV.c	$⊢ C = RngCatALTV (U)$
2		rngcsectALTV.b	$⊢ B = {Base}_{C}$
3		rngcsectALTV.u	$⊢ φ \to U \in V$
4		rngcsectALTV.x	$⊢ φ \to X \in B$
5		rngcsectALTV.y	$⊢ φ \to Y \in B$
6		rngcisoALTV.n	$⊢ I = Iso (C)$
7		eqid	$⊢ Inv (C) = Inv (C)$
8	1	rngccatALTV	$⊢ U \in V \to C \in Cat$
9	3 8	syl	$⊢ φ \to C \in Cat$
10	2 7 9 4 5 6	isoval	$⊢ φ \to X I Y = dom (X Inv (C) Y)$
11	10	eleq2d	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in dom (X Inv (C) Y))$
12	2 7 9 4 5	invfun	$⊢ φ \to Fun (X Inv (C) Y)$
13		funfvbrb	$⊢ Fun (X Inv (C) Y) \to (F \in dom (X Inv (C) Y) \leftrightarrow F (X Inv (C) Y) (X Inv (C) Y) (F))$
14	12 13	syl	$⊢ φ \to (F \in dom (X Inv (C) Y) \leftrightarrow F (X Inv (C) Y) (X Inv (C) Y) (F))$
15	1 2 3 4 5 7	rngcinvALTV	$⊢ φ \to (F (X Inv (C) Y) (X Inv (C) Y) (F) \leftrightarrow (F \in (X RngIsom Y) \land (X Inv (C) Y) (F) = F^{-1}))$
16		simpl	$⊢ (F \in (X RngIsom Y) \land (X Inv (C) Y) (F) = F^{-1}) \to F \in (X RngIsom Y)$
17	15 16	syl6bi	$⊢ φ \to (F (X Inv (C) Y) (X Inv (C) Y) (F) \to F \in (X RngIsom Y))$
18	14 17	sylbid	$⊢ φ \to (F \in dom (X Inv (C) Y) \to F \in (X RngIsom Y))$
19		eqid	$⊢ F^{-1} = F^{-1}$
20	1 2 3 4 5 7	rngcinvALTV	$⊢ φ \to (F (X Inv (C) Y) F^{-1} \leftrightarrow (F \in (X RngIsom Y) \land F^{-1} = F^{-1}))$
21		funrel	$⊢ Fun (X Inv (C) Y) \to Rel (X Inv (C) Y)$
22	12 21	syl	$⊢ φ \to Rel (X Inv (C) Y)$
23		releldm	$⊢ (Rel (X Inv (C) Y) \land F (X Inv (C) Y) F^{-1}) \to F \in dom (X Inv (C) Y)$
24	23	ex	$⊢ Rel (X Inv (C) Y) \to (F (X Inv (C) Y) F^{-1} \to F \in dom (X Inv (C) Y))$
25	22 24	syl	$⊢ φ \to (F (X Inv (C) Y) F^{-1} \to F \in dom (X Inv (C) Y))$
26	20 25	sylbird	$⊢ φ \to ((F \in (X RngIsom Y) \land F^{-1} = F^{-1}) \to F \in dom (X Inv (C) Y))$
27	19 26	mpan2i	$⊢ φ \to (F \in (X RngIsom Y) \to F \in dom (X Inv (C) Y))$
28	18 27	impbid	$⊢ φ \to (F \in dom (X Inv (C) Y) \leftrightarrow F \in (X RngIsom Y))$
29	11 28	bitrd	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in (X RngIsom Y))$

Metamath Proof Explorer

Theorem rngcisoALTV

Proof