rhmsscrnghm

Description: The unital ring homomorphisms between unital rings (in a universe) are a subcategory subset of the non-unital ring homomorphisms between non-unital rings (in the same universe). (Contributed by AV, 1-Mar-2020)

	Ref	Expression
Hypotheses	rhmsscrnghm.u	$⊢ φ \to U \in V$
	rhmsscrnghm.r	$⊢ φ \to R = Ring \cap U$
	rhmsscrnghm.s	$⊢ φ \to S = Rng \cap U$
Assertion	rhmsscrnghm	$⊢ φ \to ({RingHom ↾}_{(R \times R)}) \subseteq_{cat} ({RngHomo ↾}_{(S \times S)})$

Proof

Step	Hyp	Ref	Expression
1		rhmsscrnghm.u	$⊢ φ \to U \in V$
2		rhmsscrnghm.r	$⊢ φ \to R = Ring \cap U$
3		rhmsscrnghm.s	$⊢ φ \to S = Rng \cap U$
4		ringrng	$⊢ r \in Ring \to r \in Rng$
5	4	a1i	$⊢ φ \to (r \in Ring \to r \in Rng)$
6	5	ssrdv	$⊢ φ \to Ring \subseteq Rng$
7	6	ssrind	$⊢ φ \to Ring \cap U \subseteq Rng \cap U$
8	7 2 3	3sstr4d	$⊢ φ \to R \subseteq S$
9		ovres	$⊢ (x \in R \land y \in R) \to x ({RingHom ↾}_{(R \times R)}) y = x RingHom y$
10	9	adantl	$⊢ (φ \land (x \in R \land y \in R)) \to x ({RingHom ↾}_{(R \times R)}) y = x RingHom y$
11	10	eleq2d	$⊢ (φ \land (x \in R \land y \in R)) \to (h \in (x ({RingHom ↾}_{(R \times R)}) y) \leftrightarrow h \in (x RingHom y))$
12		rhmisrnghm	$⊢ h \in (x RingHom y) \to h \in (x RngHomo y)$
13	8	sseld	$⊢ φ \to (x \in R \to x \in S)$
14	8	sseld	$⊢ φ \to (y \in R \to y \in S)$
15	13 14	anim12d	$⊢ φ \to ((x \in R \land y \in R) \to (x \in S \land y \in S))$
16	15	imp	$⊢ (φ \land (x \in R \land y \in R)) \to (x \in S \land y \in S)$
17		ovres	$⊢ (x \in S \land y \in S) \to x ({RngHomo ↾}_{(S \times S)}) y = x RngHomo y$
18	16 17	syl	$⊢ (φ \land (x \in R \land y \in R)) \to x ({RngHomo ↾}_{(S \times S)}) y = x RngHomo y$
19	18	eleq2d	$⊢ (φ \land (x \in R \land y \in R)) \to (h \in (x ({RngHomo ↾}_{(S \times S)}) y) \leftrightarrow h \in (x RngHomo y))$
20	12 19	imbitrrid	$⊢ (φ \land (x \in R \land y \in R)) \to (h \in (x RingHom y) \to h \in (x ({RngHomo ↾}_{(S \times S)}) y))$
21	11 20	sylbid	$⊢ (φ \land (x \in R \land y \in R)) \to (h \in (x ({RingHom ↾}_{(R \times R)}) y) \to h \in (x ({RngHomo ↾}_{(S \times S)}) y))$
22	21	ssrdv	$⊢ (φ \land (x \in R \land y \in R)) \to x ({RingHom ↾}_{(R \times R)}) y \subseteq x ({RngHomo ↾}_{(S \times S)}) y$
23	22	ralrimivva	$⊢ φ \to \forall x \in R \forall y \in R x ({RingHom ↾}_{(R \times R)}) y \subseteq x ({RngHomo ↾}_{(S \times S)}) y$
24		inss1	$⊢ Ring \cap U \subseteq Ring$
25	2 24	eqsstrdi	$⊢ φ \to R \subseteq Ring$
26		xpss12	$⊢ (R \subseteq Ring \land R \subseteq Ring) \to R \times R \subseteq Ring \times Ring$
27	25 25 26	syl2anc	$⊢ φ \to R \times R \subseteq Ring \times Ring$
28		rhmfn	$⊢ RingHom Fn (Ring \times Ring)$
29		fnssresb	$⊢ RingHom Fn (Ring \times Ring) \to (({RingHom ↾}_{(R \times R)}) Fn (R \times R) \leftrightarrow R \times R \subseteq Ring \times Ring)$
30	28 29	mp1i	$⊢ φ \to (({RingHom ↾}_{(R \times R)}) Fn (R \times R) \leftrightarrow R \times R \subseteq Ring \times Ring)$
31	27 30	mpbird	$⊢ φ \to ({RingHom ↾}_{(R \times R)}) Fn (R \times R)$
32		inss1	$⊢ Rng \cap U \subseteq Rng$
33	3 32	eqsstrdi	$⊢ φ \to S \subseteq Rng$
34		xpss12	$⊢ (S \subseteq Rng \land S \subseteq Rng) \to S \times S \subseteq Rng \times Rng$
35	33 33 34	syl2anc	$⊢ φ \to S \times S \subseteq Rng \times Rng$
36		rnghmfn	$⊢ RngHomo Fn (Rng \times Rng)$
37		fnssresb	$⊢ RngHomo Fn (Rng \times Rng) \to (({RngHomo ↾}_{(S \times S)}) Fn (S \times S) \leftrightarrow S \times S \subseteq Rng \times Rng)$
38	36 37	mp1i	$⊢ φ \to (({RngHomo ↾}_{(S \times S)}) Fn (S \times S) \leftrightarrow S \times S \subseteq Rng \times Rng)$
39	35 38	mpbird	$⊢ φ \to ({RngHomo ↾}_{(S \times S)}) Fn (S \times S)$
40		incom	$⊢ Rng \cap U = U \cap Rng$
41		inex1g	$⊢ U \in V \to U \cap Rng \in V$
42	40 41	eqeltrid	$⊢ U \in V \to Rng \cap U \in V$
43	1 42	syl	$⊢ φ \to Rng \cap U \in V$
44	3 43	eqeltrd	$⊢ φ \to S \in V$
45	31 39 44	isssc	$⊢ φ \to (({RingHom ↾}_{(R \times R)}) \subseteq_{cat} ({RngHomo ↾}_{(S \times S)}) \leftrightarrow (R \subseteq S \land \forall x \in R \forall y \in R x ({RingHom ↾}_{(R \times R)}) y \subseteq x ({RngHomo ↾}_{(S \times S)}) y))$
46	8 23 45	mpbir2and	$⊢ φ \to ({RingHom ↾}_{(R \times R)}) \subseteq_{cat} ({RngHomo ↾}_{(S \times S)})$

Metamath Proof Explorer

Theorem rhmsscrnghm

Proof