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 \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land 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 \in AbelOp$
6	2	cv	$setvar h$
7	3	crn	$class ran g$
8	7 7	cxp	$class (ran g \times ran g)$
9	8 7 6	wf	$wff h : ran g \times ran g ⟶ ran g$
10	5 9	wa	$wff (g \in AbelOp \land h : ran g \times 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) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z))$
32	31 13 7	wral	$wff \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z))$
33	32 12 7	wral	$wff \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z))$
34	33 11 7	wral	$wff \forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (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 \land y h x = y)$
39	38 12 7	wral	$wff \forall y \in ran g (x h y = y \land y h x = y)$
40	39 11 7	wrex	$wff \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)$
41	34 40	wa	$wff (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y))$
42	10 41	wa	$wff ((g \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)))$
43	42 1 2	copab	$class \{⟨g, h⟩ \| ((g \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)))\}$
44	0 43	wceq	$wff RingOps = \{⟨g, h⟩ \| ((g \in AbelOp \land h : ran g \times ran g ⟶ ran g) \land (\forall x \in ran g \forall y \in ran g \forall z \in ran g ((x h y) h z = x h (y h z) \land x h (y g z) = (x h y) g (x h z) \land (x g y) h z = (x h z) g (y h z)) \land \exists x \in ran g \forall y \in ran g (x h y = y \land y h x = y)))\}$

Metamath Proof Explorer

Definition df-rngo

Detailed syntax breakdown