Metamath Proof Explorer

Theorem rngohomval

Description: The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses rnghomval.1 
|- G = ( 1st ` R )
rnghomval.2 
|- H = ( 2nd ` R )
rnghomval.3 
|- X = ran G
rnghomval.4 
|- U = ( GId ` H )
rnghomval.5 
|- J = ( 1st ` S )
rnghomval.6 
|- K = ( 2nd ` S )
rnghomval.7 
|- Y = ran J
rnghomval.8 
|- V = ( GId ` K )
Assertion rngohomval 
|- ( ( R e. RingOps /\ S e. RingOps ) -> ( R RngHom S ) = { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 rnghomval.1 
 |-  G = ( 1st ` R )
2 rnghomval.2 
 |-  H = ( 2nd ` R )
3 rnghomval.3 
 |-  X = ran G
4 rnghomval.4 
 |-  U = ( GId ` H )
5 rnghomval.5 
 |-  J = ( 1st ` S )
6 rnghomval.6 
 |-  K = ( 2nd ` S )
7 rnghomval.7 
 |-  Y = ran J
8 rnghomval.8 
 |-  V = ( GId ` K )
9 simpr 
 |-  ( ( r = R /\ s = S ) -> s = S )
10 9 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( 1st ` s ) = ( 1st ` S ) )
11 10 5 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( 1st ` s ) = J )
12 11 rneqd 
 |-  ( ( r = R /\ s = S ) -> ran ( 1st ` s ) = ran J )
13 12 7 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ran ( 1st ` s ) = Y )
14 simpl 
 |-  ( ( r = R /\ s = S ) -> r = R )
15 14 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( 1st ` r ) = ( 1st ` R ) )
16 15 1 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( 1st ` r ) = G )
17 16 rneqd 
 |-  ( ( r = R /\ s = S ) -> ran ( 1st ` r ) = ran G )
18 17 3 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ran ( 1st ` r ) = X )
19 13 18 oveq12d 
 |-  ( ( r = R /\ s = S ) -> ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) = ( Y ^m X ) )
20 14 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( 2nd ` r ) = ( 2nd ` R ) )
21 20 2 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( 2nd ` r ) = H )
22 21 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( GId ` ( 2nd ` r ) ) = ( GId ` H ) )
23 22 4 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( GId ` ( 2nd ` r ) ) = U )
24 23 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( f ` ( GId ` ( 2nd ` r ) ) ) = ( f ` U ) )
25 9 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( 2nd ` s ) = ( 2nd ` S ) )
26 25 6 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( 2nd ` s ) = K )
27 26 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( GId ` ( 2nd ` s ) ) = ( GId ` K ) )
28 27 8 eqtr4di 
 |-  ( ( r = R /\ s = S ) -> ( GId ` ( 2nd ` s ) ) = V )
29 24 28 eqeq12d 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) <-> ( f ` U ) = V ) )
30 16 oveqd 
 |-  ( ( r = R /\ s = S ) -> ( x ( 1st ` r ) y ) = ( x G y ) )
31 30 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( f ` ( x ( 1st ` r ) y ) ) = ( f ` ( x G y ) ) )
32 11 oveqd 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) = ( ( f ` x ) J ( f ` y ) ) )
33 31 32 eqeq12d 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) <-> ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) ) )
34 21 oveqd 
 |-  ( ( r = R /\ s = S ) -> ( x ( 2nd ` r ) y ) = ( x H y ) )
35 34 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( f ` ( x ( 2nd ` r ) y ) ) = ( f ` ( x H y ) ) )
36 26 oveqd 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) = ( ( f ` x ) K ( f ` y ) ) )
37 35 36 eqeq12d 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) <-> ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) )
38 33 37 anbi12d 
 |-  ( ( r = R /\ s = S ) -> ( ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) <-> ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) )
39 18 38 raleqbidv 
 |-  ( ( r = R /\ s = S ) -> ( A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) <-> A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) )
40 18 39 raleqbidv 
 |-  ( ( r = R /\ s = S ) -> ( A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) <-> A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) )
41 29 40 anbi12d 
 |-  ( ( r = R /\ s = S ) -> ( ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) <-> ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) ) )
42 19 41 rabeqbidv 
 |-  ( ( r = R /\ s = S ) -> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } = { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } )
43 df-rngohom 
 |-  RngHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } )
44 ovex 
 |-  ( Y ^m X ) e. _V
45 44 rabex 
 |-  { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } e. _V
46 42 43 45 ovmpoa 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( R RngHom S ) = { f e. ( Y ^m X ) | ( ( f ` U ) = V /\ A. x e. X A. y e. X ( ( f ` ( x G y ) ) = ( ( f ` x ) J ( f ` y ) ) /\ ( f ` ( x H y ) ) = ( ( f ` x ) K ( f ` y ) ) ) ) } )