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 FRRingHomSFopprRRingHomopprS

Proof

Step Hyp Ref Expression
1 eqid BaseopprR=BaseopprR
2 eqid 1opprR=1opprR
3 eqid 1opprS=1opprS
4 eqid opprR=opprR
5 eqid opprS=opprS
6 rhmrcl1 FRRingHomSRRing
7 eqid opprR=opprR
8 7 opprringb RRingopprRRing
9 6 8 sylib FRRingHomSopprRRing
10 rhmrcl2 FRRingHomSSRing
11 eqid opprS=opprS
12 11 opprringb SRingopprSRing
13 10 12 sylib FRRingHomSopprSRing
14 eqid 1R=1R
15 7 14 oppr1 1R=1opprR
16 15 eqcomi 1opprR=1R
17 eqid 1S=1S
18 11 17 oppr1 1S=1opprS
19 18 eqcomi 1opprS=1S
20 16 19 rhm1 FRRingHomSF1opprR=1opprS
21 simpl FRRingHomSxBaseopprRyBaseopprRFRRingHomS
22 simprr FRRingHomSxBaseopprRyBaseopprRyBaseopprR
23 eqid BaseR=BaseR
24 7 23 opprbas BaseR=BaseopprR
25 22 24 eleqtrrdi FRRingHomSxBaseopprRyBaseopprRyBaseR
26 simprl FRRingHomSxBaseopprRyBaseopprRxBaseopprR
27 26 24 eleqtrrdi FRRingHomSxBaseopprRyBaseopprRxBaseR
28 eqid R=R
29 eqid S=S
30 23 28 29 rhmmul FRRingHomSyBaseRxBaseRFyRx=FySFx
31 21 25 27 30 syl3anc FRRingHomSxBaseopprRyBaseopprRFyRx=FySFx
32 23 28 7 4 opprmul xopprRy=yRx
33 32 fveq2i FxopprRy=FyRx
34 eqid BaseS=BaseS
35 34 29 11 5 opprmul FxopprSFy=FySFx
36 31 33 35 3eqtr4g FRRingHomSxBaseopprRyBaseopprRFxopprRy=FxopprSFy
37 ringgrp opprRRingopprRGrp
38 9 37 syl FRRingHomSopprRGrp
39 ringgrp opprSRingopprSGrp
40 13 39 syl FRRingHomSopprSGrp
41 23 34 rhmf FRRingHomSF:BaseRBaseS
42 rhmghm FRRingHomSFRGrpHomS
43 42 ad2antrr FRRingHomSxBaseRyBaseRFRGrpHomS
44 simplr FRRingHomSxBaseRyBaseRxBaseR
45 simpr FRRingHomSxBaseRyBaseRyBaseR
46 eqid +R=+R
47 eqid +S=+S
48 23 46 47 ghmlin FRGrpHomSxBaseRyBaseRFx+Ry=Fx+SFy
49 43 44 45 48 syl3anc FRRingHomSxBaseRyBaseRFx+Ry=Fx+SFy
50 49 ralrimiva FRRingHomSxBaseRyBaseRFx+Ry=Fx+SFy
51 50 ralrimiva FRRingHomSxBaseRyBaseRFx+Ry=Fx+SFy
52 41 51 jca FRRingHomSF:BaseRBaseSxBaseRyBaseRFx+Ry=Fx+SFy
53 38 40 52 jca31 FRRingHomSopprRGrpopprSGrpF:BaseRBaseSxBaseRyBaseRFx+Ry=Fx+SFy
54 11 34 opprbas BaseS=BaseopprS
55 7 46 oppradd +R=+opprR
56 11 47 oppradd +S=+opprS
57 24 54 55 56 isghm FopprRGrpHomopprSopprRGrpopprSGrpF:BaseRBaseSxBaseRyBaseRFx+Ry=Fx+SFy
58 53 57 sylibr FRRingHomSFopprRGrpHomopprS
59 1 2 3 4 5 9 13 20 36 58 isrhm2d FRRingHomSFopprRRingHomopprS