df-mgp

Description: Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and unitgrp shows that we get a group if we restrict to the elements that have inverses. This allows to formalize such notions as "the multiplication operation of a ring is a monoid" ( ringmgp ) or "the multiplicative identity" in terms of the identity of a monoid ( df-ur ). (Contributed by Mario Carneiro, 21-Dec-2014)

		Ref	Expression
	Assertion	df-mgp	$⊢ mulGrp = (w \in V ⟼ w sSet ⟨+_{ndx}, \cdot_{w}⟩)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgp	$class mulGrp$
1		vw	$setvar w$
2		cvv	$class V$
3	1	cv	$setvar w$
4		csts	$class sSet$
5		cplusg	$class +_{𝑔}$
6		cnx	$class ndx$
7	6 5	cfv	$class +_{ndx}$
8		cmulr	$class \cdot_{𝑟}$
9	3 8	cfv	$class \cdot_{w}$
10	7 9	cop	$class ⟨+_{ndx}, \cdot_{w}⟩$
11	3 10 4	co	$class (w sSet ⟨+_{ndx}, \cdot_{w}⟩)$
12	1 2 11	cmpt	$class (w \in V ⟼ w sSet ⟨+_{ndx}, \cdot_{w}⟩)$
13	0 12	wceq	$wff mulGrp = (w \in V ⟼ w sSet ⟨+_{ndx}, \cdot_{w}⟩)$

Metamath Proof Explorer

Definition df-mgp

Detailed syntax breakdown