Metamath Proof Explorer

Theorem zrinitorngc

Description: The zero ring is an initial object in the category of non-unital rings. (Contributed by AV, 18-Apr-2020)

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