This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zrninitoringc

Description: The zero ring is not an initial object in the category of unital rings (if the universe contains at least one unital ring different from the zero ring). (Contributed by AV, 18-Apr-2020)

Ref Expression
Hypotheses zrtermoringc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
zrtermoringc.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
zrtermoringc.z ⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
zrtermoringc.e ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
zrninitoringc.e ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) 𝑟 ∈ NzRing )
Assertion zrninitoringc ( 𝜑 → 𝑍 ∉ ( InitO ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 zrtermoringc.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 zrtermoringc.c ⊢ 𝐶 = ( RingCat ‘ 𝑈 )
3 zrtermoringc.z ⊢ ( 𝜑 → 𝑍 ∈ ( Ring ∖ NzRing ) )
4 zrtermoringc.e ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
5 zrninitoringc.e ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) 𝑟 ∈ NzRing )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → 𝑈 ∈ 𝑉 )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 3 eldifad ⊢ ( 𝜑 → 𝑍 ∈ Ring )
10 4 9 elind ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑈 ∩ Ring ) )
11 2 6 1 ringcbas ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Ring ) )
12 10 11 eleqtrrd ⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝐶 ) )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → 𝑍 ∈ ( Base ‘ 𝐶 ) )
14 simplr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → 𝑟 ∈ ( Base ‘ 𝐶 ) )
15 2 6 7 8 13 14 ringchom ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) = ( 𝑍 RingHom 𝑟 ) )
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → 𝑍 ∈ ( Ring ∖ NzRing ) )
17 nrhmzr ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑟 ∈ NzRing ) → ( 𝑍 RingHom 𝑟 ) = ∅ )
18 16 17 sylan ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ( 𝑍 RingHom 𝑟 ) = ∅ )
19 15 18 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) = ∅ )
20 eq0 ⊢ ( ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) = ∅ ↔ ∀ ℎ ¬ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
21 19 20 sylib ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ∀ ℎ ¬ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
22 alnex ⊢ ( ∀ ℎ ¬ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ↔ ¬ ∃ ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
23 21 22 sylib ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ¬ ∃ ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
24 euex ⊢ ( ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) → ∃ ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
25 23 24 nsyl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑟 ∈ NzRing ) → ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
26 25 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑟 ∈ NzRing → ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
27 26 reximdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) 𝑟 ∈ NzRing → ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
28 5 27 mpd ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
29 rexnal ⊢ ( ∃ 𝑟 ∈ ( Base ‘ 𝐶 ) ¬ ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ↔ ¬ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
30 28 29 sylib ⊢ ( 𝜑 → ¬ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) )
31 df-nel ⊢ ( 𝑍 ∉ ( InitO ‘ 𝐶 ) ↔ ¬ 𝑍 ∈ ( InitO ‘ 𝐶 ) )
32 2 ringccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
33 1 32 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
34 6 8 33 12 isinito ⊢ ( 𝜑 → ( 𝑍 ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
35 34 notbid ⊢ ( 𝜑 → ( ¬ 𝑍 ∈ ( InitO ‘ 𝐶 ) ↔ ¬ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
36 31 35 bitrid ⊢ ( 𝜑 → ( 𝑍 ∉ ( InitO ‘ 𝐶 ) ↔ ¬ ∀ 𝑟 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑍 ( Hom ‘ 𝐶 ) 𝑟 ) ) )
37 30 36 mpbird ⊢ ( 𝜑 → 𝑍 ∉ ( InitO ‘ 𝐶 ) )