Metamath Proof Explorer

Theorem 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 ⊢ φ → U ∈ V
zrtermoringc.c ⊢ C = RingCat ⁡ U
zrtermoringc.z ⊢ φ → Z ∈ Ring ∖ NzRing
zrtermoringc.e ⊢ φ → Z ∈ U
Assertion zrtermoringc ⊢ φ → Z ∈ TermO ⁡ C

Proof

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