ringcsectALTV

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

	Ref	Expression
Hypotheses	ringcsectALTV.c	$⊢ C = RingCatALTV (U)$
	ringcsectALTV.b	$⊢ B = {Base}_{C}$
	ringcsectALTV.u	$⊢ φ \to U \in V$
	ringcsectALTV.x	$⊢ φ \to X \in B$
	ringcsectALTV.y	$⊢ φ \to Y \in B$
	ringcsectALTV.e	$⊢ E = {Base}_{X}$
	ringcsectALTV.n	$⊢ S = Sect (C)$
Assertion	ringcsectALTV	$⊢ φ \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		ringcsectALTV.c	$⊢ C = RingCatALTV (U)$
2		ringcsectALTV.b	$⊢ B = {Base}_{C}$
3		ringcsectALTV.u	$⊢ φ \to U \in V$
4		ringcsectALTV.x	$⊢ φ \to X \in B$
5		ringcsectALTV.y	$⊢ φ \to Y \in B$
6		ringcsectALTV.e	$⊢ E = {Base}_{X}$
7		ringcsectALTV.n	$⊢ S = Sect (C)$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10		eqid	$⊢ Id (C) = Id (C)$
11	1	ringccatALTV	$⊢ 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	ringchomALTV	$⊢ φ \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	ringchomALTV	$⊢ φ \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	5	adantr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to Y \in B$
23		simprl	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to F \in (X RingHom Y)$
24		simprr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to G \in (Y RingHom X)$
25	1 2 20 9 21 22 21 23 24	ringccoALTV	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to G (⟨X, Y⟩ comp (C) X) F = G \circ F$
26	1 2 10 3 4 6	ringcidALTV	$⊢ φ \to Id (C) (X) = {I ↾}_{E}$
27	26	adantr	$⊢ (φ \land (F \in (X RingHom Y) \land G \in (Y RingHom X))) \to Id (C) (X) = {I ↾}_{E}$
28	25 27	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})$
29	28	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}))$
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 RingHom Y) \land G \in (Y RingHom 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 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})$
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 RingHom Y) \land G \in (Y RingHom X) \land G \circ F = {I ↾}_{E}))$
34	13 33	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 ringcsectALTV

Proof