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 𝑅 ) = ∅ )