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