rngcrescrhmALTV

Description: The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-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	rngcrescrhmALTV	$⊢ φ \to C ↾_{cat} H = (C ↾_{𝑠} R) sSet ⟨Hom (ndx), H⟩$

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		eqid	$⊢ C ↾_{cat} H = C ↾_{cat} H$
6	2	fvexi	$⊢ C \in V$
7	6	a1i	$⊢ φ \to C \in V$
8		incom	$⊢ Ring \cap U = U \cap Ring$
9	3 8	eqtrdi	$⊢ φ \to R = U \cap Ring$
10		inex1g	$⊢ U \in V \to U \cap Ring \in V$
11	1 10	syl	$⊢ φ \to U \cap Ring \in V$
12	9 11	eqeltrd	$⊢ φ \to R \in V$
13		inss1	$⊢ Ring \cap U \subseteq Ring$
14	3 13	eqsstrdi	$⊢ φ \to R \subseteq Ring$
15		xpss12	$⊢ (R \subseteq Ring \land R \subseteq Ring) \to R \times R \subseteq Ring \times Ring$
16	14 14 15	syl2anc	$⊢ φ \to R \times R \subseteq Ring \times Ring$
17		rhmfn	$⊢ RingHom Fn (Ring \times Ring)$
18		fnssresb	$⊢ RingHom Fn (Ring \times Ring) \to (({RingHom ↾}_{(R \times R)}) Fn (R \times R) \leftrightarrow R \times R \subseteq Ring \times Ring)$
19	17 18	mp1i	$⊢ φ \to (({RingHom ↾}_{(R \times R)}) Fn (R \times R) \leftrightarrow R \times R \subseteq Ring \times Ring)$
20	16 19	mpbird	$⊢ φ \to ({RingHom ↾}_{(R \times R)}) Fn (R \times R)$
21	4	fneq1i	$⊢ H Fn (R \times R) \leftrightarrow ({RingHom ↾}_{(R \times R)}) Fn (R \times R)$
22	20 21	sylibr	$⊢ φ \to H Fn (R \times R)$
23	5 7 12 22	rescval2	$⊢ φ \to C ↾_{cat} H = (C ↾_{𝑠} R) sSet ⟨Hom (ndx), H⟩$

Metamath Proof Explorer

Theorem rngcrescrhmALTV

Proof