Description: A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | rhmopp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | eqid | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | rhmrcl1 | |
|
7 | eqid | |
|
8 | 7 | opprringb | |
9 | 6 8 | sylib | |
10 | rhmrcl2 | |
|
11 | eqid | |
|
12 | 11 | opprringb | |
13 | 10 12 | sylib | |
14 | eqid | |
|
15 | 7 14 | oppr1 | |
16 | 15 | eqcomi | |
17 | eqid | |
|
18 | 11 17 | oppr1 | |
19 | 18 | eqcomi | |
20 | 16 19 | rhm1 | |
21 | simpl | |
|
22 | simprr | |
|
23 | eqid | |
|
24 | 7 23 | opprbas | |
25 | 22 24 | eleqtrrdi | |
26 | simprl | |
|
27 | 26 24 | eleqtrrdi | |
28 | eqid | |
|
29 | eqid | |
|
30 | 23 28 29 | rhmmul | |
31 | 21 25 27 30 | syl3anc | |
32 | 23 28 7 4 | opprmul | |
33 | 32 | fveq2i | |
34 | eqid | |
|
35 | 34 29 11 5 | opprmul | |
36 | 31 33 35 | 3eqtr4g | |
37 | ringgrp | |
|
38 | 9 37 | syl | |
39 | ringgrp | |
|
40 | 13 39 | syl | |
41 | 23 34 | rhmf | |
42 | rhmghm | |
|
43 | 42 | ad2antrr | |
44 | simplr | |
|
45 | simpr | |
|
46 | eqid | |
|
47 | eqid | |
|
48 | 23 46 47 | ghmlin | |
49 | 43 44 45 48 | syl3anc | |
50 | 49 | ralrimiva | |
51 | 50 | ralrimiva | |
52 | 41 51 | jca | |
53 | 38 40 52 | jca31 | |
54 | 11 34 | opprbas | |
55 | 7 46 | oppradd | |
56 | 11 47 | oppradd | |
57 | 24 54 55 56 | isghm | |
58 | 53 57 | sylibr | |
59 | 1 2 3 4 5 9 13 20 36 58 | isrhm2d | |