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 ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( ( oppr𝑅 ) RingHom ( oppr𝑆 ) ) )

Proof

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