Definition df-rngo 36062

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

Assertion

Ref	Expression
df-rngo	⊢ RingOps = {⟨𝑔, ℎ⟩ ∣ ((𝑔 ∈ AbelOp ∧ ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))) ∧ ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)))}

Distinct variable group:   𝑔,ℎ,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-rngo

Step	Hyp	Ref	Expression
1		crngo 36061	. 2 class RingOps
2		vg	. . . . . . 7 setvar 𝑔
3	2	cv 1538	. . . . . 6 class 𝑔
4		cablo 28915	. . . . . 6 class AbelOp
5	3, 4	wcel 2107	. . . . 5 wff 𝑔 ∈ AbelOp
6	3	crn 5591	. . . . . . 7 class ran 𝑔
7	6, 6	cxp 5588	. . . . . 6 class (ran 𝑔 × ran 𝑔)
8		vh	. . . . . . 7 setvar ℎ
9	8	cv 1538	. . . . . 6 class ℎ
10	7, 6, 9	wf 6433	. . . . 5 wff ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔
11	5, 10	wa 396	. . . 4 wff (𝑔 ∈ AbelOp ∧ ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔)
12		vx	. . . . . . . . . . . . 13 setvar 𝑥
13	12	cv 1538	. . . . . . . . . . . 12 class 𝑥
14		vy	. . . . . . . . . . . . 13 setvar 𝑦
15	14	cv 1538	. . . . . . . . . . . 12 class 𝑦
16	13, 15, 9	co 7284	. . . . . . . . . . 11 class (𝑥ℎ𝑦)
17		vz	. . . . . . . . . . . 12 setvar 𝑧
18	17	cv 1538	. . . . . . . . . . 11 class 𝑧
19	16, 18, 9	co 7284	. . . . . . . . . 10 class ((𝑥ℎ𝑦)ℎ𝑧)
20	15, 18, 9	co 7284	. . . . . . . . . . 11 class (𝑦ℎ𝑧)
21	13, 20, 9	co 7284	. . . . . . . . . 10 class (𝑥ℎ(𝑦ℎ𝑧))
22	19, 21	wceq 1539	. . . . . . . . 9 wff ((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧))
23	15, 18, 3	co 7284	. . . . . . . . . . 11 class (𝑦𝑔𝑧)
24	13, 23, 9	co 7284	. . . . . . . . . 10 class (𝑥ℎ(𝑦𝑔𝑧))
25	13, 18, 9	co 7284	. . . . . . . . . . 11 class (𝑥ℎ𝑧)
26	16, 25, 3	co 7284	. . . . . . . . . 10 class ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧))
27	24, 26	wceq 1539	. . . . . . . . 9 wff (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧))
28	13, 15, 3	co 7284	. . . . . . . . . . 11 class (𝑥𝑔𝑦)
29	28, 18, 9	co 7284	. . . . . . . . . 10 class ((𝑥𝑔𝑦)ℎ𝑧)
30	25, 20, 3	co 7284	. . . . . . . . . 10 class ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))
31	29, 30	wceq 1539	. . . . . . . . 9 wff ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))
32	22, 27, 31	w3a 1086	. . . . . . . 8 wff (((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧)))
33	32, 17, 6	wral 3065	. . . . . . 7 wff ∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧)))
34	33, 14, 6	wral 3065	. . . . . 6 wff ∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧)))
35	34, 12, 6	wral 3065	. . . . 5 wff ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧)))
36	16, 15	wceq 1539	. . . . . . . 8 wff (𝑥ℎ𝑦) = 𝑦
37	15, 13, 9	co 7284	. . . . . . . . 9 class (𝑦ℎ𝑥)
38	37, 15	wceq 1539	. . . . . . . 8 wff (𝑦ℎ𝑥) = 𝑦
39	36, 38	wa 396	. . . . . . 7 wff ((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)
40	39, 14, 6	wral 3065	. . . . . 6 wff ∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)
41	40, 12, 6	wrex 3066	. . . . 5 wff ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)
42	35, 41	wa 396	. . . 4 wff (∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))) ∧ ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦))
43	11, 42	wa 396	. . 3 wff ((𝑔 ∈ AbelOp ∧ ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))) ∧ ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)))
44	43, 2, 8	copab 5137	. 2 class {⟨𝑔, ℎ⟩ ∣ ((𝑔 ∈ AbelOp ∧ ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))) ∧ ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)))}
45	1, 44	wceq 1539	1 wff RingOps = {⟨𝑔, ℎ⟩ ∣ ((𝑔 ∈ AbelOp ∧ ℎ:(ran 𝑔 × ran 𝑔)⟶ran 𝑔) ∧ (∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔∀𝑧 ∈ ran 𝑔(((𝑥ℎ𝑦)ℎ𝑧) = (𝑥ℎ(𝑦ℎ𝑧)) ∧ (𝑥ℎ(𝑦𝑔𝑧)) = ((𝑥ℎ𝑦)𝑔(𝑥ℎ𝑧)) ∧ ((𝑥𝑔𝑦)ℎ𝑧) = ((𝑥ℎ𝑧)𝑔(𝑦ℎ𝑧))) ∧ ∃𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔((𝑥ℎ𝑦) = 𝑦 ∧ (𝑦ℎ𝑥) = 𝑦)))}

This definition is referenced by:  relrngo  36063  isrngo  36064