Metamath Proof Explorer

Theorem zrinitorngc

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

Ref Expression
Hypotheses zrinitorngc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
zrinitorngc.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
zrinitorngc.z ⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
zrinitorngc.e ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
Assertion zrinitorngc ( 𝜑 → 𝑍 ∈ ( InitO ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 zrinitorngc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 zrinitorngc.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
3 zrinitorngc.z ⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
4 zrinitorngc.e ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
5 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
6 2 5 1 rngcbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Rng ) )
7 6 eleq2d ⊢ ( 𝜑 → ( 𝑟 ∈ ( Base ‘ 𝐶 ) ↔ 𝑟 ∈ ( 𝑈 ∩ Rng ) ) )
8 elin ⊢ ( 𝑟 ∈ ( 𝑈 ∩ Rng ) ↔ ( 𝑟 ∈ 𝑈 ∧ 𝑟 ∈ Rng ) )
9 8 simprbi ⊢ ( 𝑟 ∈ ( 𝑈 ∩ Rng ) → 𝑟 ∈ Rng )
10 7 9 syl6bi ⊢ ( 𝜑 → ( 𝑟 ∈ ( Base ‘ 𝐶 ) → 𝑟 ∈ Rng ) )
11 10 imp ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑟 ∈ Rng )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑍 ∈ ( Ring ∖ NzRing ) )
13 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
14 eqid ⊢ ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑟 )
15 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) )
16 13 14 15 zrrnghm ⊢ ( ( 𝑟 ∈ Rng ∧ 𝑍 ∈ ( Ring ∖ NzRing ) ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) )
17 11 12 16 syl2anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) )
18 simpr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) )
19 1 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑈 ∈ 𝑉 )
20 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
21 eldifi ⊢ ( 𝑍 ∈ ( Ring ∖ NzRing ) → 𝑍 ∈ Ring )
22 ringrng ⊢ ( 𝑍 ∈ Ring → 𝑍 ∈ Rng )
23 3 21 22 3syl ⊢ ( 𝜑 → 𝑍 ∈ Rng )
24 4 23 elind ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑈 ∩ Rng ) )
25 24 6 eleqtrrd ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
27 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑟 ∈ ( Base ‘ 𝐶 ) )
28 2 5 19 20 26 27 rngchom ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) = ( 𝑍 RngHomo 𝑟 ) )
29 28 eqcomd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑍 RngHomo 𝑟 ) = ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
30 29 eleq2d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
31 30 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
32 28 eleq2d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ↔ ℎ ∈ ( 𝑍 RngHomo 𝑟 ) ) )
33 eqid ⊢ ( Base ‘ 𝑟 ) = ( Base ‘ 𝑟 )
34 13 33 rnghmf ⊢ ( ℎ ∈ ( 𝑍 RngHomo 𝑟 ) → ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) )
35 32 34 syl6bi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) )
36 35 imp ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) → ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) )
37 ffn ⊢ ( ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) → ℎ Fn ( Base ‘ 𝑍 ) )
38 37 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) ∧ ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) → ℎ Fn ( Base ‘ 𝑍 ) )
39 fvex ⊢ ( 0g ‘ 𝑟 ) ∈ V
40 39 15 fnmpti ⊢ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) Fn ( Base ‘ 𝑍 )
41 40 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) ∧ ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) Fn ( Base ‘ 𝑍 ) )
42 32 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) → ℎ ∈ ( 𝑍 RngHomo 𝑟 ) )
43 rnghmghm ⊢ ( ℎ ∈ ( 𝑍 RngHomo 𝑟 ) → ℎ ∈ ( 𝑍 GrpHom 𝑟 ) )
44 eqid ⊢ ( 0g ‘ 𝑍 ) = ( 0g ‘ 𝑍 )
45 44 14 ghmid ⊢ ( ℎ ∈ ( 𝑍 GrpHom 𝑟 ) → ( ℎ ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑟 ) )
46 42 43 45 3syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) → ( ℎ ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑟 ) )
47 46 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) ∧ ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑍 ) ) → ( ℎ ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑟 ) )
48 13 44 0ringbas ⊢ ( 𝑍 ∈ ( Ring ∖ NzRing ) → ( Base ‘ 𝑍 ) = { ( 0g ‘ 𝑍 ) } )
49 3 48 syl ⊢ ( 𝜑 → ( Base ‘ 𝑍 ) = { ( 0g ‘ 𝑍 ) } )
50 49 eleq2d ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝑍 ) ↔ 𝑎 ∈ { ( 0g ‘ 𝑍 ) } ) )
51 elsni ⊢ ( 𝑎 ∈ { ( 0g ‘ 𝑍 ) } → 𝑎 = ( 0g ‘ 𝑍 ) )
52 51 fveq2d ⊢ ( 𝑎 ∈ { ( 0g ‘ 𝑍 ) } → ( ℎ ‘ 𝑎 ) = ( ℎ ‘ ( 0g ‘ 𝑍 ) ) )
53 50 52 syl6bi ⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝑍 ) → ( ℎ ‘ 𝑎 ) = ( ℎ ‘ ( 0g ‘ 𝑍 ) ) ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑍 ) → ( ℎ ‘ 𝑎 ) = ( ℎ ‘ ( 0g ‘ 𝑍 ) ) ) )
55 54 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) ∧ ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑍 ) → ( ℎ ‘ 𝑎 ) = ( ℎ ‘ ( 0g ‘ 𝑍 ) ) ) )
56 55 imp ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) ∧ ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑍 ) ) → ( ℎ ‘ 𝑎 ) = ( ℎ ‘ ( 0g ‘ 𝑍 ) ) )
57 eqidd ⊢ ( 𝑎 ∈ ( Base ‘ 𝑍 ) → ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) )
58 eqidd ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑍 ) ∧ 𝑥 = 𝑎 ) → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑟 ) )
59 id ⊢ ( 𝑎 ∈ ( Base ‘ 𝑍 ) → 𝑎 ∈ ( Base ‘ 𝑍 ) )
60 39 a1i ⊢ ( 𝑎 ∈ ( Base ‘ 𝑍 ) → ( 0g ‘ 𝑟 ) ∈ V )
61 57 58 59 60 fvmptd ⊢ ( 𝑎 ∈ ( Base ‘ 𝑍 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ‘ 𝑎 ) = ( 0g ‘ 𝑟 ) )
62 61 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) ∧ ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑍 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ‘ 𝑎 ) = ( 0g ‘ 𝑟 ) )
63 47 56 62 3eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) ∧ ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑍 ) ) → ( ℎ ‘ 𝑎 ) = ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ‘ 𝑎 ) )
64 38 41 63 eqfnfvd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) ∧ ℎ : ( Base ‘ 𝑍 ) ⟶ ( Base ‘ 𝑟 ) ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) )
65 36 64 mpdan ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) )
66 65 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ) )
67 66 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ) → ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ) )
68 67 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ) → ∀ ℎ ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ) )
69 18 31 68 3jca ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ∧ ∀ ℎ ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ) ) )
70 17 69 mpdan ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ∧ ∀ ℎ ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ) ) )
71 eleq1 ⊢ ( ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) → ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
72 71 eqeu ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 RngHomo 𝑟 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ∧ ∀ ℎ ( ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑍 ) ↦ ( 0g ‘ 𝑟 ) ) ) ) → ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
73 70 72 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
74 73 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
75 2 rngccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
76 1 75 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
77 5 20 76 25 isinito ⊢ ( 𝜑 → ( 𝑍 ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
78 74 77 mpbird ⊢ ( 𝜑 → 𝑍 ∈ ( InitO ‘ 𝐶 ) )