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	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to Z RingHom R = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
2		eqid	$⊢ 0_{Z} = 0_{Z}$
3		eqid	$⊢ 1_{Z} = 1_{Z}$
4	1 2 3	0ring1eq0	$⊢ Z \in (Ring ∖ NzRing) \to 1_{Z} = 0_{Z}$
5	4	adantr	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to 1_{Z} = 0_{Z}$
6	5	adantr	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f \in (Z RingHom R)) \to 1_{Z} = 0_{Z}$
7	6	eqcomd	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f \in (Z RingHom R)) \to 0_{Z} = 1_{Z}$
8	7	fveq2d	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f \in (Z RingHom R)) \to f (0_{Z}) = f (1_{Z})$
9		eqid	$⊢ 1_{R} = 1_{R}$
10	3 9	rhm1	$⊢ f \in (Z RingHom R) \to f (1_{Z}) = 1_{R}$
11	10	adantl	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f \in (Z RingHom R)) \to f (1_{Z}) = 1_{R}$
12	8 11	eqtrd	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f \in (Z RingHom R)) \to f (0_{Z}) = 1_{R}$
13		rhmghm	$⊢ f \in (Z RingHom R) \to f \in (Z GrpHom R)$
14	13	adantl	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f \in (Z RingHom R)) \to f \in (Z GrpHom R)$
15		eqid	$⊢ 0_{R} = 0_{R}$
16	2 15	ghmid	$⊢ f \in (Z GrpHom R) \to f (0_{Z}) = 0_{R}$
17	14 16	syl	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f \in (Z RingHom R)) \to f (0_{Z}) = 0_{R}$
18	12 17	jca	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f \in (Z RingHom R)) \to (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R})$
19	18	ralrimiva	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to \forall f \in (Z RingHom R) (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R})$
20	9 15	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
21	20	necomd	$⊢ R \in NzRing \to 0_{R} \neq 1_{R}$
22	21	adantl	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to 0_{R} \neq 1_{R}$
23	22	adantr	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f (0_{Z}) = 0_{R}) \to 0_{R} \neq 1_{R}$
24		neeq1	$⊢ f (0_{Z}) = 0_{R} \to (f (0_{Z}) \neq 1_{R} \leftrightarrow 0_{R} \neq 1_{R})$
25	24	adantl	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f (0_{Z}) = 0_{R}) \to (f (0_{Z}) \neq 1_{R} \leftrightarrow 0_{R} \neq 1_{R})$
26	23 25	mpbird	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f (0_{Z}) = 0_{R}) \to f (0_{Z}) \neq 1_{R}$
27	26	orcd	$⊢ ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \land f (0_{Z}) = 0_{R}) \to (f (0_{Z}) \neq 1_{R} \lor f (0_{Z}) \neq 0_{R})$
28	27	expcom	$⊢ f (0_{Z}) = 0_{R} \to ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \to (f (0_{Z}) \neq 1_{R} \lor f (0_{Z}) \neq 0_{R}))$
29		olc	$⊢ f (0_{Z}) \neq 0_{R} \to (f (0_{Z}) \neq 1_{R} \lor f (0_{Z}) \neq 0_{R})$
30	29	a1d	$⊢ f (0_{Z}) \neq 0_{R} \to ((Z \in (Ring ∖ NzRing) \land R \in NzRing) \to (f (0_{Z}) \neq 1_{R} \lor f (0_{Z}) \neq 0_{R}))$
31	28 30	pm2.61ine	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to (f (0_{Z}) \neq 1_{R} \lor f (0_{Z}) \neq 0_{R})$
32		neorian	$⊢ (f (0_{Z}) \neq 1_{R} \lor f (0_{Z}) \neq 0_{R}) \leftrightarrow \neg (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R})$
33	31 32	sylib	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to \neg (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R})$
34		con3	$⊢ (f \in (Z RingHom R) \to (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R})) \to (\neg (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R}) \to \neg f \in (Z RingHom R))$
35	33 34	syl5com	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to ((f \in (Z RingHom R) \to (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R})) \to \neg f \in (Z RingHom R))$
36	35	alimdv	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to (\forall f (f \in (Z RingHom R) \to (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R})) \to \forall f \neg f \in (Z RingHom R))$
37		df-ral	$⊢ \forall f \in (Z RingHom R) (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R}) \leftrightarrow \forall f (f \in (Z RingHom R) \to (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R}))$
38		eq0	$⊢ Z RingHom R = \emptyset \leftrightarrow \forall f \neg f \in (Z RingHom R)$
39	36 37 38	3imtr4g	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to (\forall f \in (Z RingHom R) (f (0_{Z}) = 1_{R} \land f (0_{Z}) = 0_{R}) \to Z RingHom R = \emptyset)$
40	19 39	mpd	$⊢ (Z \in (Ring ∖ NzRing) \land R \in NzRing) \to Z RingHom R = \emptyset$

Metamath Proof Explorer

Theorem nrhmzr

Proof