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 syl6bb 
 |-  ( ( 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 ) ) ) )