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

Proof

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