dfrngc2

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

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

Proof

Step	Hyp	Ref	Expression
1		dfrngc2.c	$⊢ C = RngCat (U)$
2		dfrngc2.u	$⊢ φ \to U \in V$
3		dfrngc2.b	$⊢ φ \to B = U \cap Rng$
4		dfrngc2.h	$⊢ φ \to H = {RngHomo ↾}_{(B \times B)}$
5		dfrngc2.o	$⊢ φ \to \underset{˙}{\cdot} = comp (ExtStrCat (U))$
6	1 2 3 4	rngcval	$⊢ φ \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 Rng \in V$
10	2 9	syl	$⊢ φ \to U \cap Rng \in V$
11	3 10	eqeltrd	$⊢ φ \to B \in V$
12	3 4	rnghmresfn	$⊢ φ \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		rnghmfn	$⊢ RngHomo Fn (Rng \times Rng)$
25		fnfun	$⊢ RngHomo Fn (Rng \times Rng) \to Fun RngHomo$
26	24 25	mp1i	$⊢ φ \to Fun RngHomo$
27		sqxpexg	$⊢ B \in V \to B \times B \in V$
28	11 27	syl	$⊢ φ \to B \times B \in V$
29		resfunexg	$⊢ (Fun RngHomo \land B \times B \in V) \to {RngHomo ↾}_{(B \times B)} \in V$
30	26 28 29	syl2anc	$⊢ φ \to {RngHomo ↾}_{(B \times B)} \in V$
31	4 30	eqeltrd	$⊢ φ \to H \in V$
32		inss1	$⊢ U \cap Rng \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 dfrngc2

Proof