opprrng

Description: An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025)

		Ref	Expression
	Hypothesis	opprrng.o	$⊢ O = {opp}_{r} (R)$
	Assertion	opprrng	$⊢ R \in Rng \to O \in Rng$

Proof

Step	Hyp	Ref	Expression
1		opprrng.o	$⊢ O = {opp}_{r} (R)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	1 2	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
4	3	a1i	$⊢ R \in Rng \to {Base}_{R} = {Base}_{O}$
5		eqid	$⊢ +_{R} = +_{R}$
6	1 5	oppradd	$⊢ +_{R} = +_{O}$
7	6	a1i	$⊢ R \in Rng \to +_{R} = +_{O}$
8		eqidd	$⊢ R \in Rng \to \cdot_{O} = \cdot_{O}$
9		rngabl	$⊢ R \in Rng \to R \in Abel$
10	3 6	ablprop	$⊢ R \in Abel \leftrightarrow O \in Abel$
11	9 10	sylib	$⊢ R \in Rng \to O \in Abel$
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	rngcl	$⊢ (R \in Rng \land y \in {Base}_{R} \land x \in {Base}_{R}) \to y \cdot_{R} x \in {Base}_{R}$
16	15	3com23	$⊢ (R \in Rng \land x \in {Base}_{R} \land y \in {Base}_{R}) \to y \cdot_{R} x \in {Base}_{R}$
17	14 16	eqeltrid	$⊢ (R \in Rng \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x \cdot_{O} y \in {Base}_{R}$
18		simpl	$⊢ (R \in Rng \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to R \in Rng$
19		simpr3	$⊢ (R \in Rng \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to z \in {Base}_{R}$
20		simpr2	$⊢ (R \in Rng \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to y \in {Base}_{R}$
21		simpr1	$⊢ (R \in Rng \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to x \in {Base}_{R}$
22	2 12	rngass	$⊢ (R \in Rng \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 Rng \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 Rng \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 Rng \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	rngdir	$⊢ (R \in Rng \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 Rng \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 Rng \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	rngdi	$⊢ (R \in Rng \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 Rng \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 Rng \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	4 7 8 11 17 32 38 43	isrngd	$⊢ R \in Rng \to O \in Rng$

Metamath Proof Explorer

Theorem opprrng

Proof