Definition 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 us 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 = ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgp	⊢ mulGrp
1		vw	⊢ 𝑤
2		cvv	⊢ V
3	1	cv	⊢ 𝑤
4		csts	⊢ sSet
5		cplusg	⊢ +g
6		cnx	⊢ ndx
7	6 5	cfv	⊢ ( +g ‘ ndx )
8		cmulr	⊢ .r
9	3 8	cfv	⊢ ( .r ‘ 𝑤 )
10	7 9	cop	⊢ ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩
11	3 10 4	co	⊢ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ )
12	1 2 11	cmpt	⊢ ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) )
13	0 12	wceq	⊢ mulGrp = ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑤 ) ⟩ ) )