opprring

Description: An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Aug-2015)

		Ref	Expression
	Hypothesis	opprbas.1	$⊢ O = {opp}_{r} (R)$
	Assertion	opprring	$⊢ R \in Ring \to O \in Ring$

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	$⊢ O = {opp}_{r} (R)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	1 2	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
4	3	a1i	$⊢ R \in Ring \to {Base}_{R} = {Base}_{O}$
5		eqid	$⊢ +_{R} = +_{R}$
6	1 5	oppradd	$⊢ +_{R} = +_{O}$
7	6	a1i	$⊢ R \in Ring \to +_{R} = +_{O}$
8		eqidd	$⊢ R \in Ring \to \cdot_{O} = \cdot_{O}$
9		ringgrp	$⊢ R \in Ring \to R \in Grp$
10	3 6	grpprop	$⊢ R \in Grp \leftrightarrow O \in Grp$
11	9 10	sylib	$⊢ R \in Ring \to O \in Grp$
12		eqid	$⊢ \cdot_{R} = \cdot_{R}$
13		eqid	$⊢ \cdot_{O} = \cdot_{O}$
14	2 12 1 13	opprmul	$⊢ x \cdot_{O} y = y \cdot_{R} x$
15	2 12	ringcl	$⊢ (R \in Ring \land y \in {Base}_{R} \land x \in {Base}_{R}) \to y \cdot_{R} x \in {Base}_{R}$
16	15	3com23	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to y \cdot_{R} x \in {Base}_{R}$
17	14 16	eqeltrid	$⊢ (R \in Ring \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{O} y \in {Base}_{R}$
18		simpl	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to R \in Ring$
19		simpr3	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to z \in {Base}_{R}$
20		simpr2	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to y \in {Base}_{R}$
21		simpr1	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to x \in {Base}_{R}$
22	2 12	ringass	$⊢ (R \in Ring \land (z \in {Base}_{R} \land y \in {Base}_{R} \land x \in {Base}_{R})) \to (z \cdot_{R} y) \cdot_{R} x = z \cdot_{R} (y \cdot_{R} x)$
23	18 19 20 21 22	syl13anc	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (z \cdot_{R} y) \cdot_{R} x = z \cdot_{R} (y \cdot_{R} x)$
24	23	eqcomd	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to z \cdot_{R} (y \cdot_{R} x) = (z \cdot_{R} y) \cdot_{R} x$
25	14	oveq1i	$⊢ (x \cdot_{O} y) \cdot_{O} z = (y \cdot_{R} x) \cdot_{O} z$
26	2 12 1 13	opprmul	$⊢ (y \cdot_{R} x) \cdot_{O} z = z \cdot_{R} (y \cdot_{R} x)$
27	25 26	eqtri	$⊢ (x \cdot_{O} y) \cdot_{O} z = z \cdot_{R} (y \cdot_{R} x)$
28	2 12 1 13	opprmul	$⊢ y \cdot_{O} z = z \cdot_{R} y$
29	28	oveq2i	$⊢ x \cdot_{O} (y \cdot_{O} z) = x \cdot_{O} (z \cdot_{R} y)$
30	2 12 1 13	opprmul	$⊢ x \cdot_{O} (z \cdot_{R} y) = (z \cdot_{R} y) \cdot_{R} x$
31	29 30	eqtri	$⊢ x \cdot_{O} (y \cdot_{O} z) = (z \cdot_{R} y) \cdot_{R} x$
32	24 27 31	3eqtr4g	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x \cdot_{O} y) \cdot_{O} z = x \cdot_{O} (y \cdot_{O} z)$
33	2 5 12	ringdir	$⊢ (R \in Ring \land (y \in {Base}_{R} \land z \in {Base}_{R} \land x \in {Base}_{R})) \to (y +_{R} z) \cdot_{R} x = (y \cdot_{R} x) +_{R} (z \cdot_{R} x)$
34	18 20 19 21 33	syl13anc	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (y +_{R} z) \cdot_{R} x = (y \cdot_{R} x) +_{R} (z \cdot_{R} x)$
35	2 12 1 13	opprmul	$⊢ x \cdot_{O} (y +_{R} z) = (y +_{R} z) \cdot_{R} x$
36	2 12 1 13	opprmul	$⊢ x \cdot_{O} z = z \cdot_{R} x$
37	14 36	oveq12i	$⊢ (x \cdot_{O} y) +_{R} (x \cdot_{O} z) = (y \cdot_{R} x) +_{R} (z \cdot_{R} x)$
38	34 35 37	3eqtr4g	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to x \cdot_{O} (y +_{R} z) = (x \cdot_{O} y) +_{R} (x \cdot_{O} z)$
39	2 5 12	ringdi	$⊢ (R \in Ring \land (z \in {Base}_{R} \land x \in {Base}_{R} \land y \in {Base}_{R})) \to z \cdot_{R} (x +_{R} y) = (z \cdot_{R} x) +_{R} (z \cdot_{R} y)$
40	18 19 21 20 39	syl13anc	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to z \cdot_{R} (x +_{R} y) = (z \cdot_{R} x) +_{R} (z \cdot_{R} y)$
41	2 12 1 13	opprmul	$⊢ (x +_{R} y) \cdot_{O} z = z \cdot_{R} (x +_{R} y)$
42	36 28	oveq12i	$⊢ (x \cdot_{O} z) +_{R} (y \cdot_{O} z) = (z \cdot_{R} x) +_{R} (z \cdot_{R} y)$
43	40 41 42	3eqtr4g	$⊢ (R \in Ring \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x +_{R} y) \cdot_{O} z = (x \cdot_{O} z) +_{R} (y \cdot_{O} z)$
44		eqid	$⊢ 1_{R} = 1_{R}$
45	2 44	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
46	2 12 1 13	opprmul	$⊢ 1_{R} \cdot_{O} x = x \cdot_{R} 1_{R}$
47	2 12 44	ringridm	$⊢ (R \in Ring \land x \in {Base}_{R}) \to x \cdot_{R} 1_{R} = x$
48	46 47	eqtrid	$⊢ (R \in Ring \land x \in {Base}_{R}) \to 1_{R} \cdot_{O} x = x$
49	2 12 1 13	opprmul	$⊢ x \cdot_{O} 1_{R} = 1_{R} \cdot_{R} x$
50	2 12 44	ringlidm	$⊢ (R \in Ring \land x \in {Base}_{R}) \to 1_{R} \cdot_{R} x = x$
51	49 50	eqtrid	$⊢ (R \in Ring \land x \in {Base}_{R}) \to x \cdot_{O} 1_{R} = x$
52	4 7 8 11 17 32 38 43 45 48 51	isringd	$⊢ R \in Ring \to O \in Ring$

Metamath Proof Explorer

Theorem opprring

Proof