Metamath Proof Explorer

Definition df-rhm

Description: Define the set of ring homomorphisms from r to s . (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion 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 ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crh 
 |-  RingHom
1 vr 
 |-  r
2 crg 
 |-  Ring
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  r
6 5 4 cfv 
 |-  ( Base ` r )
7 vv 
 |-  v
8 3 cv 
 |-  s
9 8 4 cfv 
 |-  ( Base ` s )
10 vw 
 |-  w
11 vf 
 |-  f
12 10 cv 
 |-  w
13 cmap 
 |-  ^m
14 7 cv 
 |-  v
15 12 14 13 co 
 |-  ( w ^m v )
16 11 cv 
 |-  f
17 cur 
 |-  1r
18 5 17 cfv 
 |-  ( 1r ` r )
19 18 16 cfv 
 |-  ( f ` ( 1r ` r ) )
20 8 17 cfv 
 |-  ( 1r ` s )
21 19 20 wceq 
 |-  ( f ` ( 1r ` r ) ) = ( 1r ` s )
22 vx 
 |-  x
23 vy 
 |-  y
24 22 cv 
 |-  x
25 cplusg 
 |-  +g
26 5 25 cfv 
 |-  ( +g ` r )
27 23 cv 
 |-  y
28 24 27 26 co 
 |-  ( x ( +g ` r ) y )
29 28 16 cfv 
 |-  ( f ` ( x ( +g ` r ) y ) )
30 24 16 cfv 
 |-  ( f ` x )
31 8 25 cfv 
 |-  ( +g ` s )
32 27 16 cfv 
 |-  ( f ` y )
33 30 32 31 co 
 |-  ( ( f ` x ) ( +g ` s ) ( f ` y ) )
34 29 33 wceq 
 |-  ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) )
35 cmulr 
 |-  .r
36 5 35 cfv 
 |-  ( .r ` r )
37 24 27 36 co 
 |-  ( x ( .r ` r ) y )
38 37 16 cfv 
 |-  ( f ` ( x ( .r ` r ) y ) )
39 8 35 cfv 
 |-  ( .r ` s )
40 30 32 39 co 
 |-  ( ( f ` x ) ( .r ` s ) ( f ` y ) )
41 38 40 wceq 
 |-  ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) )
42 34 41 wa 
 |-  ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) )
43 42 23 14 wral 
 |-  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 ) ) )
44 43 22 14 wral 
 |-  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 ) ) )
45 21 44 wa 
 |-  ( ( 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 ) ) ) )
46 45 11 15 crab 
 |-  { 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 ) ) ) ) }
47 10 9 46 csb 
 |-  [_ ( 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 ) ) ) ) }
48 7 6 47 csb 
 |-  [_ ( 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 ) ) ) ) }
49 1 3 2 2 48 cmpo 
 |-  ( 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 ) ) ) ) } )
50 0 49 wceq 
 |-  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 ) ) ) ) } )