This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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