isrngd

Description: Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025)

	Ref	Expression
Hypotheses	isrngd.b	$⊢ φ \to B = {Base}_{R}$
	isrngd.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
	isrngd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
	isrngd.g	$⊢ φ \to R \in Abel$
	isrngd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B$
	isrngd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)$
	isrngd.d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z)$
	isrngd.e	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
Assertion	isrngd	$⊢ φ \to R \in Rng$

Proof

Step	Hyp	Ref	Expression
1		isrngd.b	$⊢ φ \to B = {Base}_{R}$
2		isrngd.p	$⊢ φ \to \underset{˙}{+} = +_{R}$
3		isrngd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{R}$
4		isrngd.g	$⊢ φ \to R \in Abel$
5		isrngd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B$
6		isrngd.a	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} y) \underset{˙}{\cdot} z = x \underset{˙}{\cdot} (y \underset{˙}{\cdot} z)$
7		isrngd.d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} (y \underset{˙}{+} z) = (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z)$
8		isrngd.e	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z)$
9		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11	9 10	mgpbas	$⊢ {Base}_{R} = {Base}_{{mulGrp}_{R}}$
12	1 11	eqtrdi	$⊢ φ \to B = {Base}_{{mulGrp}_{R}}$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14	9 13	mgpplusg	$⊢ \cdot_{R} = +_{{mulGrp}_{R}}$
15	3 14	eqtrdi	$⊢ φ \to \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
16		fvexd	$⊢ φ \to {mulGrp}_{R} \in V$
17	12 15 5 6 16	issgrpd	$⊢ φ \to {mulGrp}_{R} \in Smgrp$
18	1	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in {Base}_{R})$
19	1	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{R})$
20	1	eleq2d	$⊢ φ \to (z \in B \leftrightarrow z \in {Base}_{R})$
21	18 19 20	3anbi123d	$⊢ φ \to ((x \in B \land y \in B \land z \in B) \leftrightarrow (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R}))$
22	21	biimpar	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x \in B \land y \in B \land z \in B)$
23	3	adantr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to \underset{˙}{\cdot} = \cdot_{R}$
24		eqidd	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x = x$
25	2	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to y \underset{˙}{+} z = y +_{R} z$
26	23 24 25	oveq123d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} (y \underset{˙}{+} z) = x \cdot_{R} (y +_{R} z)$
27	2	adantr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to \underset{˙}{+} = +_{R}$
28	3	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} y = x \cdot_{R} y$
29	3	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{\cdot} z = x \cdot_{R} z$
30	27 28 29	oveq123d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} y) \underset{˙}{+} (x \underset{˙}{\cdot} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z)$
31	7 26 30	3eqtr3d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z)$
32	2	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to x \underset{˙}{+} y = x +_{R} y$
33		eqidd	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to z = z$
34	23 32 33	oveq123d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{+} y) \underset{˙}{\cdot} z = (x +_{R} y) \cdot_{R} z$
35	3	oveqdr	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to y \underset{˙}{\cdot} z = y \cdot_{R} z$
36	27 29 35	oveq123d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \underset{˙}{\cdot} z) \underset{˙}{+} (y \underset{˙}{\cdot} z) = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)$
37	8 34 36	3eqtr3d	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)$
38	31 37	jca	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))$
39	22 38	syldan	$⊢ (φ \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))$
40	39	ralrimivvva	$⊢ φ \to \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z))$
41		eqid	$⊢ +_{R} = +_{R}$
42	10 9 41 13	isrng	$⊢ R \in Rng \leftrightarrow (R \in Abel \land {mulGrp}_{R} \in Smgrp \land \forall x \in {Base}_{R} \forall y \in {Base}_{R} \forall z \in {Base}_{R} (x \cdot_{R} (y +_{R} z) = (x \cdot_{R} y) +_{R} (x \cdot_{R} z) \land (x +_{R} y) \cdot_{R} z = (x \cdot_{R} z) +_{R} (y \cdot_{R} z)))$
43	4 17 40 42	syl3anbrc	$⊢ φ \to R \in Rng$

Metamath Proof Explorer

Theorem isrngd

Proof