Metamath Proof Explorer


Theorem rhmopp

Description: A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017)

Ref Expression
Assertion rhmopp
|- ( F e. ( R RingHom S ) -> F e. ( ( oppR ` R ) RingHom ( oppR ` S ) ) )

Proof

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 ) ) )