Metamath Proof Explorer

Definition df-rng

Description: Define the class of all non-unital rings. Anon-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of BourbakiAlg1 p. 93 or the definition of a ring in part Preliminaries of Roman p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020)

Ref Expression
Assertion df-rng ⊢ Rng = f ∈ Abel | mulGrp f ∈ Smgrp ∧ [˙Base f / b]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z

Detailed syntax breakdown

Step Hyp Ref Expression
0 crng class Rng
1 vf setvar f
2 cabl class Abel
3 cmgp class mulGrp
4 1 cv setvar f
5 4 3 cfv class mulGrp f
6 csgrp class Smgrp
7 5 6 wcel wff mulGrp f ∈ Smgrp
8 cbs class Base
9 4 8 cfv class Base f
10 vb setvar b
11 cplusg class + 𝑔
12 4 11 cfv class + f
13 vp setvar p
14 cmulr class ⋅ 𝑟
15 4 14 cfv class ⋅ f
16 vt setvar t
17 vx setvar x
18 10 cv setvar b
19 vy setvar y
20 vz setvar z
21 17 cv setvar x
22 16 cv setvar t
23 19 cv setvar y
24 13 cv setvar p
25 20 cv setvar z
26 23 25 24 co class y p z
27 21 26 22 co class x t y p z
28 21 23 22 co class x t y
29 21 25 22 co class x t z
30 28 29 24 co class x t y p x t z
31 27 30 wceq wff x t y p z = x t y p x t z
32 21 23 24 co class x p y
33 32 25 22 co class x p y t z
34 23 25 22 co class y t z
35 29 34 24 co class x t z p y t z
36 33 35 wceq wff x p y t z = x t z p y t z
37 31 36 wa wff x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
38 37 20 18 wral wff ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
39 38 19 18 wral wff ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
40 39 17 18 wral wff ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
41 40 16 15 wsbc wff [˙⋅ f / t]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
42 41 13 12 wsbc wff [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
43 42 10 9 wsbc wff [˙Base f / b]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
44 7 43 wa wff mulGrp f ∈ Smgrp ∧ [˙Base f / b]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
45 44 1 2 crab class f ∈ Abel | mulGrp f ∈ Smgrp ∧ [˙Base f / b]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z
46 0 45 wceq wff Rng = f ∈ Abel | mulGrp f ∈ Smgrp ∧ [˙Base f / b]˙ [˙+ f / p]˙ [˙⋅ f / t]˙ ∀ x ∈ b ∀ y ∈ b ∀ z ∈ b x t y p z = x t y p x t z ∧ x p y t z = x t z p y t z