irinitoringc

Description: The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of Adamek p. 101 , and example in Lang p. 58. (Contributed by AV, 3-Apr-2020)

	Ref	Expression
Hypotheses	irinitoringc.u	$⊢ φ \to U \in V$
	irinitoringc.z	$⊢ φ \to ℤ_{ring} \in U$
	irinitoringc.c	$⊢ C = RingCat (U)$
Assertion	irinitoringc	$⊢ φ \to ℤ_{ring} \in InitO (C)$

Proof

Step	Hyp	Ref	Expression
1		irinitoringc.u	$⊢ φ \to U \in V$
2		irinitoringc.z	$⊢ φ \to ℤ_{ring} \in U$
3		irinitoringc.c	$⊢ C = RingCat (U)$
4		zex	$⊢ ℤ \in V$
5	4	mptex	$⊢ (z \in ℤ ⟼ z \cdot_{r} 1_{r}) \in V$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7		eqid	$⊢ Hom (C) = Hom (C)$
8	3 6 1 7	ringchomfval	$⊢ φ \to Hom (C) = {RingHom ↾}_{({Base}_{C} \times {Base}_{C})}$
9	8	adantr	$⊢ (φ \land r \in {Base}_{C}) \to Hom (C) = {RingHom ↾}_{({Base}_{C} \times {Base}_{C})}$
10	9	oveqd	$⊢ (φ \land r \in {Base}_{C}) \to ℤ_{ring} Hom (C) r = ℤ_{ring} ({RingHom ↾}_{({Base}_{C} \times {Base}_{C})}) r$
11		id	$⊢ ℤ_{ring} \in U \to ℤ_{ring} \in U$
12		zringring	$⊢ ℤ_{ring} \in Ring$
13	12	a1i	$⊢ ℤ_{ring} \in U \to ℤ_{ring} \in Ring$
14	11 13	elind	$⊢ ℤ_{ring} \in U \to ℤ_{ring} \in (U \cap Ring)$
15	2 14	syl	$⊢ φ \to ℤ_{ring} \in (U \cap Ring)$
16	3 6 1	ringcbas	$⊢ φ \to {Base}_{C} = U \cap Ring$
17	15 16	eleqtrrd	$⊢ φ \to ℤ_{ring} \in {Base}_{C}$
18	17	adantr	$⊢ (φ \land r \in {Base}_{C}) \to ℤ_{ring} \in {Base}_{C}$
19		simpr	$⊢ (φ \land r \in {Base}_{C}) \to r \in {Base}_{C}$
20	18 19	ovresd	$⊢ (φ \land r \in {Base}_{C}) \to ℤ_{ring} ({RingHom ↾}_{({Base}_{C} \times {Base}_{C})}) r = ℤ_{ring} RingHom r$
21	16	eleq2d	$⊢ φ \to (r \in {Base}_{C} \leftrightarrow r \in (U \cap Ring))$
22		elin	$⊢ r \in (U \cap Ring) \leftrightarrow (r \in U \land r \in Ring)$
23	22	simprbi	$⊢ r \in (U \cap Ring) \to r \in Ring$
24	21 23	biimtrdi	$⊢ φ \to (r \in {Base}_{C} \to r \in Ring)$
25	24	imp	$⊢ (φ \land r \in {Base}_{C}) \to r \in Ring$
26		eqid	$⊢ \cdot_{r} = \cdot_{r}$
27		eqid	$⊢ (z \in ℤ ⟼ z \cdot_{r} 1_{r}) = (z \in ℤ ⟼ z \cdot_{r} 1_{r})$
28		eqid	$⊢ 1_{r} = 1_{r}$
29	26 27 28	mulgrhm2	$⊢ r \in Ring \to ℤ_{ring} RingHom r = \{(z \in ℤ ⟼ z \cdot_{r} 1_{r})\}$
30	25 29	syl	$⊢ (φ \land r \in {Base}_{C}) \to ℤ_{ring} RingHom r = \{(z \in ℤ ⟼ z \cdot_{r} 1_{r})\}$
31	10 20 30	3eqtrd	$⊢ (φ \land r \in {Base}_{C}) \to ℤ_{ring} Hom (C) r = \{(z \in ℤ ⟼ z \cdot_{r} 1_{r})\}$
32		sneq	$⊢ f = (z \in ℤ ⟼ z \cdot_{r} 1_{r}) \to \{f\} = \{(z \in ℤ ⟼ z \cdot_{r} 1_{r})\}$
33	32	eqeq2d	$⊢ f = (z \in ℤ ⟼ z \cdot_{r} 1_{r}) \to (ℤ_{ring} Hom (C) r = \{f\} \leftrightarrow ℤ_{ring} Hom (C) r = \{(z \in ℤ ⟼ z \cdot_{r} 1_{r})\})$
34	33	spcegv	$⊢ (z \in ℤ ⟼ z \cdot_{r} 1_{r}) \in V \to (ℤ_{ring} Hom (C) r = \{(z \in ℤ ⟼ z \cdot_{r} 1_{r})\} \to \exists f ℤ_{ring} Hom (C) r = \{f\})$
35	5 31 34	mpsyl	$⊢ (φ \land r \in {Base}_{C}) \to \exists f ℤ_{ring} Hom (C) r = \{f\}$
36		eusn	$⊢ \exists! f f \in (ℤ_{ring} Hom (C) r) \leftrightarrow \exists f ℤ_{ring} Hom (C) r = \{f\}$
37	35 36	sylibr	$⊢ (φ \land r \in {Base}_{C}) \to \exists! f f \in (ℤ_{ring} Hom (C) r)$
38	37	ralrimiva	$⊢ φ \to \forall r \in {Base}_{C} \exists! f f \in (ℤ_{ring} Hom (C) r)$
39	3	ringccat	$⊢ U \in V \to C \in Cat$
40	1 39	syl	$⊢ φ \to C \in Cat$
41	12	a1i	$⊢ φ \to ℤ_{ring} \in Ring$
42	2 41	elind	$⊢ φ \to ℤ_{ring} \in (U \cap Ring)$
43	42 16	eleqtrrd	$⊢ φ \to ℤ_{ring} \in {Base}_{C}$
44	6 7 40 43	isinito	$⊢ φ \to (ℤ_{ring} \in InitO (C) \leftrightarrow \forall r \in {Base}_{C} \exists! f f \in (ℤ_{ring} Hom (C) r))$
45	38 44	mpbird	$⊢ φ \to ℤ_{ring} \in InitO (C)$

Metamath Proof Explorer

Theorem irinitoringc

Proof