Metamath Proof Explorer


Theorem 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 ℝExt ℝHom R 0 = 0 R

Proof

Step Hyp Ref Expression
1 zssq
2 0z 0
3 1 2 sselii 0
4 simpl R ℝExt 0 R ℝExt
5 simpr R ℝExt 0 0
6 rrhqima R ℝExt 0 ℝHom R 0 = ℚHom R 0
7 4 5 6 syl2anc R ℝExt 0 ℝHom R 0 = ℚHom R 0
8 3 7 mpan2 R ℝExt ℝHom R 0 = ℚHom R 0
9 rrextdrg R ℝExt R DivRing
10 rrextchr R ℝExt 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 DivRing chr R = 0 ℚHom R 0 = 0 R
15 9 10 14 syl2anc R ℝExt ℚHom R 0 = 0 R
16 8 15 eqtrd R ℝExt ℝHom R 0 = 0 R