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
|- M = ( mulGrp ` R )
isrhm.n
|- N = ( mulGrp ` S )
Assertion isrhm
|- ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) ) )

Proof

Step Hyp Ref Expression
1 isrhm.m
 |-  M = ( mulGrp ` R )
2 isrhm.n
 |-  N = ( mulGrp ` S )
3 dfrhm2
 |-  RingHom = ( r e. Ring , s e. Ring |-> ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) )
4 3 elmpocl
 |-  ( F e. ( R RingHom S ) -> ( R e. Ring /\ S e. Ring ) )
5 oveq12
 |-  ( ( r = R /\ s = S ) -> ( r GrpHom s ) = ( R GrpHom S ) )
6 fveq2
 |-  ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
7 fveq2
 |-  ( s = S -> ( mulGrp ` s ) = ( mulGrp ` S ) )
8 6 7 oveqan12d
 |-  ( ( r = R /\ s = S ) -> ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) = ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
9 5 8 ineq12d
 |-  ( ( r = R /\ s = S ) -> ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) = ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )
10 ovex
 |-  ( R GrpHom S ) e. _V
11 10 inex1
 |-  ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) e. _V
12 9 3 11 ovmpoa
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( R RingHom S ) = ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )
13 12 eleq2d
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( F e. ( R RingHom S ) <-> F e. ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) ) )
14 elin
 |-  ( F e. ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) <-> ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )
15 1 2 oveq12i
 |-  ( M MndHom N ) = ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) )
16 15 eqcomi
 |-  ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) = ( M MndHom N )
17 16 eleq2i
 |-  ( F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) <-> F e. ( M MndHom N ) )
18 17 anbi2i
 |-  ( ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) <-> ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) )
19 14 18 bitri
 |-  ( F e. ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) <-> ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) )
20 13 19 bitrdi
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( F e. ( R RingHom S ) <-> ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) ) )
21 4 20 biadanii
 |-  ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) ) )