fldcALTV

Description: The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		drhmsubcALTV.c	$⊢ C = U \cap DivRing$
2		drhmsubcALTV.j	$⊢ J = (r \in C, s \in C ⟼ r RingHom s)$
3		fldhmsubcALTV.d	$⊢ D = U \cap Field$
4		fldhmsubcALTV.f	$⊢ F = (r \in D, s \in D ⟼ r RingHom s)$
5		fvexd	$⊢ U \in V \to RingCatALTV (U) \in V$
6		ovex	$⊢ r RingHom s \in V$
7	2 6	fnmpoi	$⊢ J Fn (C \times C)$
8	7	a1i	$⊢ U \in V \to J Fn (C \times C)$
9	4 6	fnmpoi	$⊢ F Fn (D \times D)$
10	9	a1i	$⊢ U \in V \to F Fn (D \times D)$
11		inex1g	$⊢ U \in V \to U \cap DivRing \in V$
12	1 11	eqeltrid	$⊢ U \in V \to C \in V$
13		df-field	$⊢ Field = DivRing \cap CRing$
14		inss1	$⊢ DivRing \cap CRing \subseteq DivRing$
15	13 14	eqsstri	$⊢ Field \subseteq DivRing$
16		sslin	$⊢ Field \subseteq DivRing \to U \cap Field \subseteq U \cap DivRing$
17	15 16	mp1i	$⊢ U \in V \to U \cap Field \subseteq U \cap DivRing$
18	17 3 1	3sstr4g	$⊢ U \in V \to D \subseteq C$
19	5 8 10 12 18	rescabs	$⊢ U \in V \to (RingCatALTV (U) ↾_{cat} J) ↾_{cat} F = RingCatALTV (U) ↾_{cat} F$
20	1 2 3 4	fldcatALTV	$⊢ U \in V \to RingCatALTV (U) ↾_{cat} F \in Cat$
21	19 20	eqeltrd	$⊢ U \in V \to (RingCatALTV (U) ↾_{cat} J) ↾_{cat} F \in Cat$

Metamath Proof Explorer

Theorem fldcALTV

Proof