This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-ring

Description: Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition 1 in BourbakiAlg1 p. 92 or definition of a ring with identity in part Preliminaries of Roman p. 19. So that the additive structure must be abelian (see ringcom ), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. Therefore, it can be shown that a unital ring is a non-unital ring ( ringrng ) only after ringabl was proven. (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion df-ring Ring = { 𝑓 ∈ Grp ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Mnd ∧ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crg ⊢ Ring
1 vf ⊢ 𝑓
2 cgrp ⊢ Grp
3 cmgp ⊢ mulGrp
4 1 cv ⊢ 𝑓
5 4 3 cfv ⊢ ( mulGrp ‘ 𝑓 )
6 cmnd ⊢ Mnd
7 5 6 wcel ⊢ ( mulGrp ‘ 𝑓 ) ∈ Mnd
8 cbs ⊢ Base
9 4 8 cfv ⊢ ( Base ‘ 𝑓 )
10 vr ⊢ 𝑟
11 cplusg ⊢ +g
12 4 11 cfv ⊢ ( +g ‘ 𝑓 )
13 vp ⊢ 𝑝
14 cmulr ⊢ .r
15 4 14 cfv ⊢ ( .r ‘ 𝑓 )
16 vt ⊢ 𝑡
17 vx ⊢ 𝑥
18 10 cv ⊢ 𝑟
19 vy ⊢ 𝑦
20 vz ⊢ 𝑧
21 17 cv ⊢ 𝑥
22 16 cv ⊢ 𝑡
23 19 cv ⊢ 𝑦
24 13 cv ⊢ 𝑝
25 20 cv ⊢ 𝑧
26 23 25 24 co ⊢ ( 𝑦 𝑝 𝑧 )
27 21 26 22 co ⊢ ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) )
28 21 23 22 co ⊢ ( 𝑥 𝑡 𝑦 )
29 21 25 22 co ⊢ ( 𝑥 𝑡 𝑧 )
30 28 29 24 co ⊢ ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) )
31 27 30 wceq ⊢ ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) )
32 21 23 24 co ⊢ ( 𝑥 𝑝 𝑦 )
33 32 25 22 co ⊢ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 )
34 23 25 22 co ⊢ ( 𝑦 𝑡 𝑧 )
35 29 34 24 co ⊢ ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) )
36 33 35 wceq ⊢ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) )
37 31 36 wa ⊢ ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
38 37 20 18 wral ⊢ ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
39 38 19 18 wral ⊢ ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
40 39 17 18 wral ⊢ ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
41 40 16 15 wsbc ⊢ [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
42 41 13 12 wsbc ⊢ [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
43 42 10 9 wsbc ⊢ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) )
44 7 43 wa ⊢ ( ( mulGrp ‘ 𝑓 ) ∈ Mnd ∧ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) )
45 44 1 2 crab ⊢ { 𝑓 ∈ Grp ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Mnd ∧ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }
46 0 45 wceq ⊢ Ring = { 𝑓 ∈ Grp ∣ ( ( mulGrp ‘ 𝑓 ) ∈ Mnd ∧ [ ( Base ‘ 𝑓 ) / 𝑟 ] [ ( +g ‘ 𝑓 ) / 𝑝 ] [ ( .r ‘ 𝑓 ) / 𝑡 ] ∀ 𝑥 ∈ 𝑟 ∀ 𝑦 ∈ 𝑟 ∀ 𝑧 ∈ 𝑟 ( ( 𝑥 𝑡 ( 𝑦 𝑝 𝑧 ) ) = ( ( 𝑥 𝑡 𝑦 ) 𝑝 ( 𝑥 𝑡 𝑧 ) ) ∧ ( ( 𝑥 𝑝 𝑦 ) 𝑡 𝑧 ) = ( ( 𝑥 𝑡 𝑧 ) 𝑝 ( 𝑦 𝑡 𝑧 ) ) ) ) }