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

Metamath Proof Explorer

Theorem zrhrhmb

Description: The ZRHom homomorphism is the unique ring homomorphism from ZZ . (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 12-Jun-2019)

Ref Expression
Hypothesis zrhval.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion zrhrhmb ( 𝑅 ∈ Ring → ( 𝐹 ∈ ( ℤring RingHom 𝑅 ) ↔ 𝐹 = 𝐿 ) )

Proof

Step Hyp Ref Expression
1 zrhval.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2 eqid ⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
3 eqid ⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
4 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
5 2 3 4 mulgrhm2 ⊢ ( 𝑅 ∈ Ring → ( ℤring RingHom 𝑅 ) = { ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) } )
6 1 2 4 zrhval2 ⊢ ( 𝑅 ∈ Ring → 𝐿 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
7 6 sneqd ⊢ ( 𝑅 ∈ Ring → { 𝐿 } = { ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) } )
8 5 7 eqtr4d ⊢ ( 𝑅 ∈ Ring → ( ℤring RingHom 𝑅 ) = { 𝐿 } )
9 8 eleq2d ⊢ ( 𝑅 ∈ Ring → ( 𝐹 ∈ ( ℤring RingHom 𝑅 ) ↔ 𝐹 ∈ { 𝐿 } ) )
10 1 fvexi ⊢ 𝐿 ∈ V
11 10 elsn2 ⊢ ( 𝐹 ∈ { 𝐿 } ↔ 𝐹 = 𝐿 )
12 9 11 bitrdi ⊢ ( 𝑅 ∈ Ring → ( 𝐹 ∈ ( ℤring RingHom 𝑅 ) ↔ 𝐹 = 𝐿 ) )