rnghmsscmap

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

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

Metamath Proof Explorer

Theorem rnghmsscmap

Proof