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 \in (R RingHom S) \to F \in ({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	$⊢ \cdot_{{opp}_{r} (R)} = \cdot_{{opp}_{r} (R)}$
5		eqid	$⊢ \cdot_{{opp}_{r} (S)} = \cdot_{{opp}_{r} (S)}$
6		rhmrcl1	$⊢ F \in (R RingHom S) \to R \in Ring$
7		eqid	$⊢ {opp}_{r} (R) = {opp}_{r} (R)$
8	7	opprringb	$⊢ R \in Ring \leftrightarrow {opp}_{r} (R) \in Ring$
9	6 8	sylib	$⊢ F \in (R RingHom S) \to {opp}_{r} (R) \in Ring$
10		rhmrcl2	$⊢ F \in (R RingHom S) \to S \in Ring$
11		eqid	$⊢ {opp}_{r} (S) = {opp}_{r} (S)$
12	11	opprringb	$⊢ S \in Ring \leftrightarrow {opp}_{r} (S) \in Ring$
13	10 12	sylib	$⊢ F \in (R RingHom S) \to {opp}_{r} (S) \in 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 \in (R RingHom S) \to F (1_{{opp}_{r} (R)}) = 1_{{opp}_{r} (S)}$
21		simpl	$⊢ (F \in (R RingHom S) \land (x \in {Base}_{{opp}_{r} (R)} \land y \in {Base}_{{opp}_{r} (R)})) \to F \in (R RingHom S)$
22		simprr	$⊢ (F \in (R RingHom S) \land (x \in {Base}_{{opp}_{r} (R)} \land y \in {Base}_{{opp}_{r} (R)})) \to y \in {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 \in (R RingHom S) \land (x \in {Base}_{{opp}_{r} (R)} \land y \in {Base}_{{opp}_{r} (R)})) \to y \in {Base}_{R}$
26		simprl	$⊢ (F \in (R RingHom S) \land (x \in {Base}_{{opp}_{r} (R)} \land y \in {Base}_{{opp}_{r} (R)})) \to x \in {Base}_{{opp}_{r} (R)}$
27	26 24	eleqtrrdi	$⊢ (F \in (R RingHom S) \land (x \in {Base}_{{opp}_{r} (R)} \land y \in {Base}_{{opp}_{r} (R)})) \to x \in {Base}_{R}$
28		eqid	$⊢ \cdot_{R} = \cdot_{R}$
29		eqid	$⊢ \cdot_{S} = \cdot_{S}$
30	23 28 29	rhmmul	$⊢ (F \in (R RingHom S) \land y \in {Base}_{R} \land x \in {Base}_{R}) \to F (y \cdot_{R} x) = F (y) \cdot_{S} F (x)$
31	21 25 27 30	syl3anc	$⊢ (F \in (R RingHom S) \land (x \in {Base}_{{opp}_{r} (R)} \land y \in {Base}_{{opp}_{r} (R)})) \to F (y \cdot_{R} x) = F (y) \cdot_{S} F (x)$
32	23 28 7 4	opprmul	$⊢ x \cdot_{{opp}_{r} (R)} y = y \cdot_{R} x$
33	32	fveq2i	$⊢ F (x \cdot_{{opp}_{r} (R)} y) = F (y \cdot_{R} x)$
34		eqid	$⊢ {Base}_{S} = {Base}_{S}$
35	34 29 11 5	opprmul	$⊢ F (x) \cdot_{{opp}_{r} (S)} F (y) = F (y) \cdot_{S} F (x)$
36	31 33 35	3eqtr4g	$⊢ (F \in (R RingHom S) \land (x \in {Base}_{{opp}_{r} (R)} \land y \in {Base}_{{opp}_{r} (R)})) \to F (x \cdot_{{opp}_{r} (R)} y) = F (x) \cdot_{{opp}_{r} (S)} F (y)$
37		ringgrp	$⊢ {opp}_{r} (R) \in Ring \to {opp}_{r} (R) \in Grp$
38	9 37	syl	$⊢ F \in (R RingHom S) \to {opp}_{r} (R) \in Grp$
39		ringgrp	$⊢ {opp}_{r} (S) \in Ring \to {opp}_{r} (S) \in Grp$
40	13 39	syl	$⊢ F \in (R RingHom S) \to {opp}_{r} (S) \in Grp$
41	23 34	rhmf	$⊢ F \in (R RingHom S) \to F : {Base}_{R} ⟶ {Base}_{S}$
42		rhmghm	$⊢ F \in (R RingHom S) \to F \in (R GrpHom S)$
43	42	ad2antrr	$⊢ ((F \in (R RingHom S) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to F \in (R GrpHom S)$
44		simplr	$⊢ ((F \in (R RingHom S) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to x \in {Base}_{R}$
45		simpr	$⊢ ((F \in (R RingHom S) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to y \in {Base}_{R}$
46		eqid	$⊢ +_{R} = +_{R}$
47		eqid	$⊢ +_{S} = +_{S}$
48	23 46 47	ghmlin	$⊢ (F \in (R GrpHom S) \land x \in {Base}_{R} \land y \in {Base}_{R}) \to F (x +_{R} y) = F (x) +_{S} F (y)$
49	43 44 45 48	syl3anc	$⊢ ((F \in (R RingHom S) \land x \in {Base}_{R}) \land y \in {Base}_{R}) \to F (x +_{R} y) = F (x) +_{S} F (y)$
50	49	ralrimiva	$⊢ (F \in (R RingHom S) \land x \in {Base}_{R}) \to \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y)$
51	50	ralrimiva	$⊢ F \in (R RingHom S) \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y)$
52	41 51	jca	$⊢ F \in (R RingHom S) \to (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y))$
53	38 40 52	jca31	$⊢ F \in (R RingHom S) \to (({opp}_{r} (R) \in Grp \land {opp}_{r} (S) \in Grp) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {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 \in ({opp}_{r} (R) GrpHom {opp}_{r} (S)) \leftrightarrow (({opp}_{r} (R) \in Grp \land {opp}_{r} (S) \in Grp) \land (F : {Base}_{R} ⟶ {Base}_{S} \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} F (x +_{R} y) = F (x) +_{S} F (y)))$
58	53 57	sylibr	$⊢ F \in (R RingHom S) \to F \in ({opp}_{r} (R) GrpHom {opp}_{r} (S))$
59	1 2 3 4 5 9 13 20 36 58	isrhm2d	$⊢ F \in (R RingHom S) \to F \in ({opp}_{r} (R) RingHom {opp}_{r} (S))$

Metamath Proof Explorer

Theorem rhmopp

Proof