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

Metamath Proof Explorer

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 ‘ 𝑆 ) ) ) )