Theorem rhmval

Description: The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020)

	Ref	Expression
Assertion	rhmval	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝑅 RingHom 𝑆 ) = ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfrhm2	⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )
2	1	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) ) )
3		oveq12	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑟 GrpHom 𝑠 ) = ( 𝑅 GrpHom 𝑆 ) )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
5		fveq2	⊢ ( 𝑠 = 𝑆 → ( mulGrp ‘ 𝑠 ) = ( mulGrp ‘ 𝑆 ) )
6	4 5	oveqan12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) = ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) )
7	3 6	ineq12d	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) = ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )
8	7	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) ) → ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) = ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )
9		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → 𝑅 ∈ Ring )
10		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → 𝑆 ∈ Ring )
11		ovex	⊢ ( 𝑅 GrpHom 𝑆 ) ∈ V
12	11	inex1	⊢ ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ∈ V
13	12	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ∈ V )
14	2 8 9 10 13	ovmpod	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝑅 RingHom 𝑆 ) = ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )