Theorem zrhval2

Description: Alternate value of the ZRHom homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	zrhval.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	zrhval2.m	⊢ · = ( .g ‘ 𝑅 )
	zrhval2.1	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	zrhval2	⊢ ( 𝑅 ∈ Ring → 𝐿 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2		zrhval2.m	⊢ · = ( .g ‘ 𝑅 )
3		zrhval2.1	⊢ 1 = ( 1r ‘ 𝑅 )
4	1	zrhval	⊢ 𝐿 = ∪ ( ℤring RingHom 𝑅 )
5		eqid	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
6	2 5 3	mulgrhm2	⊢ ( 𝑅 ∈ Ring → ( ℤring RingHom 𝑅 ) = { ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) } )
7	6	unieqd	⊢ ( 𝑅 ∈ Ring → ∪ ( ℤring RingHom 𝑅 ) = ∪ { ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) } )
8		zex	⊢ ℤ ∈ V
9	8	mptex	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) ∈ V
10	9	unisn	⊢ ∪ { ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) } = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) )
11	7 10	eqtrdi	⊢ ( 𝑅 ∈ Ring → ∪ ( ℤring RingHom 𝑅 ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )
12	4 11	syl5eq	⊢ ( 𝑅 ∈ Ring → 𝐿 = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 1 ) ) )