Metamath Proof Explorer


Theorem isrhm

Description: A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypotheses isrhm.m 𝑀 = ( mulGrp ‘ 𝑅 )
isrhm.n 𝑁 = ( mulGrp ‘ 𝑆 )
Assertion isrhm ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 isrhm.m 𝑀 = ( mulGrp ‘ 𝑅 )
2 isrhm.n 𝑁 = ( mulGrp ‘ 𝑆 )
3 dfrhm2 RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )
4 3 elmpocl ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) )
5 oveq12 ( ( 𝑟 = 𝑅𝑠 = 𝑆 ) → ( 𝑟 GrpHom 𝑠 ) = ( 𝑅 GrpHom 𝑆 ) )
6 fveq2 ( 𝑟 = 𝑅 → ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑅 ) )
7 fveq2 ( 𝑠 = 𝑆 → ( mulGrp ‘ 𝑠 ) = ( mulGrp ‘ 𝑆 ) )
8 6 7 oveqan12d ( ( 𝑟 = 𝑅𝑠 = 𝑆 ) → ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) = ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) )
9 5 8 ineq12d ( ( 𝑟 = 𝑅𝑠 = 𝑆 ) → ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) = ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )
10 ovex ( 𝑅 GrpHom 𝑆 ) ∈ V
11 10 inex1 ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ∈ V
12 9 3 11 ovmpoa ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝑅 RingHom 𝑆 ) = ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )
13 12 eleq2d ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ↔ 𝐹 ∈ ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ) )
14 elin ( 𝐹 ∈ ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) )
15 1 2 oveq12i ( 𝑀 MndHom 𝑁 ) = ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) )
16 15 eqcomi ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) = ( 𝑀 MndHom 𝑁 )
17 16 eleq2i ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ↔ 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )
18 17 anbi2i ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ) )
19 14 18 bitri ( 𝐹 ∈ ( ( 𝑅 GrpHom 𝑆 ) ∩ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ) )
20 13 19 bitrdi ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) → ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ) ) )
21 4 20 biadanii ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ) ) )