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 ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
zrinitorngc.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
zrinitorngc.z ⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
zrinitorngc.e ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
Assertion zrtermorngc ( 𝜑 → 𝑍 ∈ ( TermO ‘ 𝐶 ) )

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 c0rnghm ⊢ ( ( 𝑟 ∈ 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 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑟 ∈ ( Base ‘ 𝐶 ) )
22 eldifi ⊢ ( 𝑍 ∈ ( Ring ∖ NzRing ) → 𝑍 ∈ Ring )
23 ringrng ⊢ ( 𝑍 ∈ Ring → 𝑍 ∈ Rng )
24 3 22 23 3syl ⊢ ( 𝜑 → 𝑍 ∈ Rng )
25 4 24 elind ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑈 ∩ Rng ) )
26 25 6 eleqtrrd ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
28 2 5 19 20 21 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 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) → ( ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) → ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) ) )
37 ffn ⊢ ( ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) → ℎ Fn ( Base ‘ 𝑟 ) )
38 37 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) ∧ ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) ) → ℎ Fn ( Base ‘ 𝑟 ) )
39 fvex ⊢ ( 0g ‘ 𝑍 ) ∈ V
40 39 15 fnmpti ⊢ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) Fn ( Base ‘ 𝑟 )
41 40 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) ∧ ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) Fn ( Base ‘ 𝑟 ) )
42 33 14 0ringbas ⊢ ( 𝑍 ∈ ( Ring ∖ NzRing ) → ( Base ‘ 𝑍 ) = { ( 0g ‘ 𝑍 ) } )
43 3 42 syl ⊢ ( 𝜑 → ( Base ‘ 𝑍 ) = { ( 0g ‘ 𝑍 ) } )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( Base ‘ 𝑍 ) = { ( 0g ‘ 𝑍 ) } )
45 44 feq3d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) ↔ ℎ : ( Base ‘ 𝑟 ) ⟶ { ( 0g ‘ 𝑍 ) } ) )
46 fvconst ⊢ ( ( ℎ : ( Base ‘ 𝑟 ) ⟶ { ( 0g ‘ 𝑍 ) } ∧ 𝑎 ∈ ( Base ‘ 𝑟 ) ) → ( ℎ ‘ 𝑎 ) = ( 0g ‘ 𝑍 ) )
47 46 ex ⊢ ( ℎ : ( Base ‘ 𝑟 ) ⟶ { ( 0g ‘ 𝑍 ) } → ( 𝑎 ∈ ( Base ‘ 𝑟 ) → ( ℎ ‘ 𝑎 ) = ( 0g ‘ 𝑍 ) ) )
48 45 47 syl6bi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) → ( 𝑎 ∈ ( Base ‘ 𝑟 ) → ( ℎ ‘ 𝑎 ) = ( 0g ‘ 𝑍 ) ) ) )
49 48 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) → ( ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) → ( 𝑎 ∈ ( Base ‘ 𝑟 ) → ( ℎ ‘ 𝑎 ) = ( 0g ‘ 𝑍 ) ) ) )
50 49 imp31 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) ∧ ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑟 ) ) → ( ℎ ‘ 𝑎 ) = ( 0g ‘ 𝑍 ) )
51 eqidd ⊢ ( 𝑎 ∈ ( Base ‘ 𝑟 ) → ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) )
52 eqidd ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑟 ) ∧ 𝑥 = 𝑎 ) → ( 0g ‘ 𝑍 ) = ( 0g ‘ 𝑍 ) )
53 id ⊢ ( 𝑎 ∈ ( Base ‘ 𝑟 ) → 𝑎 ∈ ( Base ‘ 𝑟 ) )
54 39 a1i ⊢ ( 𝑎 ∈ ( Base ‘ 𝑟 ) → ( 0g ‘ 𝑍 ) ∈ V )
55 51 52 53 54 fvmptd ⊢ ( 𝑎 ∈ ( Base ‘ 𝑟 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ‘ 𝑎 ) = ( 0g ‘ 𝑍 ) )
56 55 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) ∧ ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑟 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ‘ 𝑎 ) = ( 0g ‘ 𝑍 ) )
57 50 56 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) ∧ ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑟 ) ) → ( ℎ ‘ 𝑎 ) = ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ‘ 𝑎 ) )
58 38 41 57 eqfnfvd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) ∧ ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) )
59 58 ex ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) → ( ℎ : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑍 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ) )
60 36 59 syld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) → ( ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ) )
61 60 alrimiv ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) → ∀ ℎ ( ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ) )
62 18 31 61 3jca ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) ∧ ∀ ℎ ( ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ) ) )
63 17 62 mpdan ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) ∧ ∀ ℎ ( ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ) ) )
64 eleq1 ⊢ ( ℎ = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) → ( ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) ) )
65 64 eqeu ⊢ ( ( ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 RngHomo 𝑍 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) ∧ ∀ ℎ ( ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) → ℎ = ( 𝑥 ∈ ( Base ‘ 𝑟 ) ↦ ( 0g ‘ 𝑍 ) ) ) ) → ∃! ℎ ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) )
66 63 65 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ∃! ℎ ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) )
67 66 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) )
68 2 rngccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
69 1 68 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
70 5 20 69 26 istermo ⊢ ( 𝜑 → ( 𝑍 ∈ ( TermO ‘ 𝐶 ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑟 ( Hom ‘ 𝐶 ) 𝑍 ) ) )
71 67 70 mpbird ⊢ ( 𝜑 → 𝑍 ∈ ( TermO ‘ 𝐶 ) )