Metamath Proof Explorer

Theorem zrtermorngc

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

Ref Expression
Hypotheses zrinitorngc.u ⊢ φ → U ∈ V
zrinitorngc.c ⊢ C = RngCat ⁡ U
zrinitorngc.z ⊢ φ → Z ∈ Ring ∖ NzRing
zrinitorngc.e ⊢ φ → Z ∈ U
Assertion zrtermorngc ⊢ φ → Z ∈ TermO ⁡ C

Proof

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