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