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 e. RRExt -> ( ( RRHom ` R ) ` 0 ) = ( 0g ` R ) )

Proof

Step Hyp Ref Expression
1 zssq 
 |-  ZZ C_ QQ
2 0z 
 |-  0 e. ZZ
3 1 2 sselii 
 |-  0 e. QQ
4 simpl 
 |-  ( ( R e. RRExt /\ 0 e. QQ ) -> R e. RRExt )
5 simpr 
 |-  ( ( R e. RRExt /\ 0 e. QQ ) -> 0 e. QQ )
6 rrhqima 
 |-  ( ( R e. RRExt /\ 0 e. QQ ) -> ( ( RRHom ` R ) ` 0 ) = ( ( QQHom ` R ) ` 0 ) )
7 4 5 6 syl2anc 
 |-  ( ( R e. RRExt /\ 0 e. QQ ) -> ( ( RRHom ` R ) ` 0 ) = ( ( QQHom ` R ) ` 0 ) )
8 3 7 mpan2 
 |-  ( R e. RRExt -> ( ( RRHom ` R ) ` 0 ) = ( ( QQHom ` R ) ` 0 ) )
9 rrextdrg 
 |-  ( R e. RRExt -> R e. DivRing )
10 rrextchr 
 |-  ( R e. RRExt -> ( chr ` R ) = 0 )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 eqid 
 |-  ( /r ` R ) = ( /r ` R )
13 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
14 11 12 13 qqh0 
 |-  ( ( R e. DivRing /\ ( chr ` R ) = 0 ) -> ( ( QQHom ` R ) ` 0 ) = ( 0g ` R ) )
15 9 10 14 syl2anc 
 |-  ( R e. RRExt -> ( ( QQHom ` R ) ` 0 ) = ( 0g ` R ) )
16 8 15 eqtrd 
 |-  ( R e. RRExt -> ( ( RRHom ` R ) ` 0 ) = ( 0g ` R ) )