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 𝑁 ) ) ) )