Metamath Proof Explorer

Definition df-rngo

Description: Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006) (New usage is discouraged.)

Ref Expression
Assertion df-rngo ⊢ RingOps = g h | g ∈ AbelOp ∧ h : ran ⁡ g × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z ∧ ∃ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x h y = y ∧ y h x = y

Detailed syntax breakdown

Step Hyp Ref Expression
0 crngo class RingOps
1 vg setvar g
2 vh setvar h
3 1 cv setvar g
4 cablo class AbelOp
5 3 4 wcel wff g ∈ AbelOp
6 2 cv setvar h
7 3 crn class ran ⁡ g
8 7 7 cxp class ran ⁡ g × ran ⁡ g
9 8 7 6 wf wff h : ran ⁡ g × ran ⁡ g ⟶ ran ⁡ g
10 5 9 wa wff g ∈ AbelOp ∧ h : ran ⁡ g × ran ⁡ g ⟶ ran ⁡ g
11 vx setvar x
12 vy setvar y
13 vz setvar z
14 11 cv setvar x
15 12 cv setvar y
16 14 15 6 co class x h y
17 13 cv setvar z
18 16 17 6 co class x h y h z
19 15 17 6 co class y h z
20 14 19 6 co class x h y h z
21 18 20 wceq wff x h y h z = x h y h z
22 15 17 3 co class y g z
23 14 22 6 co class x h y g z
24 14 17 6 co class x h z
25 16 24 3 co class x h y g x h z
26 23 25 wceq wff x h y g z = x h y g x h z
27 14 15 3 co class x g y
28 27 17 6 co class x g y h z
29 24 19 3 co class x h z g y h z
30 28 29 wceq wff x g y h z = x h z g y h z
31 21 26 30 w3a wff x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z
32 31 13 7 wral wff ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z
33 32 12 7 wral wff ∀ y ∈ ran ⁡ g ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z
34 33 11 7 wral wff ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z
35 16 15 wceq wff x h y = y
36 15 14 6 co class y h x
37 36 15 wceq wff y h x = y
38 35 37 wa wff x h y = y ∧ y h x = y
39 38 12 7 wral wff ∀ y ∈ ran ⁡ g x h y = y ∧ y h x = y
40 39 11 7 wrex wff ∃ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x h y = y ∧ y h x = y
41 34 40 wa wff ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z ∧ ∃ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x h y = y ∧ y h x = y
42 10 41 wa wff g ∈ AbelOp ∧ h : ran ⁡ g × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z ∧ ∃ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x h y = y ∧ y h x = y
43 42 1 2 copab class g h | g ∈ AbelOp ∧ h : ran ⁡ g × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z ∧ ∃ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x h y = y ∧ y h x = y
44 0 43 wceq wff RingOps = g h | g ∈ AbelOp ∧ h : ran ⁡ g × ran ⁡ g ⟶ ran ⁡ g ∧ ∀ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g ∀ z ∈ ran ⁡ g x h y h z = x h y h z ∧ x h y g z = x h y g x h z ∧ x g y h z = x h z g y h z ∧ ∃ x ∈ ran ⁡ g ∀ y ∈ ran ⁡ g x h y = y ∧ y h x = y