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-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 ) ) ) } ) |
8 |
7
|
a1i |
|- ( ( R e. Rng /\ S e. Rng ) -> 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 ) ) ) } ) ) |
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
|
syl5eq |
|- ( ( 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 RngHomo 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 ) ) ) } ) |