rngcsectALTV

Description: A section in the category of non-unital rings, written out. (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$
	rngcsectALTV.e	$⊢ E = {Base}_{X}$
	rngcsectALTV.n	$⊢ S = Sect (C)$
Assertion	rngcsectALTV	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X RngHom Y) \land G \in (Y RngHom X) \land G \circ F = {I ↾}_{E}))$

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		rngcsectALTV.e	$⊢ E = {Base}_{X}$
7		rngcsectALTV.n	$⊢ S = Sect (C)$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10		eqid	$⊢ Id (C) = Id (C)$
11	1	rngccatALTV	$⊢ U \in V \to C \in Cat$
12	3 11	syl	$⊢ φ \to C \in Cat$
13	2 8 9 10 7 12 4 5	issect	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X Hom (C) Y) \land G \in (Y Hom (C) X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
14	1 2 3 8 4 5	rngchomALTV	$⊢ φ \to X Hom (C) Y = X RngHom Y$
15	14	eleq2d	$⊢ φ \to (F \in (X Hom (C) Y) \leftrightarrow F \in (X RngHom Y))$
16	1 2 3 8 5 4	rngchomALTV	$⊢ φ \to Y Hom (C) X = Y RngHom X$
17	16	eleq2d	$⊢ φ \to (G \in (Y Hom (C) X) \leftrightarrow G \in (Y RngHom X))$
18	15 17	anbi12d	$⊢ φ \to ((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \leftrightarrow (F \in (X RngHom Y) \land G \in (Y RngHom X)))$
19	18	anbi1d	$⊢ φ \to (((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X RngHom Y) \land G \in (Y RngHom X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
20	3	adantr	$⊢ (φ \land (F \in (X RngHom Y) \land G \in (Y RngHom X))) \to U \in V$
21	4	adantr	$⊢ (φ \land (F \in (X RngHom Y) \land G \in (Y RngHom X))) \to X \in B$
22	5	adantr	$⊢ (φ \land (F \in (X RngHom Y) \land G \in (Y RngHom X))) \to Y \in B$
23		simprl	$⊢ (φ \land (F \in (X RngHom Y) \land G \in (Y RngHom X))) \to F \in (X RngHom Y)$
24		simprr	$⊢ (φ \land (F \in (X RngHom Y) \land G \in (Y RngHom X))) \to G \in (Y RngHom X)$
25	1 2 20 9 21 22 21 23 24	rngccoALTV	$⊢ (φ \land (F \in (X RngHom Y) \land G \in (Y RngHom X))) \to G (⟨X, Y⟩ comp (C) X) F = G \circ F$
26	1 2 10 3 4 6	rngcidALTV	$⊢ φ \to Id (C) (X) = {I ↾}_{E}$
27	26	adantr	$⊢ (φ \land (F \in (X RngHom Y) \land G \in (Y RngHom X))) \to Id (C) (X) = {I ↾}_{E}$
28	25 27	eqeq12d	$⊢ (φ \land (F \in (X RngHom Y) \land G \in (Y RngHom X))) \to (G (⟨X, Y⟩ comp (C) X) F = Id (C) (X) \leftrightarrow G \circ F = {I ↾}_{E})$
29	28	pm5.32da	$⊢ φ \to (((F \in (X RngHom Y) \land G \in (Y RngHom X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X RngHom Y) \land G \in (Y RngHom X)) \land G \circ F = {I ↾}_{E}))$
30	19 29	bitrd	$⊢ φ \to (((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X RngHom Y) \land G \in (Y RngHom X)) \land G \circ F = {I ↾}_{E}))$
31		df-3an	$⊢ (F \in (X Hom (C) Y) \land G \in (Y Hom (C) X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X))$
32		df-3an	$⊢ (F \in (X RngHom Y) \land G \in (Y RngHom X) \land G \circ F = {I ↾}_{E}) \leftrightarrow ((F \in (X RngHom Y) \land G \in (Y RngHom X)) \land G \circ F = {I ↾}_{E})$
33	30 31 32	3bitr4g	$⊢ φ \to ((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow (F \in (X RngHom Y) \land G \in (Y RngHom X) \land G \circ F = {I ↾}_{E}))$
34	13 33	bitrd	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X RngHom Y) \land G \in (Y RngHom X) \land G \circ F = {I ↾}_{E}))$

Metamath Proof Explorer

Theorem rngcsectALTV

Proof