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

Metamath Proof Explorer

Theorem zrh0

Description: Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015)

Step	Hyp	Ref	Expression
1		zrh0.l	$⊢ L = ℤRHom (R)$
2		zrh0.z	$⊢ \underset{˙}{0} = 0_{R}$
3	1	zrhrhm	$⊢ R \in Ring \to L \in (ℤ_{ring} RingHom R)$
4		rhmghm	$⊢ L \in (ℤ_{ring} RingHom R) \to L \in (ℤ_{ring} GrpHom R)$
5		zring0	$⊢ 0 = 0_{ℤ_{ring}}$
6	5 2	ghmid	$⊢ L \in (ℤ_{ring} GrpHom R) \to L (0) = \underset{˙}{0}$
7	3 4 6	3syl	$⊢ R \in Ring \to L (0) = \underset{˙}{0}$