rngcresringcat

Description: The restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings. (Contributed by AV, 16-Mar-2020)

	Ref	Expression
Hypotheses	rhmsubcrngc.c	$⊢ C = RngCat (U)$
	rhmsubcrngc.u	$⊢ φ \to U \in V$
	rhmsubcrngc.b	$⊢ φ \to B = Ring \cap U$
	rhmsubcrngc.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
Assertion	rngcresringcat	$⊢ φ \to C ↾_{cat} H = RingCat (U)$

Proof

Step	Hyp	Ref	Expression
1		rhmsubcrngc.c	$⊢ C = RngCat (U)$
2		rhmsubcrngc.u	$⊢ φ \to U \in V$
3		rhmsubcrngc.b	$⊢ φ \to B = Ring \cap U$
4		rhmsubcrngc.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
5		eqidd	$⊢ φ \to U \cap Rng = U \cap Rng$
6		eqidd	$⊢ φ \to {RngHom ↾}_{((U \cap Rng) \times (U \cap Rng))} = {RngHom ↾}_{((U \cap Rng) \times (U \cap Rng))}$
7		eqidd	$⊢ φ \to comp (ExtStrCat (U)) = comp (ExtStrCat (U))$
8	1 2 5 6 7	dfrngc2	$⊢ φ \to C = \{⟨{Base}_{ndx}, U \cap Rng⟩, ⟨Hom (ndx), {RngHom ↾}_{((U \cap Rng) \times (U \cap Rng))}⟩, ⟨comp (ndx), comp (ExtStrCat (U))⟩\}$
9		inex1g	$⊢ U \in V \to U \cap Rng \in V$
10	2 9	syl	$⊢ φ \to U \cap Rng \in V$
11		rnghmfn	$⊢ RngHom Fn (Rng \times Rng)$
12		fnfun	$⊢ RngHom Fn (Rng \times Rng) \to Fun RngHom$
13	11 12	mp1i	$⊢ φ \to Fun RngHom$
14		sqxpexg	$⊢ U \cap Rng \in V \to (U \cap Rng) \times (U \cap Rng) \in V$
15	10 14	syl	$⊢ φ \to (U \cap Rng) \times (U \cap Rng) \in V$
16		resfunexg	$⊢ (Fun RngHom \land (U \cap Rng) \times (U \cap Rng) \in V) \to {RngHom ↾}_{((U \cap Rng) \times (U \cap Rng))} \in V$
17	13 15 16	syl2anc	$⊢ φ \to {RngHom ↾}_{((U \cap Rng) \times (U \cap Rng))} \in V$
18		fvexd	$⊢ φ \to comp (ExtStrCat (U)) \in V$
19		rhmfn	$⊢ RingHom Fn (Ring \times Ring)$
20		fnfun	$⊢ RingHom Fn (Ring \times Ring) \to Fun RingHom$
21	19 20	mp1i	$⊢ φ \to Fun RingHom$
22		incom	$⊢ Ring \cap U = U \cap Ring$
23	3 22	eqtrdi	$⊢ φ \to B = U \cap Ring$
24		inex1g	$⊢ U \in V \to U \cap Ring \in V$
25	2 24	syl	$⊢ φ \to U \cap Ring \in V$
26	23 25	eqeltrd	$⊢ φ \to B \in V$
27		sqxpexg	$⊢ B \in V \to B \times B \in V$
28	26 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	21 28 29	syl2anc	$⊢ φ \to {RingHom ↾}_{(B \times B)} \in V$
31	4 30	eqeltrd	$⊢ φ \to H \in V$
32		ringrng	$⊢ r \in Ring \to r \in Rng$
33	32	a1i	$⊢ φ \to (r \in Ring \to r \in Rng)$
34	33	ssrdv	$⊢ φ \to Ring \subseteq Rng$
35	34	ssrind	$⊢ φ \to Ring \cap U \subseteq Rng \cap U$
36		incom	$⊢ U \cap Rng = Rng \cap U$
37	36	a1i	$⊢ φ \to U \cap Rng = Rng \cap U$
38	35 3 37	3sstr4d	$⊢ φ \to B \subseteq U \cap Rng$
39	8 10 17 18 31 38	estrres	$⊢ φ \to (C ↾_{𝑠} B) sSet ⟨Hom (ndx), H⟩ = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), comp (ExtStrCat (U))⟩\}$
40		eqid	$⊢ C ↾_{cat} H = C ↾_{cat} H$
41		fvexd	$⊢ φ \to RngCat (U) \in V$
42	1 41	eqeltrid	$⊢ φ \to C \in V$
43	23 4	rhmresfn	$⊢ φ \to H Fn (B \times B)$
44	40 42 26 43	rescval2	$⊢ φ \to C ↾_{cat} H = (C ↾_{𝑠} B) sSet ⟨Hom (ndx), H⟩$
45		eqid	$⊢ RingCat (U) = RingCat (U)$
46	45 2 23 4 7	dfringc2	$⊢ φ \to RingCat (U) = \{⟨{Base}_{ndx}, B⟩, ⟨Hom (ndx), H⟩, ⟨comp (ndx), comp (ExtStrCat (U))⟩\}$
47	39 44 46	3eqtr4d	$⊢ φ \to C ↾_{cat} H = RingCat (U)$

Metamath Proof Explorer

Theorem rngcresringcat

Proof