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 R RingHom S F opp r R RingHom opp r S

Proof

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