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

Metamath Proof Explorer

Theorem nrhmzr

Description: There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020)

Ref Expression
Assertion nrhmzr ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( 𝑍 RingHom 𝑅 ) = ∅ )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
2 eqid ⊢ ( 0g ‘ 𝑍 ) = ( 0g ‘ 𝑍 )
3 eqid ⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
4 1 2 3 0ring1eq0 ⊢ ( 𝑍 ∈ ( Ring ∖ NzRing ) → ( 1r ‘ 𝑍 ) = ( 0g ‘ 𝑍 ) )
5 4 adantr ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( 1r ‘ 𝑍 ) = ( 0g ‘ 𝑍 ) )
6 5 adantr ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) → ( 1r ‘ 𝑍 ) = ( 0g ‘ 𝑍 ) )
7 6 eqcomd ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) → ( 0g ‘ 𝑍 ) = ( 1r ‘ 𝑍 ) )
8 7 fveq2d ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) → ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 𝑓 ‘ ( 1r ‘ 𝑍 ) ) )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 3 9 rhm1 ⊢ ( 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) → ( 𝑓 ‘ ( 1r ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) )
11 10 adantl ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) → ( 𝑓 ‘ ( 1r ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) )
12 8 11 eqtrd ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) → ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) )
13 rhmghm ⊢ ( 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) → 𝑓 ∈ ( 𝑍 GrpHom 𝑅 ) )
14 13 adantl ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) → 𝑓 ∈ ( 𝑍 GrpHom 𝑅 ) )
15 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
16 2 15 ghmid ⊢ ( 𝑓 ∈ ( 𝑍 GrpHom 𝑅 ) → ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) )
17 14 16 syl ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) → ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) )
18 12 17 jca ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) )
19 18 ralrimiva ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ∀ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) )
20 9 15 nzrnz ⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
21 20 necomd ⊢ ( 𝑅 ∈ NzRing → ( 0g ‘ 𝑅 ) ≠ ( 1r ‘ 𝑅 ) )
22 21 adantl ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( 0g ‘ 𝑅 ) ≠ ( 1r ‘ 𝑅 ) )
23 22 adantr ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ≠ ( 1r ‘ 𝑅 ) )
24 neeq1 ⊢ ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) ↔ ( 0g ‘ 𝑅 ) ≠ ( 1r ‘ 𝑅 ) ) )
25 24 adantl ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) ↔ ( 0g ‘ 𝑅 ) ≠ ( 1r ‘ 𝑅 ) ) )
26 23 25 mpbird ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) )
27 26 orcd ⊢ ( ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) ∨ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
28 27 expcom ⊢ ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) → ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) ∨ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 0g ‘ 𝑅 ) ) ) )
29 olc ⊢ ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 0g ‘ 𝑅 ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) ∨ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
30 29 a1d ⊢ ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 0g ‘ 𝑅 ) → ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) ∨ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 0g ‘ 𝑅 ) ) ) )
31 28 30 pm2.61ine ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) ∨ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 0g ‘ 𝑅 ) ) )
32 neorian ⊢ ( ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 1r ‘ 𝑅 ) ∨ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) ≠ ( 0g ‘ 𝑅 ) ) ↔ ¬ ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) )
33 31 32 sylib ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ¬ ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) )
34 con3 ⊢ ( ( 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) ) → ( ¬ ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) → ¬ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) )
35 33 34 syl5com ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( ( 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) ) → ¬ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) )
36 35 alimdv ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( ∀ 𝑓 ( 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) ) → ∀ 𝑓 ¬ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ) )
37 df-ral ⊢ ( ∀ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) ↔ ∀ 𝑓 ( 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) → ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) ) )
38 eq0 ⊢ ( ( 𝑍 RingHom 𝑅 ) = ∅ ↔ ∀ 𝑓 ¬ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) )
39 36 37 38 3imtr4g ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( ∀ 𝑓 ∈ ( 𝑍 RingHom 𝑅 ) ( ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 1r ‘ 𝑅 ) ∧ ( 𝑓 ‘ ( 0g ‘ 𝑍 ) ) = ( 0g ‘ 𝑅 ) ) → ( 𝑍 RingHom 𝑅 ) = ∅ ) )
40 19 39 mpd ⊢ ( ( 𝑍 ∈ ( Ring ∖ NzRing ) ∧ 𝑅 ∈ NzRing ) → ( 𝑍 RingHom 𝑅 ) = ∅ )