srhmsubc

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 special ring homomorphisms (i.e., ring homomorphisms from a special ring to another ring of that kind) is a subcategory of the category of (unital) rings. (Contributed by AV, 19-Feb-2020)

	Ref	Expression
Hypotheses	srhmsubc.s	$⊢ \forall r \in S r \in Ring$
	srhmsubc.c	$⊢ C = U \cap S$
	srhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
Assertion	srhmsubc	$⊢ U \in V \to J \in Subcat (RingCat (U))$

Proof

Step	Hyp	Ref	Expression
1		srhmsubc.s	$⊢ \forall r \in S r \in Ring$
2		srhmsubc.c	$⊢ C = U \cap S$
3		srhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
4		eleq1w	$⊢ r = x \to (r \in Ring \leftrightarrow x \in Ring)$
5	4 1	vtoclri	$⊢ x \in S \to x \in Ring$
6	5	ssriv	$⊢ S \subseteq Ring$
7		sslin	$⊢ S \subseteq Ring \to U \cap S \subseteq U \cap Ring$
8	6 7	mp1i	$⊢ U \in V \to U \cap S \subseteq U \cap Ring$
9	2 8	eqsstrid	$⊢ U \in V \to C \subseteq U \cap Ring$
10		ssid	$⊢ x RingHom y \subseteq x RingHom y$
11		eqid	$⊢ RingCat (U) = RingCat (U)$
12		eqid	$⊢ {Base}_{RingCat (U)} = {Base}_{RingCat (U)}$
13		simpl	$⊢ (U \in V \land (x \in C \land y \in C)) \to U \in V$
14		eqid	$⊢ Hom (RingCat (U)) = Hom (RingCat (U))$
15	1 2	srhmsubclem2	$⊢ (U \in V \land x \in C) \to x \in {Base}_{RingCat (U)}$
16	15	adantrr	$⊢ (U \in V \land (x \in C \land y \in C)) \to x \in {Base}_{RingCat (U)}$
17	1 2	srhmsubclem2	$⊢ (U \in V \land y \in C) \to y \in {Base}_{RingCat (U)}$
18	17	adantrl	$⊢ (U \in V \land (x \in C \land y \in C)) \to y \in {Base}_{RingCat (U)}$
19	11 12 13 14 16 18	ringchom	$⊢ (U \in V \land (x \in C \land y \in C)) \to x Hom (RingCat (U)) y = x RingHom y$
20	10 19	sseqtrrid	$⊢ (U \in V \land (x \in C \land y \in C)) \to x RingHom y \subseteq x Hom (RingCat (U)) y$
21	3	a1i	$⊢ (U \in V \land (x \in C \land y \in C)) \to J = (r \in C, s \in C ⟼ r RingHom s)$
22		oveq12	$⊢ (r = x \land s = y) \to r RingHom s = x RingHom y$
23	22	adantl	$⊢ ((U \in V \land (x \in C \land y \in C)) \land (r = x \land s = y)) \to r RingHom s = x RingHom y$
24		simprl	$⊢ (U \in V \land (x \in C \land y \in C)) \to x \in C$
25		simprr	$⊢ (U \in V \land (x \in C \land y \in C)) \to y \in C$
26		ovexd	$⊢ (U \in V \land (x \in C \land y \in C)) \to x RingHom y \in V$
27	21 23 24 25 26	ovmpod	$⊢ (U \in V \land (x \in C \land y \in C)) \to x J y = x RingHom y$
28		eqid	$⊢ {Hom}_{𝑓} (RingCat (U)) = {Hom}_{𝑓} (RingCat (U))$
29	28 12 14 16 18	homfval	$⊢ (U \in V \land (x \in C \land y \in C)) \to x {Hom}_{𝑓} (RingCat (U)) y = x Hom (RingCat (U)) y$
30	20 27 29	3sstr4d	$⊢ (U \in V \land (x \in C \land y \in C)) \to x J y \subseteq x {Hom}_{𝑓} (RingCat (U)) y$
31	30	ralrimivva	$⊢ U \in V \to \forall x \in C \forall y \in C x J y \subseteq x {Hom}_{𝑓} (RingCat (U)) y$
32		ovex	$⊢ r RingHom s \in V$
33	3 32	fnmpoi	$⊢ J Fn (C \times C)$
34	33	a1i	$⊢ U \in V \to J Fn (C \times C)$
35	28 12	homffn	$⊢ {Hom}_{𝑓} (RingCat (U)) Fn ({Base}_{RingCat (U)} \times {Base}_{RingCat (U)})$
36		id	$⊢ U \in V \to U \in V$
37	11 12 36	ringcbas	$⊢ U \in V \to {Base}_{RingCat (U)} = U \cap Ring$
38	37	eqcomd	$⊢ U \in V \to U \cap Ring = {Base}_{RingCat (U)}$
39	38	sqxpeqd	$⊢ U \in V \to (U \cap Ring) \times (U \cap Ring) = {Base}_{RingCat (U)} \times {Base}_{RingCat (U)}$
40	39	fneq2d	$⊢ U \in V \to ({Hom}_{𝑓} (RingCat (U)) Fn ((U \cap Ring) \times (U \cap Ring)) \leftrightarrow {Hom}_{𝑓} (RingCat (U)) Fn ({Base}_{RingCat (U)} \times {Base}_{RingCat (U)}))$
41	35 40	mpbiri	$⊢ U \in V \to {Hom}_{𝑓} (RingCat (U)) Fn ((U \cap Ring) \times (U \cap Ring))$
42		inex1g	$⊢ U \in V \to U \cap Ring \in V$
43	34 41 42	isssc	$⊢ U \in V \to (J \subseteq_{cat} {Hom}_{𝑓} (RingCat (U)) \leftrightarrow (C \subseteq U \cap Ring \land \forall x \in C \forall y \in C x J y \subseteq x {Hom}_{𝑓} (RingCat (U)) y))$
44	9 31 43	mpbir2and	$⊢ U \in V \to J \subseteq_{cat} {Hom}_{𝑓} (RingCat (U))$
45	2	elin2	$⊢ x \in C \leftrightarrow (x \in U \land x \in S)$
46	5	adantl	$⊢ (x \in U \land x \in S) \to x \in Ring$
47	45 46	sylbi	$⊢ x \in C \to x \in Ring$
48	47	adantl	$⊢ (U \in V \land x \in C) \to x \in Ring$
49		eqid	$⊢ {Base}_{x} = {Base}_{x}$
50	49	idrhm	$⊢ x \in Ring \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
51	48 50	syl	$⊢ (U \in V \land x \in C) \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
52		eqid	$⊢ Id (RingCat (U)) = Id (RingCat (U))$
53		simpl	$⊢ (U \in V \land x \in C) \to U \in V$
54	11 12 52 53 15 49	ringcid	$⊢ (U \in V \land x \in C) \to Id (RingCat (U)) (x) = {I ↾}_{{Base}_{x}}$
55	3	a1i	$⊢ (U \in V \land x \in C) \to J = (r \in C, s \in C ⟼ r RingHom s)$
56		oveq12	$⊢ (r = x \land s = x) \to r RingHom s = x RingHom x$
57	56	adantl	$⊢ ((U \in V \land x \in C) \land (r = x \land s = x)) \to r RingHom s = x RingHom x$
58		simpr	$⊢ (U \in V \land x \in C) \to x \in C$
59		ovexd	$⊢ (U \in V \land x \in C) \to x RingHom x \in V$
60	55 57 58 58 59	ovmpod	$⊢ (U \in V \land x \in C) \to x J x = x RingHom x$
61	51 54 60	3eltr4d	$⊢ (U \in V \land x \in C) \to Id (RingCat (U)) (x) \in (x J x)$
62		eqid	$⊢ comp (RingCat (U)) = comp (RingCat (U))$
63	11	ringccat	$⊢ U \in V \to RingCat (U) \in Cat$
64	63	ad3antrrr	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to RingCat (U) \in Cat$
65	15	adantr	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to x \in {Base}_{RingCat (U)}$
66	65	adantr	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to x \in {Base}_{RingCat (U)}$
67	17	ad2ant2r	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to y \in {Base}_{RingCat (U)}$
68	67	adantr	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to y \in {Base}_{RingCat (U)}$
69	1 2	srhmsubclem2	$⊢ (U \in V \land z \in C) \to z \in {Base}_{RingCat (U)}$
70	69	ad2ant2rl	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to z \in {Base}_{RingCat (U)}$
71	70	adantr	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to z \in {Base}_{RingCat (U)}$
72	53	adantr	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to U \in V$
73		simpl	$⊢ (y \in C \land z \in C) \to y \in C$
74	58 73	anim12i	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to (x \in C \land y \in C)$
75	72 74	jca	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to (U \in V \land (x \in C \land y \in C))$
76	1 2 3	srhmsubclem3	$⊢ (U \in V \land (x \in C \land y \in C)) \to x J y = x Hom (RingCat (U)) y$
77	75 76	syl	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to x J y = x Hom (RingCat (U)) y$
78	77	eleq2d	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to (f \in (x J y) \leftrightarrow f \in (x Hom (RingCat (U)) y))$
79	78	biimpcd	$⊢ f \in (x J y) \to (((U \in V \land x \in C) \land (y \in C \land z \in C)) \to f \in (x Hom (RingCat (U)) y))$
80	79	adantr	$⊢ (f \in (x J y) \land g \in (y J z)) \to (((U \in V \land x \in C) \land (y \in C \land z \in C)) \to f \in (x Hom (RingCat (U)) y))$
81	80	impcom	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to f \in (x Hom (RingCat (U)) y)$
82	1 2 3	srhmsubclem3	$⊢ (U \in V \land (y \in C \land z \in C)) \to y J z = y Hom (RingCat (U)) z$
83	82	adantlr	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to y J z = y Hom (RingCat (U)) z$
84	83	eleq2d	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to (g \in (y J z) \leftrightarrow g \in (y Hom (RingCat (U)) z))$
85	84	biimpd	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to (g \in (y J z) \to g \in (y Hom (RingCat (U)) z))$
86	85	adantld	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to ((f \in (x J y) \land g \in (y J z)) \to g \in (y Hom (RingCat (U)) z))$
87	86	imp	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to g \in (y Hom (RingCat (U)) z)$
88	12 14 62 64 66 68 71 81 87	catcocl	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to g (⟨x, y⟩ comp (RingCat (U)) z) f \in (x Hom (RingCat (U)) z)$
89	11 12 72 14 65 70	ringchom	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to x Hom (RingCat (U)) z = x RingHom z$
90	89	eqcomd	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to x RingHom z = x Hom (RingCat (U)) z$
91	90	adantr	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to x RingHom z = x Hom (RingCat (U)) z$
92	88 91	eleqtrrd	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to g (⟨x, y⟩ comp (RingCat (U)) z) f \in (x RingHom z)$
93	3	a1i	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to J = (r \in C, s \in C ⟼ r RingHom s)$
94		oveq12	$⊢ (r = x \land s = z) \to r RingHom s = x RingHom z$
95	94	adantl	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (r = x \land s = z)) \to r RingHom s = x RingHom z$
96	58	adantr	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to x \in C$
97		simprr	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to z \in C$
98		ovexd	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to x RingHom z \in V$
99	93 95 96 97 98	ovmpod	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to x J z = x RingHom z$
100	99	adantr	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to x J z = x RingHom z$
101	92 100	eleqtrrd	$⊢ (((U \in V \land x \in C) \land (y \in C \land z \in C)) \land (f \in (x J y) \land g \in (y J z))) \to g (⟨x, y⟩ comp (RingCat (U)) z) f \in (x J z)$
102	101	ralrimivva	$⊢ ((U \in V \land x \in C) \land (y \in C \land z \in C)) \to \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (RingCat (U)) z) f \in (x J z)$
103	102	ralrimivva	$⊢ (U \in V \land x \in C) \to \forall y \in C \forall z \in C \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (RingCat (U)) z) f \in (x J z)$
104	61 103	jca	$⊢ (U \in V \land x \in C) \to (Id (RingCat (U)) (x) \in (x J x) \land \forall y \in C \forall z \in C \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (RingCat (U)) z) f \in (x J z))$
105	104	ralrimiva	$⊢ U \in V \to \forall x \in C (Id (RingCat (U)) (x) \in (x J x) \land \forall y \in C \forall z \in C \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (RingCat (U)) z) f \in (x J z))$
106	28 52 62 63 34	issubc2	$⊢ U \in V \to (J \in Subcat (RingCat (U)) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (RingCat (U)) \land \forall x \in C (Id (RingCat (U)) (x) \in (x J x) \land \forall y \in C \forall z \in C \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (RingCat (U)) z) f \in (x J z))))$
107	44 105 106	mpbir2and	$⊢ U \in V \to J \in Subcat (RingCat (U))$

Metamath Proof Explorer

Theorem srhmsubc

Proof