Metamath Proof Explorer

Theorem isrnghm

Description: A function is a non-unital ring homomorphism iff it is a group homomorphism and preserves multiplication. (Contributed by AV, 22-Feb-2020)

Ref Expression
Hypotheses isrnghm.b 
|- B = ( Base ` R )
isrnghm.t 
|- .x. = ( .r ` R )
isrnghm.m 
|- .* = ( .r ` S )
Assertion isrnghm 
|- ( F e. ( R RngHom S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isrnghm.b 
 |-  B = ( Base ` R )
2 isrnghm.t 
 |-  .x. = ( .r ` R )
3 isrnghm.m 
 |-  .* = ( .r ` S )
4 rnghmrcl 
 |-  ( F e. ( R RngHom S ) -> ( R e. Rng /\ S e. Rng ) )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 eqid 
 |-  ( +g ` R ) = ( +g ` R )
7 eqid 
 |-  ( +g ` S ) = ( +g ` S )
8 1 2 3 5 6 7 rnghmval 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( R RngHom S ) = { f e. ( ( Base ` S ) ^m B ) | A. x e. B A. y e. B ( ( f ` ( x ( +g ` R ) y ) ) = ( ( f ` x ) ( +g ` S ) ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
9 8 eleq2d 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( F e. ( R RngHom S ) <-> F e. { f e. ( ( Base ` S ) ^m B ) | A. x e. B A. y e. B ( ( f ` ( x ( +g ` R ) y ) ) = ( ( f ` x ) ( +g ` S ) ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } ) )
10 fveq1 
 |-  ( f = F -> ( f ` ( x ( +g ` R ) y ) ) = ( F ` ( x ( +g ` R ) y ) ) )
11 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
12 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
13 11 12 oveq12d 
 |-  ( f = F -> ( ( f ` x ) ( +g ` S ) ( f ` y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) )
14 10 13 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x ( +g ` R ) y ) ) = ( ( f ` x ) ( +g ` S ) ( f ` y ) ) <-> ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) )
15 fveq1 
 |-  ( f = F -> ( f ` ( x .x. y ) ) = ( F ` ( x .x. y ) ) )
16 11 12 oveq12d 
 |-  ( f = F -> ( ( f ` x ) .* ( f ` y ) ) = ( ( F ` x ) .* ( F ` y ) ) )
17 15 16 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) <-> ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) )
18 14 17 anbi12d 
 |-  ( f = F -> ( ( ( f ` ( x ( +g ` R ) y ) ) = ( ( f ` x ) ( +g ` S ) ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) <-> ( ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
19 18 2ralbidv 
 |-  ( f = F -> ( A. x e. B A. y e. B ( ( f ` ( x ( +g ` R ) y ) ) = ( ( f ` x ) ( +g ` S ) ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) <-> A. x e. B A. y e. B ( ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
20 19 elrab 
 |-  ( F e. { f e. ( ( Base ` S ) ^m B ) | A. x e. B A. y e. B ( ( f ` ( x ( +g ` R ) y ) ) = ( ( f ` x ) ( +g ` S ) ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } <-> ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
21 r19.26-2 
 |-  ( A. x e. B A. y e. B ( ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) <-> ( A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) )
22 21 anbi2i 
 |-  ( ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) <-> ( F e. ( ( Base ` S ) ^m B ) /\ ( A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
23 anass 
 |-  ( ( ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) <-> ( F e. ( ( Base ` S ) ^m B ) /\ ( A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
24 22 23 bitr4i 
 |-  ( ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) <-> ( ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) )
25 1 5 6 7 isghm 
 |-  ( F e. ( R GrpHom S ) <-> ( ( R e. Grp /\ S e. Grp ) /\ ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) )
26 fvex 
 |-  ( Base ` S ) e. _V
27 1 fvexi 
 |-  B e. _V
28 26 27 pm3.2i 
 |-  ( ( Base ` S ) e. _V /\ B e. _V )
29 elmapg 
 |-  ( ( ( Base ` S ) e. _V /\ B e. _V ) -> ( F e. ( ( Base ` S ) ^m B ) <-> F : B --> ( Base ` S ) ) )
30 28 29 mp1i 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( F e. ( ( Base ` S ) ^m B ) <-> F : B --> ( Base ` S ) ) )
31 30 anbi1d 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) <-> ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) )
32 rngabl 
 |-  ( R e. Rng -> R e. Abel )
33 ablgrp 
 |-  ( R e. Abel -> R e. Grp )
34 32 33 syl 
 |-  ( R e. Rng -> R e. Grp )
35 rngabl 
 |-  ( S e. Rng -> S e. Abel )
36 ablgrp 
 |-  ( S e. Abel -> S e. Grp )
37 35 36 syl 
 |-  ( S e. Rng -> S e. Grp )
38 ibar 
 |-  ( ( R e. Grp /\ S e. Grp ) -> ( ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) <-> ( ( R e. Grp /\ S e. Grp ) /\ ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) ) )
39 34 37 38 syl2an 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) <-> ( ( R e. Grp /\ S e. Grp ) /\ ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) ) )
40 31 39 bitr2d 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( ( R e. Grp /\ S e. Grp ) /\ ( F : B --> ( Base ` S ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) <-> ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) )
41 25 40 bitr2id 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) <-> F e. ( R GrpHom S ) ) )
42 41 anbi1d 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) <-> ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
43 24 42 bitrid 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( F e. ( ( Base ` S ) ^m B ) /\ A. x e. B A. y e. B ( ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) <-> ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
44 20 43 bitrid 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( F e. { f e. ( ( Base ` S ) ^m B ) | A. x e. B A. y e. B ( ( f ` ( x ( +g ` R ) y ) ) = ( ( f ` x ) ( +g ` S ) ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } <-> ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
45 9 44 bitrd 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( F e. ( R RngHom S ) <-> ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )
46 4 45 biadanii 
 |-  ( F e. ( R RngHom S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. B A. y e. B ( F ` ( x .x. y ) ) = ( ( F ` x ) .* ( F ` y ) ) ) ) )