Theorem zrhrhmb

Description: The ZRHom homomorphism is the unique ring homomorphism from Z . (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 𝑅 ) ↔ 𝐹 = 𝐿 ) )