dfringc2

Description: Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020)

	Ref	Expression
Hypotheses	dfringc2.c	$⊢ C = RingCat (U)$
	dfringc2.u	$⊢ φ \to U \in V$
	dfringc2.b	$⊢ φ \to B = U \cap Ring$
	dfringc2.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
	dfringc2.o	$⊢ φ \to \underset{˙}{\cdot} = comp (ExtStrCat (U))$
Assertion	dfringc2	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		dfringc2.c	$⊢ C = RingCat (U)$
2		dfringc2.u	$⊢ φ \to U \in V$
3		dfringc2.b	$⊢ φ \to B = U \cap Ring$
4		dfringc2.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
5		dfringc2.o	$⊢ φ \to \underset{˙}{\cdot} = comp (ExtStrCat (U))$
6	1 2 3 4	ringcval	$⊢ φ \to C = ExtStrCat (U) ↾_{cat} H$
7		eqid	$⊢ ExtStrCat (U) ↾_{cat} H = ExtStrCat (U) ↾_{cat} H$
8		fvexd	$⊢ φ \to ExtStrCat (U) \in V$
9		inex1g	$⊢ U \in V \to U \cap Ring \in V$
10	2 9	syl	$⊢ φ \to U \cap Ring \in V$
11	3 10	eqeltrd	$⊢ φ \to B \in V$
12	3 4	rhmresfn	$⊢ φ \to H Fn (B \times B)$
13	7 8 11 12	rescval2	$⊢ φ \to ExtStrCat (U) ↾_{cat} H = (ExtStrCat (U) ↾_{𝑠} B) sSet ⟨Hom (ndx), H⟩$
14		eqid	$⊢ ExtStrCat (U) = ExtStrCat (U)$
15		eqidd	$⊢ φ \to (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}}) = (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}})$
16		eqid	$⊢ comp (ExtStrCat (U)) = comp (ExtStrCat (U))$
17	14 2 16	estrccofval	$⊢ φ \to comp (ExtStrCat (U)) = (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))$
18	5 17	eqtrd	$⊢ φ \to \underset{˙}{\cdot} = (v \in (U \times U), z \in U ⟼ (g \in ({Base}_{z}^{{Base}_{2^{nd} (v)}}), f \in ({Base}_{2^{nd} (v)}^{{Base}_{1^{st} (v)}}) ⟼ g \circ f))$
19	14 2 15 18	estrcval	$⊢ φ \to ExtStrCat (U) = \{⟨{Base}_{ndx}, U⟩, ⟨Hom (ndx), (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}})⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
20		mpoexga	$⊢ (U \in V \land U \in V) \to (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}}) \in V$
21	2 2 20	syl2anc	$⊢ φ \to (x \in U, y \in U ⟼ {Base}_{y}^{{Base}_{x}}) \in V$
22		fvexd	$⊢ φ \to comp (ExtStrCat (U)) \in V$
23	5 22	eqeltrd	$⊢ φ \to \underset{˙}{\cdot} \in V$
24		rhmfn	$⊢ RingHom Fn (Ring \times Ring)$
25		fnfun	$⊢ RingHom Fn (Ring \times Ring) \to Fun RingHom$
26	24 25	mp1i	$⊢ φ \to Fun RingHom$
27		sqxpexg	$⊢ B \in V \to B \times B \in V$
28	11 27	syl	$⊢ φ \to B \times B \in V$
29		resfunexg	$⊢ (Fun RingHom \land B \times B \in V) \to {RingHom ↾}_{(B \times B)} \in V$
30	26 28 29	syl2anc	$⊢ φ \to {RingHom ↾}_{(B \times B)} \in V$
31	4 30	eqeltrd	$⊢ φ \to H \in V$
32		inss1	$⊢ U \cap Ring \subseteq U$
33	3 32	eqsstrdi	$⊢ φ \to B \subseteq U$
34	19 2 21 23 31 33	estrres	$⊢ φ \to (ExtStrCat (U) ↾_{𝑠} B) sSet ⟨Hom (ndx), H⟩ = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$
35	6 13 34	3eqtrd	$⊢ φ \to C = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), \underset{˙}{\cdot}⟩\}$

Metamath Proof Explorer

Theorem dfringc2

Proof