Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Base ` ( oppR ` R ) ) = ( Base ` ( oppR ` R ) ) |
2 |
|
eqid |
|- ( 1r ` ( oppR ` R ) ) = ( 1r ` ( oppR ` R ) ) |
3 |
|
eqid |
|- ( 1r ` ( oppR ` S ) ) = ( 1r ` ( oppR ` S ) ) |
4 |
|
eqid |
|- ( .r ` ( oppR ` R ) ) = ( .r ` ( oppR ` R ) ) |
5 |
|
eqid |
|- ( .r ` ( oppR ` S ) ) = ( .r ` ( oppR ` S ) ) |
6 |
|
rhmrcl1 |
|- ( F e. ( R RingHom S ) -> R e. Ring ) |
7 |
|
eqid |
|- ( oppR ` R ) = ( oppR ` R ) |
8 |
7
|
opprringb |
|- ( R e. Ring <-> ( oppR ` R ) e. Ring ) |
9 |
6 8
|
sylib |
|- ( F e. ( R RingHom S ) -> ( oppR ` R ) e. Ring ) |
10 |
|
rhmrcl2 |
|- ( F e. ( R RingHom S ) -> S e. Ring ) |
11 |
|
eqid |
|- ( oppR ` S ) = ( oppR ` S ) |
12 |
11
|
opprringb |
|- ( S e. Ring <-> ( oppR ` S ) e. Ring ) |
13 |
10 12
|
sylib |
|- ( F e. ( R RingHom S ) -> ( oppR ` S ) e. Ring ) |
14 |
|
eqid |
|- ( 1r ` R ) = ( 1r ` R ) |
15 |
7 14
|
oppr1 |
|- ( 1r ` R ) = ( 1r ` ( oppR ` R ) ) |
16 |
15
|
eqcomi |
|- ( 1r ` ( oppR ` R ) ) = ( 1r ` R ) |
17 |
|
eqid |
|- ( 1r ` S ) = ( 1r ` S ) |
18 |
11 17
|
oppr1 |
|- ( 1r ` S ) = ( 1r ` ( oppR ` S ) ) |
19 |
18
|
eqcomi |
|- ( 1r ` ( oppR ` S ) ) = ( 1r ` S ) |
20 |
16 19
|
rhm1 |
|- ( F e. ( R RingHom S ) -> ( F ` ( 1r ` ( oppR ` R ) ) ) = ( 1r ` ( oppR ` S ) ) ) |
21 |
|
simpl |
|- ( ( F e. ( R RingHom S ) /\ ( x e. ( Base ` ( oppR ` R ) ) /\ y e. ( Base ` ( oppR ` R ) ) ) ) -> F e. ( R RingHom S ) ) |
22 |
|
simprr |
|- ( ( F e. ( R RingHom S ) /\ ( x e. ( Base ` ( oppR ` R ) ) /\ y e. ( Base ` ( oppR ` R ) ) ) ) -> y e. ( Base ` ( oppR ` R ) ) ) |
23 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
24 |
7 23
|
opprbas |
|- ( Base ` R ) = ( Base ` ( oppR ` R ) ) |
25 |
22 24
|
eleqtrrdi |
|- ( ( F e. ( R RingHom S ) /\ ( x e. ( Base ` ( oppR ` R ) ) /\ y e. ( Base ` ( oppR ` R ) ) ) ) -> y e. ( Base ` R ) ) |
26 |
|
simprl |
|- ( ( F e. ( R RingHom S ) /\ ( x e. ( Base ` ( oppR ` R ) ) /\ y e. ( Base ` ( oppR ` R ) ) ) ) -> x e. ( Base ` ( oppR ` R ) ) ) |
27 |
26 24
|
eleqtrrdi |
|- ( ( F e. ( R RingHom S ) /\ ( x e. ( Base ` ( oppR ` R ) ) /\ y e. ( Base ` ( oppR ` R ) ) ) ) -> x e. ( Base ` R ) ) |
28 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
29 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
30 |
23 28 29
|
rhmmul |
|- ( ( F e. ( R RingHom S ) /\ y e. ( Base ` R ) /\ x e. ( Base ` R ) ) -> ( F ` ( y ( .r ` R ) x ) ) = ( ( F ` y ) ( .r ` S ) ( F ` x ) ) ) |
31 |
21 25 27 30
|
syl3anc |
|- ( ( F e. ( R RingHom S ) /\ ( x e. ( Base ` ( oppR ` R ) ) /\ y e. ( Base ` ( oppR ` R ) ) ) ) -> ( F ` ( y ( .r ` R ) x ) ) = ( ( F ` y ) ( .r ` S ) ( F ` x ) ) ) |
32 |
23 28 7 4
|
opprmul |
|- ( x ( .r ` ( oppR ` R ) ) y ) = ( y ( .r ` R ) x ) |
33 |
32
|
fveq2i |
|- ( F ` ( x ( .r ` ( oppR ` R ) ) y ) ) = ( F ` ( y ( .r ` R ) x ) ) |
34 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
35 |
34 29 11 5
|
opprmul |
|- ( ( F ` x ) ( .r ` ( oppR ` S ) ) ( F ` y ) ) = ( ( F ` y ) ( .r ` S ) ( F ` x ) ) |
36 |
31 33 35
|
3eqtr4g |
|- ( ( F e. ( R RingHom S ) /\ ( x e. ( Base ` ( oppR ` R ) ) /\ y e. ( Base ` ( oppR ` R ) ) ) ) -> ( F ` ( x ( .r ` ( oppR ` R ) ) y ) ) = ( ( F ` x ) ( .r ` ( oppR ` S ) ) ( F ` y ) ) ) |
37 |
|
ringgrp |
|- ( ( oppR ` R ) e. Ring -> ( oppR ` R ) e. Grp ) |
38 |
9 37
|
syl |
|- ( F e. ( R RingHom S ) -> ( oppR ` R ) e. Grp ) |
39 |
|
ringgrp |
|- ( ( oppR ` S ) e. Ring -> ( oppR ` S ) e. Grp ) |
40 |
13 39
|
syl |
|- ( F e. ( R RingHom S ) -> ( oppR ` S ) e. Grp ) |
41 |
23 34
|
rhmf |
|- ( F e. ( R RingHom S ) -> F : ( Base ` R ) --> ( Base ` S ) ) |
42 |
|
rhmghm |
|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) ) |
43 |
42
|
ad2antrr |
|- ( ( ( F e. ( R RingHom S ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> F e. ( R GrpHom S ) ) |
44 |
|
simplr |
|- ( ( ( F e. ( R RingHom S ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> x e. ( Base ` R ) ) |
45 |
|
simpr |
|- ( ( ( F e. ( R RingHom S ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> y e. ( Base ` R ) ) |
46 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
47 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
48 |
23 46 47
|
ghmlin |
|- ( ( F e. ( R GrpHom S ) /\ x e. ( Base ` R ) /\ y e. ( Base ` R ) ) -> ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) |
49 |
43 44 45 48
|
syl3anc |
|- ( ( ( F e. ( R RingHom S ) /\ x e. ( Base ` R ) ) /\ y e. ( Base ` R ) ) -> ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) |
50 |
49
|
ralrimiva |
|- ( ( F e. ( R RingHom S ) /\ x e. ( Base ` R ) ) -> A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) |
51 |
50
|
ralrimiva |
|- ( F e. ( R RingHom S ) -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) |
52 |
41 51
|
jca |
|- ( F e. ( R RingHom S ) -> ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) |
53 |
38 40 52
|
jca31 |
|- ( F e. ( R RingHom S ) -> ( ( ( oppR ` R ) e. Grp /\ ( oppR ` S ) e. Grp ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) ) |
54 |
11 34
|
opprbas |
|- ( Base ` S ) = ( Base ` ( oppR ` S ) ) |
55 |
7 46
|
oppradd |
|- ( +g ` R ) = ( +g ` ( oppR ` R ) ) |
56 |
11 47
|
oppradd |
|- ( +g ` S ) = ( +g ` ( oppR ` S ) ) |
57 |
24 54 55 56
|
isghm |
|- ( F e. ( ( oppR ` R ) GrpHom ( oppR ` S ) ) <-> ( ( ( oppR ` R ) e. Grp /\ ( oppR ` S ) e. Grp ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( +g ` R ) y ) ) = ( ( F ` x ) ( +g ` S ) ( F ` y ) ) ) ) ) |
58 |
53 57
|
sylibr |
|- ( F e. ( R RingHom S ) -> F e. ( ( oppR ` R ) GrpHom ( oppR ` S ) ) ) |
59 |
1 2 3 4 5 9 13 20 36 58
|
isrhm2d |
|- ( F e. ( R RingHom S ) -> F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) ) |