This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnghmval

Description: The set of the non-unital ring homomorphisms between two non-unital rings. (Contributed by AV, 22-Feb-2020)

Ref Expression
Hypotheses isrnghm.b 
|- B = ( Base ` R )
isrnghm.t 
|- .x. = ( .r ` R )
isrnghm.m 
|- .* = ( .r ` S )
rnghmval.c 
|- C = ( Base ` S )
rnghmval.p 
|- .+ = ( +g ` R )
rnghmval.a 
|- .+b = ( +g ` S )
Assertion rnghmval 
|- ( ( R e. Rng /\ S e. Rng ) -> ( R RngHom S ) = { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )

Proof

Step Hyp Ref Expression
1 isrnghm.b 
 |-  B = ( Base ` R )
2 isrnghm.t 
 |-  .x. = ( .r ` R )
3 isrnghm.m 
 |-  .* = ( .r ` S )
4 rnghmval.c 
 |-  C = ( Base ` S )
5 rnghmval.p 
 |-  .+ = ( +g ` R )
6 rnghmval.a 
 |-  .+b = ( +g ` S )
7 df-rnghm 
 |-  RngHom = ( 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 ) ) ) } )
8 7 a1i 
 |-  ( ( R e. Rng /\ S e. Rng ) -> RngHom = ( 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 ) ) ) } ) )
9 fveq2 
 |-  ( r = R -> ( Base ` r ) = ( Base ` R ) )
10 9 1 eqtr4di 
 |-  ( r = R -> ( Base ` r ) = B )
11 10 csbeq1d 
 |-  ( r = R -> [_ ( 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 ) ) ) } = [_ B / 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 ) ) ) } )
12 fveq2 
 |-  ( s = S -> ( Base ` s ) = ( Base ` S ) )
13 12 4 eqtr4di 
 |-  ( s = S -> ( Base ` s ) = C )
14 13 csbeq1d 
 |-  ( s = S -> [_ ( 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 ) ) ) } = [_ C / 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 ) ) ) } )
15 14 csbeq2dv 
 |-  ( s = S -> [_ B / 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 ) ) ) } = [_ B / v ]_ [_ C / 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 ) ) ) } )
16 11 15 sylan9eq 
 |-  ( ( r = R /\ s = S ) -> [_ ( 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 ) ) ) } = [_ B / v ]_ [_ C / 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 ) ) ) } )
17 16 adantl 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ ( r = R /\ s = S ) ) -> [_ ( 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 ) ) ) } = [_ B / v ]_ [_ C / 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 ) ) ) } )
18 1 fvexi 
 |-  B e. _V
19 4 fvexi 
 |-  C e. _V
20 oveq12 
 |-  ( ( w = C /\ v = B ) -> ( w ^m v ) = ( C ^m B ) )
21 20 ancoms 
 |-  ( ( v = B /\ w = C ) -> ( w ^m v ) = ( C ^m B ) )
22 raleq 
 |-  ( v = B -> ( 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. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) )
23 22 raleqbi1dv 
 |-  ( v = B -> ( 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. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) )
24 23 adantr 
 |-  ( ( v = B /\ w = C ) -> ( 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. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) )
25 21 24 rabeqbidv 
 |-  ( ( v = B /\ w = C ) -> { 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 ) ) ) } = { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) } )
26 18 19 25 csbie2 
 |-  [_ B / v ]_ [_ C / 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 ) ) ) } = { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) }
27 fveq2 
 |-  ( r = R -> ( +g ` r ) = ( +g ` R ) )
28 27 5 eqtr4di 
 |-  ( r = R -> ( +g ` r ) = .+ )
29 28 oveqdr 
 |-  ( ( r = R /\ s = S ) -> ( x ( +g ` r ) y ) = ( x .+ y ) )
30 29 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( f ` ( x ( +g ` r ) y ) ) = ( f ` ( x .+ y ) ) )
31 fveq2 
 |-  ( s = S -> ( +g ` s ) = ( +g ` S ) )
32 31 6 eqtr4di 
 |-  ( s = S -> ( +g ` s ) = .+b )
33 32 adantl 
 |-  ( ( r = R /\ s = S ) -> ( +g ` s ) = .+b )
34 33 oveqd 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` x ) ( +g ` s ) ( f ` y ) ) = ( ( f ` x ) .+b ( f ` y ) ) )
35 30 34 eqeq12d 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) <-> ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) ) )
36 fveq2 
 |-  ( r = R -> ( .r ` r ) = ( .r ` R ) )
37 36 2 eqtr4di 
 |-  ( r = R -> ( .r ` r ) = .x. )
38 37 oveqdr 
 |-  ( ( r = R /\ s = S ) -> ( x ( .r ` r ) y ) = ( x .x. y ) )
39 38 fveq2d 
 |-  ( ( r = R /\ s = S ) -> ( f ` ( x ( .r ` r ) y ) ) = ( f ` ( x .x. y ) ) )
40 fveq2 
 |-  ( s = S -> ( .r ` s ) = ( .r ` S ) )
41 40 3 eqtr4di 
 |-  ( s = S -> ( .r ` s ) = .* )
42 41 adantl 
 |-  ( ( r = R /\ s = S ) -> ( .r ` s ) = .* )
43 42 oveqd 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` x ) ( .r ` s ) ( f ` y ) ) = ( ( f ` x ) .* ( f ` y ) ) )
44 39 43 eqeq12d 
 |-  ( ( r = R /\ s = S ) -> ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) <-> ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) )
45 35 44 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 ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) ) )
46 45 2ralbidv 
 |-  ( ( r = R /\ s = S ) -> ( A. x e. B A. y e. B ( ( 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. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) ) )
47 46 rabbidv 
 |-  ( ( r = R /\ s = S ) -> { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( 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 ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
48 26 47 eqtrid 
 |-  ( ( r = R /\ s = S ) -> [_ B / v ]_ [_ C / 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 ) ) ) } = { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
49 48 adantl 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ ( r = R /\ s = S ) ) -> [_ B / v ]_ [_ C / 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 ) ) ) } = { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
50 17 49 eqtrd 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ ( r = R /\ s = S ) ) -> [_ ( 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 ) ) ) } = { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )
51 simpl 
 |-  ( ( R e. Rng /\ S e. Rng ) -> R e. Rng )
52 simpr 
 |-  ( ( R e. Rng /\ S e. Rng ) -> S e. Rng )
53 ovex 
 |-  ( C ^m B ) e. _V
54 53 rabex 
 |-  { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } e. _V
55 54 a1i 
 |-  ( ( R e. Rng /\ S e. Rng ) -> { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } e. _V )
56 8 50 51 52 55 ovmpod 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( R RngHom S ) = { f e. ( C ^m B ) | A. x e. B A. y e. B ( ( f ` ( x .+ y ) ) = ( ( f ` x ) .+b ( f ` y ) ) /\ ( f ` ( x .x. y ) ) = ( ( f ` x ) .* ( f ` y ) ) ) } )