Metamath Proof Explorer

Theorem rhmval0

Description: The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 22-Sep-2015) (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 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 ) ) ) ) } )

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 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
10 9 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
11 10 adantr 
 |-  ( ( r = R /\ s = S ) -> ( Base ` r ) = B )
12 fveq2 
 |-  ( r = R -> ( 1r ` r ) = ( 1r ` R ) )
13 12 3 eqtr4di 
 |-  ( r = R -> ( 1r ` r ) = .1. )
14 13 fveq2d 
 |-  ( r = R -> ( f ` ( 1r ` r ) ) = ( f ` .1. ) )
15 fveq2 
 |-  ( s = S -> ( 1r ` s ) = ( 1r ` S ) )
16 15 4 eqtr4di 
 |-  ( s = S -> ( 1r ` s ) = N )
17 14 16 eqeqan12d 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) <-> ( f ` .1. ) = N ) )
18 fveq2 
 |-  ( r = R -> ( +g ` r ) = ( +g ` R ) )
19 18 7 eqtr4di 
 |-  ( r = R -> ( +g ` r ) = .+ )
20 19 oveqd 
 |-  ( r = R -> ( x ( +g ` r ) y ) = ( x .+ y ) )
21 20 fveq2d 
 |-  ( r = R -> ( f ` ( x ( +g ` r ) y ) ) = ( f ` ( x .+ y ) ) )
22 fveq2 
 |-  ( s = S -> ( +g ` s ) = ( +g ` S ) )
23 22 8 eqtr4di 
 |-  ( s = S -> ( +g ` s ) = .+^ )
24 23 oveqd 
 |-  ( s = S -> ( ( f ` x ) ( +g ` s ) ( f ` y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) )
25 21 24 eqeqan12d 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) <-> ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) ) )
26 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
27 26 5 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
28 27 oveqd 
 |-  ( r = R -> ( x ( .r ` r ) y ) = ( x .x. y ) )
29 28 fveq2d 
 |-  ( r = R -> ( f ` ( x ( .r ` r ) y ) ) = ( f ` ( x .x. y ) ) )
30 fveq2 
 |-  ( s = S -> ( .r ` s ) = ( .r ` S ) )
31 30 6 eqtr4di 
 |-  ( s = S -> ( .r ` s ) = .X. )
32 31 oveqd 
 |-  ( s = S -> ( ( f ` x ) ( .r ` s ) ( f ` y ) ) = ( ( f ` x ) .X. ( f ` y ) ) )
33 29 32 eqeqan12d 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) <-> ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) )
34 25 33 anbi12d 
 |-  ( ( r = R /\ s = S ) -> ( ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) <-> ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) )
35 34 2ralbidv 
 |-  ( ( r = R /\ s = S ) -> ( A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) <-> A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) )
36 17 35 anbi12d 
 |-  ( ( r = R /\ s = S ) -> ( ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) <-> ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) ) )
37 36 rabbidv 
 |-  ( ( r = R /\ s = S ) -> { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } = { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } )
38 37 csbeq2dv 
 |-  ( ( r = R /\ s = S ) -> [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } = [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } )
39 11 38 csbeq12dv 
 |-  ( ( r = R /\ s = S ) -> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } = [_ B / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } )
40 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
41 40 2 eqtr4di 
 |-  ( s = S -> ( Base ` s ) = C )
42 41 adantl 
 |-  ( ( r = R /\ s = S ) -> ( Base ` s ) = C )
43 42 csbeq1d 
 |-  ( ( r = R /\ s = S ) -> [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } = [_ C / w ]_ { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } )
44 43 csbeq2dv 
 |-  ( ( r = R /\ s = S ) -> [_ B / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } = [_ B / v ]_ [_ C / w ]_ { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) } )
45 1 fvexi 
 |-  B e. _V
46 2 fvexi 
 |-  C e. _V
47 oveq12 
 |-  ( ( w = C /\ v = B ) -> ( w ^m v ) = ( C ^m B ) )
48 47 ancoms 
 |-  ( ( v = B /\ w = C ) -> ( w ^m v ) = ( C ^m B ) )
49 raleq 
 |-  ( v = B -> ( A. x e. v A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) <-> A. x e. B A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) )
50 raleq 
 |-  ( v = B -> ( A. y e. v ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) <-> A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+^ ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .X. ( f ` y ) ) ) ) )
51 50 ralbidv 
 |-  ( v = B -> ( A. x e. B A. y e. v ( ( 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 ) ) ) ) )
52 49 51 bitrd 
 |-  ( v = B -> ( A. x e. v A. y e. v ( ( 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 ) ) ) ) )
53 52 adantr 
 |-  ( ( v = B /\ w = C ) -> ( A. x e. v A. y e. v ( ( 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 ) ) ) ) )
54 53 anbi2d 
 |-  ( ( v = B /\ w = C ) -> ( ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( 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 ) ) ) ) ) )
55 48 54 rabeqbidv 
 |-  ( ( v = B /\ w = C ) -> { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( 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 ) ) ) ) } )
56 45 46 55 csbie2 
 |-  [_ B / v ]_ [_ C / w ]_ { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( 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 ) ) ) ) }
57 56 a1i 
 |-  ( ( r = R /\ s = S ) -> [_ B / v ]_ [_ C / w ]_ { f e. ( w ^m v ) | ( ( f ` .1. ) = N /\ A. x e. v A. y e. v ( ( 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 ) ) ) ) } )
58 39 44 57 3eqtrd 
 |-  ( ( r = R /\ s = S ) -> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( 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 ) ) ) ) } )
59 df-rhm 
 |-  RingHom = ( r e. Ring , s e. Ring |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } )
60 ovex 
 |-  ( C ^m B ) e. _V
61 60 rabex 
 |-  { 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 ) ) ) ) } e. _V
62 58 59 61 ovmpoa 
 |-  ( ( 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 ) ) ) ) } )