Metamath Proof Explorer

Theorem rhmval

Description: The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020)

Ref Expression
Assertion rhmval 
|- ( ( R e. Ring /\ S e. Ring ) -> ( R RingHom S ) = ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )

Proof

Step Hyp Ref Expression
1 dfrhm2 
 |-  RingHom = ( r e. Ring , s e. Ring |-> ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) )
2 1 a1i 
 |-  ( ( R e. Ring /\ S e. Ring ) -> RingHom = ( r e. Ring , s e. Ring |-> ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) ) )
3 oveq12 
 |-  ( ( r = R /\ s = S ) -> ( r GrpHom s ) = ( R GrpHom S ) )
4 fveq2 
 |-  ( r = R -> ( mulGrp ` r ) = ( mulGrp ` R ) )
5 fveq2 
 |-  ( s = S -> ( mulGrp ` s ) = ( mulGrp ` S ) )
6 4 5 oveqan12d 
 |-  ( ( r = R /\ s = S ) -> ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) = ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
7 3 6 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 ) ) ) )
8 7 adantl 
 |-  ( ( ( R e. Ring /\ S e. Ring ) /\ ( r = R /\ s = S ) ) -> ( ( r GrpHom s ) i^i ( ( mulGrp ` r ) MndHom ( mulGrp ` s ) ) ) = ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )
9 simpl 
 |-  ( ( R e. Ring /\ S e. Ring ) -> R e. Ring )
10 simpr 
 |-  ( ( R e. Ring /\ S e. Ring ) -> S e. Ring )
11 ovex 
 |-  ( R GrpHom S ) e. _V
12 11 inex1 
 |-  ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) e. _V
13 12 a1i 
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) e. _V )
14 2 8 9 10 13 ovmpod 
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( R RingHom S ) = ( ( R GrpHom S ) i^i ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )