Metamath Proof Explorer

Theorem isrhm0

Description: The predicate "is a ring homomorphism from R to S ". (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by AV, 24-Jul-2026)

Ref Expression
Hypotheses rhmval0.b 
|- B = ( Base ` R )
rhmval0.c 
|- C = ( Base ` S )
rhmval0.1 
|- .1. = ( 1r ` R )
rhmval0.i 
|- N = ( 1r ` S )
rhmval0.m 
|- .x. = ( .r ` R )
rhmval0.n 
|- .X. = ( .r ` S )
rhmval0.p 
|- .+ = ( +g ` R )
rhmval0.q 
|- .+^ = ( +g ` S )
Assertion isrhm0 
|- ( ( R e. Ring /\ S e. Ring ) -> ( F e. ( R RingHom S ) <-> ( F : B --> C /\ ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rhmval0.b 
 |-  B = ( Base ` R )
2 rhmval0.c 
 |-  C = ( Base ` S )
3 rhmval0.1 
 |-  .1. = ( 1r ` R )
4 rhmval0.i 
 |-  N = ( 1r ` S )
5 rhmval0.m 
 |-  .x. = ( .r ` R )
6 rhmval0.n 
 |-  .X. = ( .r ` S )
7 rhmval0.p 
 |-  .+ = ( +g ` R )
8 rhmval0.q 
 |-  .+^ = ( +g ` S )
9 1 2 3 4 5 6 7 8 rhmval0 
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( R RingHom S ) = { f e. ( C ^m B ) | ( ( f ` .1. ) = N /\ A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } )
10 9 eleq2d 
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( F e. ( R RingHom S ) <-> F e. { f e. ( C ^m B ) | ( ( f ` .1. ) = N /\ A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } ) )
11 2 fvexi 
 |-  C e. _V
12 1 fvexi 
 |-  B e. _V
13 11 12 elmap 
 |-  ( F e. ( C ^m B ) <-> F : B --> C )
14 13 anbi1i 
 |-  ( ( F e. ( C ^m B ) /\ ( ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) ) <-> ( F : B --> C /\ ( ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) ) )
15 fveq1 
 |-  ( f = F -> ( f ` .1. ) = ( F ` .1. ) )
16 15 eqeq1d 
 |-  ( f = F -> ( ( f ` .1. ) = N <-> ( F ` .1. ) = N ) )
17 fveq1 
 |-  ( f = F -> ( f ` ( x .+ y ) ) = ( F ` ( x .+ y ) ) )
18 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
19 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
20 18 19 oveq12d 
 |-  ( f = F -> ( ( f ` x ) .+^ ( f ` y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )
21 17 20 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) <-> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) )
22 fveq1 
 |-  ( f = F -> ( f ` ( x .x. y ) ) = ( F ` ( x .x. y ) ) )
23 18 19 oveq12d 
 |-  ( f = F -> ( ( f ` x ) .X. ( f ` y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )
24 22 23 eqeq12d 
 |-  ( f = F -> ( ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) <-> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) )
25 21 24 anbi12d 
 |-  ( f = F -> ( ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) <-> ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) )
26 25 2ralbidv 
 |-  ( f = F -> ( A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) <-> A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) )
27 16 26 anbi12d 
 |-  ( f = F -> ( ( ( f ` .1. ) = N /\ A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) <-> ( ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) ) )
28 27 elrab 
 |-  ( F e. { f e. ( C ^m B ) | ( ( f ` .1. ) = N /\ A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } <-> ( F e. ( C ^m B ) /\ ( ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) ) )
29 3anass 
 |-  ( ( F : B --> C /\ ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) <-> ( F : B --> C /\ ( ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) ) )
30 14 28 29 3bitr4i 
 |-  ( F e. { f e. ( C ^m B ) | ( ( f ` .1. ) = N /\ A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } <-> ( F : B --> C /\ ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) )
31 10 30 bitrdi 
 |-  ( ( R e. Ring /\ S e. Ring ) -> ( F e. ( R RingHom S ) <-> ( F : B --> C /\ ( F ` .1. ) = N /\ A. x e. B A. y e. B ( ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) /\ ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) ) ) ) )