rngcsect

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

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		rngcsect.e	$⊢ E = {Base}_{X}$
7		rngcsect.n	$⊢ S = Sect (C)$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10		eqid	$⊢ Id (C) = Id (C)$
11	1	rngccat	$⊢ 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	rngchom	$⊢ φ \to X Hom (C) Y = X RngHomo Y$
15	14	eleq2d	$⊢ φ \to (F \in (X Hom (C) Y) \leftrightarrow F \in (X RngHomo Y))$
16	1 2 3 8 5 4	rngchom	$⊢ φ \to Y Hom (C) X = Y RngHomo X$
17	16	eleq2d	$⊢ φ \to (G \in (Y Hom (C) X) \leftrightarrow G \in (Y RngHomo X))$
18	15 17	anbi12d	$⊢ φ \to ((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \leftrightarrow (F \in (X RngHomo Y) \land G \in (Y RngHomo 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 RngHomo Y) \land G \in (Y RngHomo X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
20	3	adantr	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to U \in V$
21	4	adantr	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to X \in B$
22	1 2 3	rngcbas	$⊢ φ \to B = U \cap Rng$
23	22	eleq2d	$⊢ φ \to (X \in B \leftrightarrow X \in (U \cap Rng))$
24		inss1	$⊢ U \cap Rng \subseteq U$
25	24	a1i	$⊢ φ \to U \cap Rng \subseteq U$
26	25	sseld	$⊢ φ \to (X \in (U \cap Rng) \to X \in U)$
27	23 26	sylbid	$⊢ φ \to (X \in B \to X \in U)$
28	27	adantr	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to (X \in B \to X \in U)$
29	21 28	mpd	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to X \in U$
30	5	adantr	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to Y \in B$
31	22	eleq2d	$⊢ φ \to (Y \in B \leftrightarrow Y \in (U \cap Rng))$
32	25	sseld	$⊢ φ \to (Y \in (U \cap Rng) \to Y \in U)$
33	31 32	sylbid	$⊢ φ \to (Y \in B \to Y \in U)$
34	33	adantr	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to (Y \in B \to Y \in U)$
35	30 34	mpd	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to Y \in U$
36		eqid	$⊢ {Base}_{X} = {Base}_{X}$
37		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
38	36 37	rnghmf	$⊢ F \in (X RngHomo Y) \to F : {Base}_{X} ⟶ {Base}_{Y}$
39	38	adantr	$⊢ (F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \to F : {Base}_{X} ⟶ {Base}_{Y}$
40	39	adantl	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to F : {Base}_{X} ⟶ {Base}_{Y}$
41	37 36	rnghmf	$⊢ G \in (Y RngHomo X) \to G : {Base}_{Y} ⟶ {Base}_{X}$
42	41	adantl	$⊢ (F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \to G : {Base}_{Y} ⟶ {Base}_{X}$
43	42	adantl	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to G : {Base}_{Y} ⟶ {Base}_{X}$
44	1 20 9 29 35 29 40 43	rngcco	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to G (⟨X, Y⟩ comp (C) X) F = G \circ F$
45	1 2 10 3 4 6	rngcid	$⊢ φ \to Id (C) (X) = {I ↾}_{E}$
46	45	adantr	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to Id (C) (X) = {I ↾}_{E}$
47	44 46	eqeq12d	$⊢ (φ \land (F \in (X RngHomo Y) \land G \in (Y RngHomo X))) \to (G (⟨X, Y⟩ comp (C) X) F = Id (C) (X) \leftrightarrow G \circ F = {I ↾}_{E})$
48	47	pm5.32da	$⊢ φ \to (((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{E}))$
49	19 48	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 RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{E}))$
50		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))$
51		df-3an	$⊢ (F \in (X RngHomo Y) \land G \in (Y RngHomo X) \land G \circ F = {I ↾}_{E}) \leftrightarrow ((F \in (X RngHomo Y) \land G \in (Y RngHomo X)) \land G \circ F = {I ↾}_{E})$
52	49 50 51	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 RngHomo Y) \land G \in (Y RngHomo X) \land G \circ F = {I ↾}_{E}))$
53	13 52	bitrd	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X RngHomo Y) \land G \in (Y RngHomo X) \land G \circ F = {I ↾}_{E}))$

Metamath Proof Explorer

Theorem rngcsect

Proof