fldhmsubc

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 field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020)

	Ref	Expression
Hypotheses	drhmsubc.c	$⊢ C = U \cap DivRing$
	drhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
	fldhmsubc.d	$⊢ D = U \cap Field$
	fldhmsubc.f	$⊢ F = (r \in D, s \in D ⟼ r RingHom s)$
Assertion	fldhmsubc	$⊢ U \in V \to F \in Subcat (RingCat (U) ↾_{cat} J)$

Proof

Step	Hyp	Ref	Expression
1		drhmsubc.c	$⊢ C = U \cap DivRing$
2		drhmsubc.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
3		fldhmsubc.d	$⊢ D = U \cap Field$
4		fldhmsubc.f	$⊢ F = (r \in D, s \in D ⟼ r RingHom s)$
5		elin	$⊢ r \in (DivRing \cap CRing) \leftrightarrow (r \in DivRing \land r \in CRing)$
6	5	simprbi	$⊢ r \in (DivRing \cap CRing) \to r \in CRing$
7		crngring	$⊢ r \in CRing \to r \in Ring$
8	6 7	syl	$⊢ r \in (DivRing \cap CRing) \to r \in Ring$
9		df-field	$⊢ Field = DivRing \cap CRing$
10	8 9	eleq2s	$⊢ r \in Field \to r \in Ring$
11	10	rgen	$⊢ \forall r \in Field r \in Ring$
12	11 3 4	srhmsubc	$⊢ U \in V \to F \in Subcat (RingCat (U))$
13		inss1	$⊢ DivRing \cap CRing \subseteq DivRing$
14	9 13	eqsstri	$⊢ Field \subseteq DivRing$
15		sslin	$⊢ Field \subseteq DivRing \to U \cap Field \subseteq U \cap DivRing$
16	14 15	ax-mp	$⊢ U \cap Field \subseteq U \cap DivRing$
17	16	a1i	$⊢ U \in V \to U \cap Field \subseteq U \cap DivRing$
18	3 1	sseq12i	$⊢ D \subseteq C \leftrightarrow U \cap Field \subseteq U \cap DivRing$
19	17 18	sylibr	$⊢ U \in V \to D \subseteq C$
20		ssidd	$⊢ (U \in V \land (x \in D \land y \in D)) \to x RingHom y \subseteq x RingHom y$
21	4	a1i	$⊢ (U \in V \land (x \in D \land y \in D)) \to F = (r \in D, s \in D ⟼ 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 D \land y \in D)) \land (r = x \land s = y)) \to r RingHom s = x RingHom y$
24		simprl	$⊢ (U \in V \land (x \in D \land y \in D)) \to x \in D$
25		simpr	$⊢ (x \in D \land y \in D) \to y \in D$
26	25	adantl	$⊢ (U \in V \land (x \in D \land y \in D)) \to y \in D$
27		ovexd	$⊢ (U \in V \land (x \in D \land y \in D)) \to x RingHom y \in V$
28	21 23 24 26 27	ovmpod	$⊢ (U \in V \land (x \in D \land y \in D)) \to x F y = x RingHom y$
29	2	a1i	$⊢ (U \in V \land (x \in D \land y \in D)) \to J = (r \in C, s \in C ⟼ r RingHom s)$
30	16 18	mpbir	$⊢ D \subseteq C$
31	30	sseli	$⊢ x \in D \to x \in C$
32	31	ad2antrl	$⊢ (U \in V \land (x \in D \land y \in D)) \to x \in C$
33	30	sseli	$⊢ y \in D \to y \in C$
34	33	adantl	$⊢ (x \in D \land y \in D) \to y \in C$
35	34	adantl	$⊢ (U \in V \land (x \in D \land y \in D)) \to y \in C$
36	29 23 32 35 27	ovmpod	$⊢ (U \in V \land (x \in D \land y \in D)) \to x J y = x RingHom y$
37	20 28 36	3sstr4d	$⊢ (U \in V \land (x \in D \land y \in D)) \to x F y \subseteq x J y$
38	37	ralrimivva	$⊢ U \in V \to \forall x \in D \forall y \in D x F y \subseteq x J y$
39		ovex	$⊢ r RingHom s \in V$
40	4 39	fnmpoi	$⊢ F Fn (D \times D)$
41	40	a1i	$⊢ U \in V \to F Fn (D \times D)$
42	2 39	fnmpoi	$⊢ J Fn (C \times C)$
43	42	a1i	$⊢ U \in V \to J Fn (C \times C)$
44		inex1g	$⊢ U \in V \to U \cap DivRing \in V$
45	1 44	eqeltrid	$⊢ U \in V \to C \in V$
46	41 43 45	isssc	$⊢ U \in V \to (F \subseteq_{cat} J \leftrightarrow (D \subseteq C \land \forall x \in D \forall y \in D x F y \subseteq x J y))$
47	19 38 46	mpbir2and	$⊢ U \in V \to F \subseteq_{cat} J$
48	1 2	drhmsubc	$⊢ U \in V \to J \in Subcat (RingCat (U))$
49		eqid	$⊢ RingCat (U) ↾_{cat} J = RingCat (U) ↾_{cat} J$
50	49	subsubc	$⊢ J \in Subcat (RingCat (U)) \to (F \in Subcat (RingCat (U) ↾_{cat} J) \leftrightarrow (F \in Subcat (RingCat (U)) \land F \subseteq_{cat} J))$
51	48 50	syl	$⊢ U \in V \to (F \in Subcat (RingCat (U) ↾_{cat} J) \leftrightarrow (F \in Subcat (RingCat (U)) \land F \subseteq_{cat} J))$
52	12 47 51	mpbir2and	$⊢ U \in V \to F \in Subcat (RingCat (U) ↾_{cat} J)$

Metamath Proof Explorer

Theorem fldhmsubc

Proof