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 ( 𝑅 ∈ ℝExt → ( ( ℝHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 zssq ⊢ ℤ ⊆ ℚ
2 0z ⊢ 0 ∈ ℤ
3 1 2 sselii ⊢ 0 ∈ ℚ
4 simpl ⊢ ( ( 𝑅 ∈ ℝExt ∧ 0 ∈ ℚ ) → 𝑅 ∈ ℝExt )
5 simpr ⊢ ( ( 𝑅 ∈ ℝExt ∧ 0 ∈ ℚ ) → 0 ∈ ℚ )
6 rrhqima ⊢ ( ( 𝑅 ∈ ℝExt ∧ 0 ∈ ℚ ) → ( ( ℝHom ‘ 𝑅 ) ‘ 0 ) = ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) )
7 4 5 6 syl2anc ⊢ ( ( 𝑅 ∈ ℝExt ∧ 0 ∈ ℚ ) → ( ( ℝHom ‘ 𝑅 ) ‘ 0 ) = ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) )
8 3 7 mpan2 ⊢ ( 𝑅 ∈ ℝExt → ( ( ℝHom ‘ 𝑅 ) ‘ 0 ) = ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) )
9 rrextdrg ⊢ ( 𝑅 ∈ ℝExt → 𝑅 ∈ DivRing )
10 rrextchr ⊢ ( 𝑅 ∈ ℝExt → ( chr ‘ 𝑅 ) = 0 )
11 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 eqid ⊢ ( /r ‘ 𝑅 ) = ( /r ‘ 𝑅 )
13 eqid ⊢ ( ℤRHom ‘ 𝑅 ) = ( ℤRHom ‘ 𝑅 )
14 11 12 13 qqh0 ⊢ ( ( 𝑅 ∈ DivRing ∧ ( chr ‘ 𝑅 ) = 0 ) → ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
15 9 10 14 syl2anc ⊢ ( 𝑅 ∈ ℝExt → ( ( ℚHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )
16 8 15 eqtrd ⊢ ( 𝑅 ∈ ℝExt → ( ( ℝHom ‘ 𝑅 ) ‘ 0 ) = ( 0g ‘ 𝑅 ) )