rrh0

Description: The image of 0 by the RRHom homomorphism is the ring's zero. (Contributed by Thierry Arnoux, 22-Oct-2017)

		Ref	Expression
	Assertion	rrh0	$⊢ R \in ℝExt \to ℝHom (R) (0) = 0_{R}$

Step	Hyp	Ref	Expression
1		zssq	$⊢ ℤ \subseteq ℚ$
2		0z	$⊢ 0 \in ℤ$
3	1 2	sselii	$⊢ 0 \in ℚ$
4		simpl	$⊢ (R \in ℝExt \land 0 \in ℚ) \to R \in ℝExt$
5		simpr	$⊢ (R \in ℝExt \land 0 \in ℚ) \to 0 \in ℚ$
6		rrhqima	$⊢ (R \in ℝExt \land 0 \in ℚ) \to ℝHom (R) (0) = ℚHom (R) (0)$
7	4 5 6	syl2anc	$⊢ (R \in ℝExt \land 0 \in ℚ) \to ℝHom (R) (0) = ℚHom (R) (0)$
8	3 7	mpan2	$⊢ R \in ℝExt \to ℝHom (R) (0) = ℚHom (R) (0)$
9		rrextdrg	$⊢ R \in ℝExt \to R \in DivRing$
10		rrextchr	$⊢ R \in ℝExt \to chr (R) = 0$
11		eqid	$⊢ {Base}_{R} = {Base}_{R}$
12		eqid	$⊢ /_{r} (R) = /_{r} (R)$
13		eqid	$⊢ ℤRHom (R) = ℤRHom (R)$
14	11 12 13	qqh0	$⊢ (R \in DivRing \land chr (R) = 0) \to ℚHom (R) (0) = 0_{R}$
15	9 10 14	syl2anc	$⊢ R \in ℝExt \to ℚHom (R) (0) = 0_{R}$
16	8 15	eqtrd	$⊢ R \in ℝExt \to ℝHom (R) (0) = 0_{R}$

Metamath Proof Explorer