This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isrhm2d

Description: Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015)

Ref Expression
Hypotheses isrhmd.b 
|- B = ( Base ` R )
isrhmd.o 
|- .1. = ( 1r ` R )
isrhmd.n 
|- N = ( 1r ` S )
isrhmd.t 
|- .x. = ( .r ` R )
isrhmd.u 
|- .X. = ( .r ` S )
isrhmd.r 
|- ( ph -> R e. Ring )
isrhmd.s 
|- ( ph -> S e. Ring )
isrhmd.ho 
|- ( ph -> ( F ` .1. ) = N )
isrhmd.ht 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
isrhm2d.f 
|- ( ph -> F e. ( R GrpHom S ) )
Assertion isrhm2d 
|- ( ph -> F e. ( R RingHom S ) )

Proof

Step Hyp Ref Expression
1 isrhmd.b 
 |-  B = ( Base ` R )
2 isrhmd.o 
 |-  .1. = ( 1r ` R )
3 isrhmd.n 
 |-  N = ( 1r ` S )
4 isrhmd.t 
 |-  .x. = ( .r ` R )
5 isrhmd.u 
 |-  .X. = ( .r ` S )
6 isrhmd.r 
 |-  ( ph -> R e. Ring )
7 isrhmd.s 
 |-  ( ph -> S e. Ring )
8 isrhmd.ho 
 |-  ( ph -> ( F ` .1. ) = N )
9 isrhmd.ht 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
10 isrhm2d.f 
 |-  ( ph -> F e. ( R GrpHom S ) )
11 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
12 11 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
13 6 12 syl 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
14 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
15 14 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
16 7 15 syl 
 |-  ( ph -> ( mulGrp ` S ) e. Mnd )
17 eqid 
 |-  ( Base ` S ) = ( Base ` S )
18 1 17 ghmf 
 |-  ( F e. ( R GrpHom S ) -> F : B --> ( Base ` S ) )
19 10 18 syl 
 |-  ( ph -> F : B --> ( Base ` S ) )
20 9 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
21 11 2 ringidval 
 |-  .1. = ( 0g ` ( mulGrp ` R ) )
22 21 fveq2i 
 |-  ( F ` .1. ) = ( F ` ( 0g ` ( mulGrp ` R ) ) )
23 14 3 ringidval 
 |-  N = ( 0g ` ( mulGrp ` S ) )
24 8 22 23 3eqtr3g 
 |-  ( ph -> ( F ` ( 0g ` ( mulGrp ` R ) ) ) = ( 0g ` ( mulGrp ` S ) ) )
25 19 20 24 3jca 
 |-  ( ph -> ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) /\ ( F ` ( 0g ` ( mulGrp ` R ) ) ) = ( 0g ` ( mulGrp ` S ) ) ) )
26 11 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
27 14 17 mgpbas 
 |-  ( Base ` S ) = ( Base ` ( mulGrp ` S ) )
28 11 4 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
29 14 5 mgpplusg 
 |-  .X. = ( +g ` ( mulGrp ` S ) )
30 eqid 
 |-  ( 0g ` ( mulGrp ` R ) ) = ( 0g ` ( mulGrp ` R ) )
31 eqid 
 |-  ( 0g ` ( mulGrp ` S ) ) = ( 0g ` ( mulGrp ` S ) )
32 26 27 28 29 30 31 ismhm 
 |-  ( F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) <-> ( ( ( mulGrp ` R ) e. Mnd /\ ( mulGrp ` S ) e. Mnd ) /\ ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) /\ ( F ` ( 0g ` ( mulGrp ` R ) ) ) = ( 0g ` ( mulGrp ` S ) ) ) ) )
33 13 16 25 32 syl21anbrc 
 |-  ( ph -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
34 10 33 jca 
 |-  ( ph -> ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) )
35 11 14 isrhm 
 |-  ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) ) ) )
36 6 7 34 35 syl21anbrc 
 |-  ( ph -> F e. ( R RingHom S ) )