rhmsubcALTV

Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of unital ring homomorphisms is a "subcategory" of the category of non-unital rings. (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngcrescrhmALTV.u	$⊢ φ \to U \in V$
	rngcrescrhmALTV.c	$⊢ C = RngCatALTV (U)$
	rngcrescrhmALTV.r	$⊢ φ \to R = Ring \cap U$
	rngcrescrhmALTV.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
Assertion	rhmsubcALTV	$⊢ φ \to H \in Subcat (RngCatALTV (U))$

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	$⊢ φ \to U \in V$
2		rngcrescrhmALTV.c	$⊢ C = RngCatALTV (U)$
3		rngcrescrhmALTV.r	$⊢ φ \to R = Ring \cap U$
4		rngcrescrhmALTV.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
5		eqidd	$⊢ φ \to Rng \cap U = Rng \cap U$
6	1 3 5	rhmsscrnghm	$⊢ φ \to ({RingHom ↾}_{(R \times R)}) \subseteq_{cat} ({RngHomo ↾}_{((Rng \cap U) \times (Rng \cap U))})$
7	4	a1i	$⊢ φ \to H = {RingHom ↾}_{(R \times R)}$
8		eqid	$⊢ RngCatALTV (U) = RngCatALTV (U)$
9		eqid	$⊢ Rng \cap U = Rng \cap U$
10		eqid	$⊢ {Hom}_{𝑓} (RngCatALTV (U)) = {Hom}_{𝑓} (RngCatALTV (U))$
11	8 9 1 10	rngchomrnghmresALTV	$⊢ φ \to {Hom}_{𝑓} (RngCatALTV (U)) = {RngHomo ↾}_{((Rng \cap U) \times (Rng \cap U))}$
12	6 7 11	3brtr4d	$⊢ φ \to H \subseteq_{cat} {Hom}_{𝑓} (RngCatALTV (U))$
13	1 2 3 4	rhmsubcALTVlem3	$⊢ (φ \land x \in R) \to Id (RngCatALTV (U)) (x) \in (x H x)$
14	1 2 3 4	rhmsubcALTVlem4	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ comp (RngCatALTV (U)) z) f \in (x H z)$
15	14	ralrimivva	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ comp (RngCatALTV (U)) z) f \in (x H z)$
16	15	ralrimivva	$⊢ (φ \land x \in R) \to \forall y \in R \forall z \in R \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ comp (RngCatALTV (U)) z) f \in (x H z)$
17	13 16	jca	$⊢ (φ \land x \in R) \to (Id (RngCatALTV (U)) (x) \in (x H x) \land \forall y \in R \forall z \in R \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ comp (RngCatALTV (U)) z) f \in (x H z))$
18	17	ralrimiva	$⊢ φ \to \forall x \in R (Id (RngCatALTV (U)) (x) \in (x H x) \land \forall y \in R \forall z \in R \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ comp (RngCatALTV (U)) z) f \in (x H z))$
19		eqid	$⊢ Id (RngCatALTV (U)) = Id (RngCatALTV (U))$
20		eqid	$⊢ comp (RngCatALTV (U)) = comp (RngCatALTV (U))$
21	8	rngccatALTV	$⊢ U \in V \to RngCatALTV (U) \in Cat$
22	1 21	syl	$⊢ φ \to RngCatALTV (U) \in Cat$
23	1 2 3 4	rhmsubcALTVlem1	$⊢ φ \to H Fn (R \times R)$
24	10 19 20 22 23	issubc2	$⊢ φ \to (H \in Subcat (RngCatALTV (U)) \leftrightarrow (H \subseteq_{cat} {Hom}_{𝑓} (RngCatALTV (U)) \land \forall x \in R (Id (RngCatALTV (U)) (x) \in (x H x) \land \forall y \in R \forall z \in R \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ comp (RngCatALTV (U)) z) f \in (x H z))))$
25	12 18 24	mpbir2and	$⊢ φ \to H \in Subcat (RngCatALTV (U))$

Metamath Proof Explorer

Theorem rhmsubcALTV

Proof