ringcsect

Description: A section in the category of unital rings, written out. (Contributed by AV, 14-Feb-2020)

	Ref	Expression
Hypotheses	ringcsect.c	$⊢ C = RingCat (U)$
	ringcsect.b	$⊢ B = {Base}_{C}$
	ringcsect.u	$⊢ φ \to U \in V$
	ringcsect.x	$⊢ φ \to X \in B$
	ringcsect.y	$⊢ φ \to Y \in B$
	ringcsect.e	$⊢ E = {Base}_{X}$
	ringcsect.n	$⊢ S = Sect (C)$
Assertion	ringcsect	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X RingHom Y) \land G \in (Y RingHom X) \land G \circ F = {I ↾}_{E}))$

Proof

Step	Hyp	Ref	Expression
1		ringcsect.c	$⊢ C = RingCat (U)$
2		ringcsect.b	$⊢ B = {Base}_{C}$
3		ringcsect.u	$⊢ φ \to U \in V$
4		ringcsect.x	$⊢ φ \to X \in B$
5		ringcsect.y	$⊢ φ \to Y \in B$
6		ringcsect.e	$⊢ E = {Base}_{X}$
7		ringcsect.n	$⊢ S = Sect (C)$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10		eqid	$⊢ Id (C) = Id (C)$
11	1	ringccat	$⊢ 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	ringchom	$⊢ φ \to X Hom (C) Y = X RingHom Y$
15	14	eleq2d	$⊢ φ \to (F \in (X Hom (C) Y) \leftrightarrow F \in (X RingHom Y))$
16	1 2 3 8 5 4	ringchom	$⊢ φ \to Y Hom (C) X = Y RingHom X$
17	16	eleq2d	$⊢ φ \to (G \in (Y Hom (C) X) \leftrightarrow G \in (Y RingHom X))$
18	15 17	anbi12d	$⊢ φ \to ((F \in (X Hom (C) Y) \land G \in (Y Hom (C) X)) \leftrightarrow (F \in (X RingHom Y) \land G \in (Y RingHom 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 RingHom Y) \land G \in (Y RingHom X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
20	3	adantr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to U \in V$
21	4	adantr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to X \in B$
22	1 2 3	ringcbas	$⊢ φ \to B = U \cap Ring$
23	22	eleq2d	$⊢ φ \to (X \in B \leftrightarrow X \in (U \cap Ring))$
24		inss1	$⊢ U \cap Ring \subseteq U$
25	24	a1i	$⊢ φ \to U \cap Ring \subseteq U$
26	25	sseld	$⊢ φ \to (X \in (U \cap Ring) \to X \in U)$
27	23 26	sylbid	$⊢ φ \to (X \in B \to X \in U)$
28	27	adantr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to (X \in B \to X \in U)$
29	21 28	mpd	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to X \in U$
30	5	adantr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to Y \in B$
31	22	eleq2d	$⊢ φ \to (Y \in B \leftrightarrow Y \in (U \cap Ring))$
32	25	sseld	$⊢ φ \to (Y \in (U \cap Ring) \to Y \in U)$
33	31 32	sylbid	$⊢ φ \to (Y \in B \to Y \in U)$
34	33	adantr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to (Y \in B \to Y \in U)$
35	30 34	mpd	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to Y \in U$
36		eqid	$⊢ {Base}_{X} = {Base}_{X}$
37		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
38	36 37	rhmf	$⊢ F \in (X RingHom Y) \to F : {Base}_{X} ⟶ {Base}_{Y}$
39	38	adantr	$⊢ (F \in (X RingHom Y) \land G \in (Y RingHom X)) \to F : {Base}_{X} ⟶ {Base}_{Y}$
40	39	adantl	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to F : {Base}_{X} ⟶ {Base}_{Y}$
41	37 36	rhmf	$⊢ G \in (Y RingHom X) \to G : {Base}_{Y} ⟶ {Base}_{X}$
42	41	adantl	$⊢ (F \in (X RingHom Y) \land G \in (Y RingHom X)) \to G : {Base}_{Y} ⟶ {Base}_{X}$
43	42	adantl	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to G : {Base}_{Y} ⟶ {Base}_{X}$
44	1 20 9 29 35 29 40 43	ringcco	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to G (⟨X, Y⟩ comp (C) X) F = G \circ F$
45	1 2 10 3 4 6	ringcid	$⊢ φ \to Id (C) (X) = {I ↾}_{E}$
46	45	adantr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to Id (C) (X) = {I ↾}_{E}$
47	44 46	eqeq12d	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom 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 RingHom Y) \land G \in (Y RingHom X)) \land G (⟨X, Y⟩ comp (C) X) F = Id (C) (X)) \leftrightarrow ((F \in (X RingHom Y) \land G \in (Y RingHom 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 RingHom Y) \land G \in (Y RingHom 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 RingHom Y) \land G \in (Y RingHom X) \land G \circ F = {I ↾}_{E}) \leftrightarrow ((F \in (X RingHom Y) \land G \in (Y RingHom 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 RingHom Y) \land G \in (Y RingHom X) \land G \circ F = {I ↾}_{E}))$
53	13 52	bitrd	$⊢ φ \to (F (X S Y) G \leftrightarrow (F \in (X RingHom Y) \land G \in (Y RingHom X) \land G \circ F = {I ↾}_{E}))$

Metamath Proof Explorer

Theorem ringcsect

Proof