Metamath Proof Explorer

Definition df-rnghomo

Description: Define the set of non-unital ring homomorphisms from r to s . (Contributed by AV, 20-Feb-2020)

Ref Expression
Assertion df-rnghomo 
|- RngHomo = ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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 crngh 
 |-  RngHomo
1 vr 
 |-  r
2 crng 
 |-  Rng
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 vx 
 |-  x
17 vy 
 |-  y
18 11 cv 
 |-  f
19 16 cv 
 |-  x
20 cplusg 
 |-  +g
21 5 20 cfv 
 |-  ( +g ` r )
22 17 cv 
 |-  y
23 19 22 21 co 
 |-  ( x ( +g ` r ) y )
24 23 18 cfv 
 |-  ( f ` ( x ( +g ` r ) y ) )
25 19 18 cfv 
 |-  ( f ` x )
26 8 20 cfv 
 |-  ( +g ` s )
27 22 18 cfv 
 |-  ( f ` y )
28 25 27 26 co 
 |-  ( ( f ` x ) ( +g ` s ) ( f ` y ) )
29 24 28 wceq 
 |-  ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) )
30 cmulr 
 |-  .r
31 5 30 cfv 
 |-  ( .r ` r )
32 19 22 31 co 
 |-  ( x ( .r ` r ) y )
33 32 18 cfv 
 |-  ( f ` ( x ( .r ` r ) y ) )
34 8 30 cfv 
 |-  ( .r ` s )
35 25 27 34 co 
 |-  ( ( f ` x ) ( .r ` s ) ( f ` y ) )
36 33 35 wceq 
 |-  ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) )
37 29 36 wa 
 |-  ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) )
38 37 17 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 ) ) )
39 38 16 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 ) ) )
40 39 11 15 crab 
 |-  { f e. ( w ^m v ) | 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 ) ) ) }
41 10 9 40 csb 
 |-  [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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 ) ) ) }
42 7 6 41 csb 
 |-  [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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 ) ) ) }
43 1 3 2 2 42 cmpo 
 |-  ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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 ) ) ) } )
44 0 43 wceq 
 |-  RngHomo = ( r e. Rng , s e. Rng |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | 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 ) ) ) } )