rnghmsscmap2

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

	Ref	Expression
Hypotheses	rnghmsscmap.u	$⊢ φ \to U \in V$
	rnghmsscmap.r	$⊢ φ \to R = Rng \cap U$
Assertion	rnghmsscmap2	$⊢ φ \to ({RngHom ↾}_{(R \times R)}) \subseteq_{cat} (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}})$

Proof

Step	Hyp	Ref	Expression
1		rnghmsscmap.u	$⊢ φ \to U \in V$
2		rnghmsscmap.r	$⊢ φ \to R = Rng \cap U$
3		ssidd	$⊢ φ \to R \subseteq R$
4		eqid	$⊢ {Base}_{a} = {Base}_{a}$
5		eqid	$⊢ {Base}_{b} = {Base}_{b}$
6	4 5	rnghmf	$⊢ h \in (a RngHom b) \to h : {Base}_{a} ⟶ {Base}_{b}$
7		simpr	$⊢ ((φ \land (a \in R \land b \in R)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to h : {Base}_{a} ⟶ {Base}_{b}$
8		fvex	$⊢ {Base}_{b} \in V$
9		fvex	$⊢ {Base}_{a} \in V$
10	8 9	pm3.2i	$⊢ ({Base}_{b} \in V \land {Base}_{a} \in V)$
11		elmapg	$⊢ ({Base}_{b} \in V \land {Base}_{a} \in V) \to (h \in ({Base}_{b}^{{Base}_{a}}) \leftrightarrow h : {Base}_{a} ⟶ {Base}_{b})$
12	10 11	mp1i	$⊢ ((φ \land (a \in R \land b \in R)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to (h \in ({Base}_{b}^{{Base}_{a}}) \leftrightarrow h : {Base}_{a} ⟶ {Base}_{b})$
13	7 12	mpbird	$⊢ ((φ \land (a \in R \land b \in R)) \land h : {Base}_{a} ⟶ {Base}_{b}) \to h \in ({Base}_{b}^{{Base}_{a}})$
14	13	ex	$⊢ (φ \land (a \in R \land b \in R)) \to (h : {Base}_{a} ⟶ {Base}_{b} \to h \in ({Base}_{b}^{{Base}_{a}}))$
15	6 14	syl5	$⊢ (φ \land (a \in R \land b \in R)) \to (h \in (a RngHom b) \to h \in ({Base}_{b}^{{Base}_{a}}))$
16	15	ssrdv	$⊢ (φ \land (a \in R \land b \in R)) \to a RngHom b \subseteq {Base}_{b}^{{Base}_{a}}$
17		ovres	$⊢ (a \in R \land b \in R) \to a ({RngHom ↾}_{(R \times R)}) b = a RngHom b$
18	17	adantl	$⊢ (φ \land (a \in R \land b \in R)) \to a ({RngHom ↾}_{(R \times R)}) b = a RngHom b$
19		eqidd	$⊢ (a \in R \land b \in R) \to (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) = (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}})$
20		fveq2	$⊢ y = b \to {Base}_{y} = {Base}_{b}$
21		fveq2	$⊢ x = a \to {Base}_{x} = {Base}_{a}$
22	20 21	oveqan12rd	$⊢ (x = a \land y = b) \to {Base}_{y}^{{Base}_{x}} = {Base}_{b}^{{Base}_{a}}$
23	22	adantl	$⊢ ((a \in R \land b \in R) \land (x = a \land y = b)) \to {Base}_{y}^{{Base}_{x}} = {Base}_{b}^{{Base}_{a}}$
24		simpl	$⊢ (a \in R \land b \in R) \to a \in R$
25		simpr	$⊢ (a \in R \land b \in R) \to b \in R$
26		ovexd	$⊢ (a \in R \land b \in R) \to {Base}_{b}^{{Base}_{a}} \in V$
27	19 23 24 25 26	ovmpod	$⊢ (a \in R \land b \in R) \to a (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) b = {Base}_{b}^{{Base}_{a}}$
28	27	adantl	$⊢ (φ \land (a \in R \land b \in R)) \to a (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) b = {Base}_{b}^{{Base}_{a}}$
29	16 18 28	3sstr4d	$⊢ (φ \land (a \in R \land b \in R)) \to a ({RngHom ↾}_{(R \times R)}) b \subseteq a (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) b$
30	29	ralrimivva	$⊢ φ \to \forall a \in R \forall b \in R a ({RngHom ↾}_{(R \times R)}) b \subseteq a (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) b$
31		rnghmfn	$⊢ RngHom Fn (Rng \times Rng)$
32	31	a1i	$⊢ φ \to RngHom Fn (Rng \times Rng)$
33		inss1	$⊢ Rng \cap U \subseteq Rng$
34	2 33	eqsstrdi	$⊢ φ \to R \subseteq Rng$
35		xpss12	$⊢ (R \subseteq Rng \land R \subseteq Rng) \to R \times R \subseteq Rng \times Rng$
36	34 34 35	syl2anc	$⊢ φ \to R \times R \subseteq Rng \times Rng$
37		fnssres	$⊢ (RngHom Fn (Rng \times Rng) \land R \times R \subseteq Rng \times Rng) \to ({RngHom ↾}_{(R \times R)}) Fn (R \times R)$
38	32 36 37	syl2anc	$⊢ φ \to ({RngHom ↾}_{(R \times R)}) Fn (R \times R)$
39		eqid	$⊢ (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) = (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}})$
40		ovex	$⊢ {Base}_{y}^{{Base}_{x}} \in V$
41	39 40	fnmpoi	$⊢ (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) Fn (R \times R)$
42	41	a1i	$⊢ φ \to (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) Fn (R \times R)$
43		incom	$⊢ Rng \cap U = U \cap Rng$
44		inex1g	$⊢ U \in V \to U \cap Rng \in V$
45	1 44	syl	$⊢ φ \to U \cap Rng \in V$
46	43 45	eqeltrid	$⊢ φ \to Rng \cap U \in V$
47	2 46	eqeltrd	$⊢ φ \to R \in V$
48	38 42 47	isssc	$⊢ φ \to (({RngHom ↾}_{(R \times R)}) \subseteq_{cat} (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) \leftrightarrow (R \subseteq R \land \forall a \in R \forall b \in R a ({RngHom ↾}_{(R \times R)}) b \subseteq a (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}}) b))$
49	3 30 48	mpbir2and	$⊢ φ \to ({RngHom ↾}_{(R \times R)}) \subseteq_{cat} (x \in R, y \in R ⟼ {Base}_{y}^{{Base}_{x}})$

Metamath Proof Explorer

Theorem rnghmsscmap2

Proof