zrtermoringc

Description: The zero ring is a terminal object in the category of unital rings. (Contributed by AV, 17-Apr-2020)

	Ref	Expression
Hypotheses	zrtermoringc.u	$⊢ φ \to U \in V$
	zrtermoringc.c	$⊢ C = RingCat (U)$
	zrtermoringc.z	$⊢ φ \to Z \in (Ring ∖ NzRing)$
	zrtermoringc.e	$⊢ φ \to Z \in U$
Assertion	zrtermoringc	$⊢ φ \to Z \in TermO (C)$

Proof

Step	Hyp	Ref	Expression
1		zrtermoringc.u	$⊢ φ \to U \in V$
2		zrtermoringc.c	$⊢ C = RingCat (U)$
3		zrtermoringc.z	$⊢ φ \to Z \in (Ring ∖ NzRing)$
4		zrtermoringc.e	$⊢ φ \to Z \in U$
5		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6	2 5 1	ringcbas	$⊢ φ \to {Base}_{C} = U \cap Ring$
7	6	eleq2d	$⊢ φ \to (r \in {Base}_{C} \leftrightarrow r \in (U \cap Ring))$
8		elin	$⊢ r \in (U \cap Ring) \leftrightarrow (r \in U \land r \in Ring)$
9	8	simprbi	$⊢ r \in (U \cap Ring) \to r \in Ring$
10	7 9	syl6bi	$⊢ φ \to (r \in {Base}_{C} \to r \in Ring)$
11	10	imp	$⊢ (φ \land r \in {Base}_{C}) \to r \in Ring$
12	3	adantr	$⊢ (φ \land r \in {Base}_{C}) \to Z \in (Ring ∖ NzRing)$
13		eqid	$⊢ {Base}_{r} = {Base}_{r}$
14		eqid	$⊢ 0_{Z} = 0_{Z}$
15		eqid	$⊢ (x \in {Base}_{r} ⟼ 0_{Z}) = (x \in {Base}_{r} ⟼ 0_{Z})$
16	13 14 15	c0rhm	$⊢ (r \in Ring \land Z \in (Ring ∖ NzRing)) \to (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)$
17	11 12 16	syl2anc	$⊢ (φ \land r \in {Base}_{C}) \to (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)$
18		simpr	$⊢ ((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \to (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)$
19	1	adantr	$⊢ (φ \land r \in {Base}_{C}) \to U \in V$
20		eqid	$⊢ Hom (C) = Hom (C)$
21		simpr	$⊢ (φ \land r \in {Base}_{C}) \to r \in {Base}_{C}$
22	3	eldifad	$⊢ φ \to Z \in Ring$
23	4 22	elind	$⊢ φ \to Z \in (U \cap Ring)$
24	23 6	eleqtrrd	$⊢ φ \to Z \in {Base}_{C}$
25	24	adantr	$⊢ (φ \land r \in {Base}_{C}) \to Z \in {Base}_{C}$
26	2 5 19 20 21 25	ringchom	$⊢ (φ \land r \in {Base}_{C}) \to r Hom (C) Z = r RingHom Z$
27	26	eqcomd	$⊢ (φ \land r \in {Base}_{C}) \to r RingHom Z = r Hom (C) Z$
28	27	eleq2d	$⊢ (φ \land r \in {Base}_{C}) \to ((x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z) \leftrightarrow (x \in {Base}_{r} ⟼ 0_{Z}) \in (r Hom (C) Z))$
29	28	biimpa	$⊢ ((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \to (x \in {Base}_{r} ⟼ 0_{Z}) \in (r Hom (C) Z)$
30	26	eleq2d	$⊢ (φ \land r \in {Base}_{C}) \to (h \in (r Hom (C) Z) \leftrightarrow h \in (r RingHom Z))$
31		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
32	13 31	rhmf	$⊢ h \in (r RingHom Z) \to h : {Base}_{r} ⟶ {Base}_{Z}$
33	30 32	syl6bi	$⊢ (φ \land r \in {Base}_{C}) \to (h \in (r Hom (C) Z) \to h : {Base}_{r} ⟶ {Base}_{Z})$
34	33	adantr	$⊢ ((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \to (h \in (r Hom (C) Z) \to h : {Base}_{r} ⟶ {Base}_{Z})$
35		ffn	$⊢ h : {Base}_{r} ⟶ {Base}_{Z} \to h Fn {Base}_{r}$
36	35	adantl	$⊢ (((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \land h : {Base}_{r} ⟶ {Base}_{Z}) \to h Fn {Base}_{r}$
37		fvex	$⊢ 0_{Z} \in V$
38	37 15	fnmpti	$⊢ (x \in {Base}_{r} ⟼ 0_{Z}) Fn {Base}_{r}$
39	38	a1i	$⊢ (((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \land h : {Base}_{r} ⟶ {Base}_{Z}) \to (x \in {Base}_{r} ⟼ 0_{Z}) Fn {Base}_{r}$
40	31 14	0ringbas	$⊢ Z \in (Ring ∖ NzRing) \to {Base}_{Z} = \{0_{Z}\}$
41	3 40	syl	$⊢ φ \to {Base}_{Z} = \{0_{Z}\}$
42	41	adantr	$⊢ (φ \land r \in {Base}_{C}) \to {Base}_{Z} = \{0_{Z}\}$
43	42	feq3d	$⊢ (φ \land r \in {Base}_{C}) \to (h : {Base}_{r} ⟶ {Base}_{Z} \leftrightarrow h : {Base}_{r} ⟶ \{0_{Z}\})$
44		fvconst	$⊢ (h : {Base}_{r} ⟶ \{0_{Z}\} \land a \in {Base}_{r}) \to h (a) = 0_{Z}$
45	44	ex	$⊢ h : {Base}_{r} ⟶ \{0_{Z}\} \to (a \in {Base}_{r} \to h (a) = 0_{Z})$
46	43 45	syl6bi	$⊢ (φ \land r \in {Base}_{C}) \to (h : {Base}_{r} ⟶ {Base}_{Z} \to (a \in {Base}_{r} \to h (a) = 0_{Z}))$
47	46	adantr	$⊢ ((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \to (h : {Base}_{r} ⟶ {Base}_{Z} \to (a \in {Base}_{r} \to h (a) = 0_{Z}))$
48	47	imp31	$⊢ ((((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \land h : {Base}_{r} ⟶ {Base}_{Z}) \land a \in {Base}_{r}) \to h (a) = 0_{Z}$
49		eqidd	$⊢ a \in {Base}_{r} \to (x \in {Base}_{r} ⟼ 0_{Z}) = (x \in {Base}_{r} ⟼ 0_{Z})$
50		eqidd	$⊢ (a \in {Base}_{r} \land x = a) \to 0_{Z} = 0_{Z}$
51		id	$⊢ a \in {Base}_{r} \to a \in {Base}_{r}$
52	37	a1i	$⊢ a \in {Base}_{r} \to 0_{Z} \in V$
53	49 50 51 52	fvmptd	$⊢ a \in {Base}_{r} \to (x \in {Base}_{r} ⟼ 0_{Z}) (a) = 0_{Z}$
54	53	adantl	$⊢ ((((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \land h : {Base}_{r} ⟶ {Base}_{Z}) \land a \in {Base}_{r}) \to (x \in {Base}_{r} ⟼ 0_{Z}) (a) = 0_{Z}$
55	48 54	eqtr4d	$⊢ ((((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \land h : {Base}_{r} ⟶ {Base}_{Z}) \land a \in {Base}_{r}) \to h (a) = (x \in {Base}_{r} ⟼ 0_{Z}) (a)$
56	36 39 55	eqfnfvd	$⊢ (((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \land h : {Base}_{r} ⟶ {Base}_{Z}) \to h = (x \in {Base}_{r} ⟼ 0_{Z})$
57	56	ex	$⊢ ((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \to (h : {Base}_{r} ⟶ {Base}_{Z} \to h = (x \in {Base}_{r} ⟼ 0_{Z}))$
58	34 57	syld	$⊢ ((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \to (h \in (r Hom (C) Z) \to h = (x \in {Base}_{r} ⟼ 0_{Z}))$
59	58	alrimiv	$⊢ ((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \to \forall h (h \in (r Hom (C) Z) \to h = (x \in {Base}_{r} ⟼ 0_{Z}))$
60	18 29 59	3jca	$⊢ ((φ \land r \in {Base}_{C}) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z)) \to ((x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r Hom (C) Z) \land \forall h (h \in (r Hom (C) Z) \to h = (x \in {Base}_{r} ⟼ 0_{Z})))$
61	17 60	mpdan	$⊢ (φ \land r \in {Base}_{C}) \to ((x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r Hom (C) Z) \land \forall h (h \in (r Hom (C) Z) \to h = (x \in {Base}_{r} ⟼ 0_{Z})))$
62		eleq1	$⊢ h = (x \in {Base}_{r} ⟼ 0_{Z}) \to (h \in (r Hom (C) Z) \leftrightarrow (x \in {Base}_{r} ⟼ 0_{Z}) \in (r Hom (C) Z))$
63	62	eqeu	$⊢ ((x \in {Base}_{r} ⟼ 0_{Z}) \in (r RingHom Z) \land (x \in {Base}_{r} ⟼ 0_{Z}) \in (r Hom (C) Z) \land \forall h (h \in (r Hom (C) Z) \to h = (x \in {Base}_{r} ⟼ 0_{Z}))) \to \exists! h h \in (r Hom (C) Z)$
64	61 63	syl	$⊢ (φ \land r \in {Base}_{C}) \to \exists! h h \in (r Hom (C) Z)$
65	64	ralrimiva	$⊢ φ \to \forall r \in {Base}_{C} \exists! h h \in (r Hom (C) Z)$
66	2	ringccat	$⊢ U \in V \to C \in Cat$
67	1 66	syl	$⊢ φ \to C \in Cat$
68	5 20 67 24	istermo	$⊢ φ \to (Z \in TermO (C) \leftrightarrow \forall r \in {Base}_{C} \exists! h h \in (r Hom (C) Z))$
69	65 68	mpbird	$⊢ φ \to Z \in TermO (C)$

Metamath Proof Explorer

Theorem zrtermoringc

Proof