Theorem zrhval

Description: Define the unique homomorphism from the integers to a ring or field. (Contributed by Mario Carneiro, 13-Jun-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Hypothesis	zrhval.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
Assertion	zrhval	⊢ 𝐿 = ∪ ( ℤring RingHom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		zrhval.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2		oveq2	⊢ ( 𝑟 = 𝑅 → ( ℤring RingHom 𝑟 ) = ( ℤring RingHom 𝑅 ) )
3	2	unieqd	⊢ ( 𝑟 = 𝑅 → ∪ ( ℤring RingHom 𝑟 ) = ∪ ( ℤring RingHom 𝑅 ) )
4		df-zrh	⊢ ℤRHom = ( 𝑟 ∈ V ↦ ∪ ( ℤring RingHom 𝑟 ) )
5		ovex	⊢ ( ℤring RingHom 𝑅 ) ∈ V
6	5	uniex	⊢ ∪ ( ℤring RingHom 𝑅 ) ∈ V
7	3 4 6	fvmpt	⊢ ( 𝑅 ∈ V → ( ℤRHom ‘ 𝑅 ) = ∪ ( ℤring RingHom 𝑅 ) )
8		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( ℤRHom ‘ 𝑅 ) = ∅ )
9		dfrhm2	⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )
10	9	reldmmpo	⊢ Rel dom RingHom
11	10	ovprc2	⊢ ( ¬ 𝑅 ∈ V → ( ℤring RingHom 𝑅 ) = ∅ )
12	11	unieqd	⊢ ( ¬ 𝑅 ∈ V → ∪ ( ℤring RingHom 𝑅 ) = ∪ ∅ )
13		uni0	⊢ ∪ ∅ = ∅
14	12 13	eqtrdi	⊢ ( ¬ 𝑅 ∈ V → ∪ ( ℤring RingHom 𝑅 ) = ∅ )
15	8 14	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( ℤRHom ‘ 𝑅 ) = ∪ ( ℤring RingHom 𝑅 ) )
16	7 15	pm2.61i	⊢ ( ℤRHom ‘ 𝑅 ) = ∪ ( ℤring RingHom 𝑅 )
17	1 16	eqtri	⊢ 𝐿 = ∪ ( ℤring RingHom 𝑅 )