P. 175 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 17401-17500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	submmnd 17401	Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝐻 ∈ Mnd)
Theorem	submbas 17402	The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 = (Base‘𝐻))
Theorem	subm0 17403	Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    &   ⊢ 0 = (0g‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 = (0g‘𝐻))
Theorem	subsubm 17404	A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐴 ∈ (SubMnd‘𝐻) ↔ (𝐴 ∈ (SubMnd‘𝐺) ∧ 𝐴 ⊆ 𝑆)))
Theorem	0mhm 17405	The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 0 = (0g‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → (𝐵 × { 0 }) ∈ (𝑀 MndHom 𝑁))
Theorem	resmhm 17406	Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇))
Theorem	resmhm2 17407	One direction of resmhm2b 17408. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	resmhm2b 17408	Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈)))
Theorem	mhmco 17409	The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈))
Theorem	mhmima 17410	The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubMnd‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMnd‘𝑁))
Theorem	mhmeql 17411	The equalizer of two monoid homomorphisms is a submonoid. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆))
Theorem	submacs 17412	Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵))
Theorem	mrcmndind 17413*	(( From SO's determinants branch )). TODO: Appropriate description to be added! (Contributed by SO, 14-Jul-2018.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 𝑧) → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 0 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 = ((mrCls‘(SubMnd‘𝑀))‘𝐺))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐺) ∧ 𝜒) → 𝜃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	prdspjmhm 17414*	A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom (𝑅‘𝐴)))
Theorem	pwspjmhm 17415*	A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom 𝑅))
Theorem	pwsdiagmhm 17416*	Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌))
Theorem	pwsco1mhm 17417*	Right composition with a function on the index sets yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐴)    &   ⊢ 𝑍 = (𝑅 ↑s 𝐵)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑅 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌))
Theorem	pwsco2mhm 17418*	Left composition with a monoid homomorphism yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐴)    &   ⊢ 𝑍 = (𝑆 ↑s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 MndHom 𝑆))    ⇒   ⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 MndHom 𝑍))
10.1.7  Ordered sums in a monoid One important use of words is as formal composites in cases where order is significant, using the general sum operator df-gsum 16150. If order is not significant, it is simpler to use families instead.
Theorem	gsumvallem2 17419*	Lemma for properties of the set of identities of 𝐺. The set of identities of a monoid is exactly the unique identity element. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}    ⇒   ⊢ (𝐺 ∈ Mnd → 𝑂 = { 0 })
Theorem	gsumsubm 17420	Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Theorem	gsumz 17421*	Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
Theorem	gsumwsubmcl 17422	Closure of the composite in any submonoid. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.)
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) → (𝐺 Σg 𝑊) ∈ 𝑆)
Theorem	gsumws1 17423	A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg ⟨“𝑆”⟩) = 𝑆)
Theorem	gsumwcl 17424	Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
Theorem	gsumccat 17425	Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
Theorem	gsumws2 17426	Valuation of a pair in a monoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵) → (𝐺 Σg ⟨“𝑆𝑇”⟩) = (𝑆 + 𝑇))
Theorem	gsumccatsn 17427	Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) + 𝑍))
Theorem	gsumspl 17428	The primary purpose of the splice construction is to enable local rewrites. Thus, in any monoidal valuation, if a splice does not cause a local change it does not cause a global change. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(#‘𝑆)))    &   ⊢ (𝜑 → 𝑋 ∈ Word 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ Word 𝐵)    &   ⊢ (𝜑 → (𝑀 Σg 𝑋) = (𝑀 Σg 𝑌))    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑆 splice ⟨𝐹, 𝑇, 𝑋⟩)) = (𝑀 Σg (𝑆 splice ⟨𝐹, 𝑇, 𝑌⟩)))
Theorem	gsumwmhm 17429	Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)))
Theorem	gsumwspan 17430*	The submonoid generated by a set of elements is precisely the set of elements which can be expressed as finite products of the generator. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐾 = (mrCls‘(SubMnd‘𝑀))    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))
10.1.8  Free monoids
Syntax	cfrmd 17431	Extend class definition with the free monoid construction.
class freeMnd
Syntax	cvrmd 17432	Extend class notation with free monoid injection.
class varFMnd
Definition	df-frmd 17433	Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ freeMnd = (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
Definition	df-vrmd 17434*	Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ varFMnd = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ ⟨“𝑗”⟩))
Theorem	frmdval 17435	Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼)    &   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩})
Theorem	frmdbas 17436	The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼)
Theorem	frmdelbas 17437	An element of the base set of a free monoid is a string on the generators. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝐼)
Theorem	frmdplusg 17438	The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))
Theorem	frmdadd 17439	Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌))
Theorem	vrmdfval 17440*	The canonical injection from the generating set 𝐼 to the base set of the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑈 = (𝑗 ∈ 𝐼 ↦ ⟨“𝑗”⟩))
Theorem	vrmdval 17441	The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = ⟨“𝐴”⟩)
Theorem	vrmdf 17442	The mapping from the index set to the generators is a function into the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶Word 𝐼)
Theorem	frmdmnd 17443	A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd)
Theorem	frmd0 17444	The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ ∅ = (0g‘𝑀)
Theorem	frmdsssubm 17445	The set of words taking values in a subset is a (free) submonoid of the free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼) → Word 𝐽 ∈ (SubMnd‘𝑀))
Theorem	frmdgsum 17446	Any word in a free monoid can be expressed as the sum of the singletons composing it. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐼) → (𝑀 Σg (𝑈 ∘ 𝑊)) = 𝑊)
Theorem	frmdss2 17447	A subset of generators is contained in a submonoid iff the set of words on the generators is in the submonoid. This can be viewed as an elementary way of saying "the monoidal closure of 𝐽 is Word 𝐽". (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ (SubMnd‘𝑀)) → ((𝑈 “ 𝐽) ⊆ 𝐴 ↔ Word 𝐽 ⊆ 𝐴))
Theorem	frmdup1 17448*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝑀 MndHom 𝐺))
Theorem	frmdup2 17449*	The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝐸‘(𝑈‘𝑌)) = (𝐴‘𝑌))
Theorem	frmdup3lem 17450*	Lemma for frmdup3 17451. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))))
Theorem	frmdup3 17451*	Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) → ∃!𝑚 ∈ (𝑀 MndHom 𝐺)(𝑚 ∘ 𝑈) = 𝐴)
10.1.9  Examples and counterexamples for magmas, semigroups and monoids
Theorem	mgm2nsgrplem1 17452*	Lemma 1 for mgm2nsgrp 17456: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 17301). (Contributed by AV, 27-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm)
Theorem	mgm2nsgrplem2 17453*	Lemma 2 for mgm2nsgrp 17456. (Contributed by AV, 27-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ⚬ 𝐴) ⚬ 𝐵) = 𝐴)
Theorem	mgm2nsgrplem3 17454*	Lemma 3 for mgm2nsgrp 17456. (Contributed by AV, 28-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⚬ (𝐴 ⚬ 𝐵)) = 𝐵)
Theorem	mgm2nsgrplem4 17455*	Lemma 4 for mgm2nsgrp 17456: M is not a semigroup. (Contributed by AV, 28-Jan-2020.) (Proof shortened by AV, 31-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    ⇒   ⊢ ((#‘𝑆) = 2 → 𝑀 ∉ SGrp)
Theorem	mgm2nsgrp 17456*	A small magma (with two elements) which is not a semigroup. (Contributed by AV, 28-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴))    ⇒   ⊢ ((#‘𝑆) = 2 → (𝑀 ∈ Mgm ∧ 𝑀 ∉ SGrp))
Theorem	sgrp2nmndlem1 17457*	Lemma 1 for sgrp2nmnd 17464: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 17301). (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm)
Theorem	sgrp2nmndlem2 17458*	Lemma 2 for sgrp2nmnd 17464. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ⚬ 𝐶) = 𝐴)
Theorem	sgrp2nmndlem3 17459*	Lemma 3 for sgrp2nmnd 17464. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐶) = 𝐵)
Theorem	sgrp2rid2 17460*	A small semigroup (with two elements) with two right identities which are different if 𝐴 ≠ 𝐵. (Contributed by AV, 10-Feb-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑦 ⚬ 𝑥) = 𝑦)
Theorem	sgrp2rid2ex 17461*	A small semigroup (with two elements) with two right identities which are different. (Contributed by AV, 10-Feb-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((#‘𝑆) = 2 → ∃𝑥 ∈ 𝑆 ∃𝑧 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ≠ 𝑧 ∧ (𝑦 ⚬ 𝑥) = 𝑦 ∧ (𝑦 ⚬ 𝑧) = 𝑦))
Theorem	sgrp2nmndlem4 17462*	Lemma 4 for sgrp2nmnd 17464: M is a semigroup. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((#‘𝑆) = 2 → 𝑀 ∈ SGrp)
Theorem	sgrp2nmndlem5 17463*	Lemma 5 for sgrp2nmnd 17464: M is not a monoid. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((#‘𝑆) = 2 → 𝑀 ∉ Mnd)
Theorem	sgrp2nmnd 17464*	A small semigroup (with two elements) which is not a monoid. (Contributed by AV, 26-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((#‘𝑆) = 2 → (𝑀 ∈ SGrp ∧ 𝑀 ∉ Mnd))
Theorem	mgmnsgrpex 17465	There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.)
⊢ ∃𝑚 ∈ Mgm 𝑚 ∉ SGrp
Theorem	sgrpnmndex 17466	There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.)
⊢ ∃𝑚 ∈ SGrp 𝑚 ∉ Mnd
Theorem	sgrpssmgm 17467	The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.)
⊢ SGrp ⊊ Mgm
Theorem	mndsssgrp 17468	The class of all monoids is a proper subclass of the class of all semigroups. (Contributed by AV, 29-Jan-2020.)
⊢ Mnd ⊊ SGrp
10.2  Groups
10.2.1  Definition and basic properties
Syntax	cgrp 17469	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 17470	Extend class notation with inverse of group element.
class invg
Syntax	csg 17471	Extend class notation with group subtraction (or division) operation.
class -g
Definition	df-grp 17472*	Define class of all groups. A group is a monoid (df-mnd 17342) whose internal operation is such that every element admits a left inverse (which can be proven to be a two-sided inverse). Thus, a group 𝐺 is an algebraic structure formed from a base set of elements (notated (Base‘𝐺) per df-base 15910) and an internal group operation (notated (+g‘𝐺) per df-plusg 16001). The operation combines any two elements of the group base set and must satisfy the 4 group axioms: closure (the result of the group operation must always be a member of the base set, see grpcl 17477), associativity (so ((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see grpass 17478), identity (there must be an element 𝑒 = (0g‘𝐺) such that 𝑒+g𝑎 = 𝑎+g𝑒 = 𝑎 for any a), and inverse (for each element a in the base set, there must be an element 𝑏 = invg𝑎 in the base set such that 𝑎+g𝑏 = 𝑏+g𝑎 = 𝑒). It can be proven that the identity element is unique (grpideu 17480). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 18242). Subgroups can often be formed from groups, see df-subg 17638. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition), as proven in cnaddablx 18317; an Abelian group is a group as proven in ablgrp 18244. Other structures include groups, including unital rings (df-ring 18595) and fields (df-field 18798). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}
Definition	df-minusg 17473*	Define inverse of group element. (Contributed by NM, 24-Aug-2011.)
⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))
Definition	df-sbg 17474*	Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.)
⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))
Theorem	isgrp 17475*	The predicate "is a group." (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ 𝐵 ∃𝑚 ∈ 𝐵 (𝑚 + 𝑎) = 0 ))
Theorem	grpmnd 17476	A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
Theorem	grpcl 17477	Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	grpass 17478	A group operation is associative. (Contributed by NM, 14-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	grpinvex 17479*	Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 )
Theorem	grpideu 17480*	The two-sided identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 8-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥))
Theorem	grpplusf 17481	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)⟶𝐵)
Theorem	grpplusfo 17482	The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)–onto→𝐵)
Theorem	resgrpplusfrn 17483	The underlying set of a group operation which is a restriction of a structure. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ 𝐹 = (+𝑓‘𝐻)    ⇒   ⊢ ((𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝑆 = ran 𝐹)
Theorem	grppropd 17484*	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp))
Theorem	grpprop 17485	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by NM, 11-Oct-2013.)
⊢ (Base‘𝐾) = (Base‘𝐿)    &   ⊢ (+g‘𝐾) = (+g‘𝐿)    ⇒   ⊢ (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp)
Theorem	grppropstr 17486	Generalize a specific 2-element group 𝐿 to show that any set 𝐾 with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ (Base‘𝐾) = 𝐵    &   ⊢ (+g‘𝐾) = +    &   ⊢ 𝐿 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp)
Theorem	grpss 17487	Show that a structure extending a constructed group (e.g., a ring) is also a group. This allows us to prove that a constructed potential ring 𝑅 is a group before we know that it is also a ring. (Theorem ringgrp 18598, on the other hand, requires that we know in advance that 𝑅 is a ring.) (Contributed by NM, 11-Oct-2013.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    &   ⊢ 𝑅 ∈ V    &   ⊢ 𝐺 ⊆ 𝑅    &   ⊢ Fun 𝑅    ⇒   ⊢ (𝐺 ∈ Grp ↔ 𝑅 ∈ Grp)
Theorem	isgrpd2e 17488*	Deduce a group from its properties. In this version of isgrpd2 17489, we don't assume there is an expression for the inverse of 𝑥. (Contributed by NM, 10-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 = (0g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpd2 17489*	Deduce a group from its properties. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). Note: normally we don't use a 𝜑 antecedent on hypotheses that name structure components, since they can be eliminated with eqid 2651, but we make an exception for theorems such as isgrpd2 17489, ismndd 17360, and islmodd 18917 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 = (0g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpde 17490*	Deduce a group from its properties. In this version of isgrpd 17491, we don't assume there is an expression for the inverse of 𝑥. (Contributed by NM, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpd 17491*	Deduce a group from its properties. Unlike isgrpd2 17489, this one goes straight from the base properties rather than going through Mnd. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 6-Jun-2013.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpi 17492*	Properties that determine a group. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 3-Sep-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ 0 ∈ 𝐵    &   ⊢ (𝑥 ∈ 𝐵 → ( 0 + 𝑥) = 𝑥)    &   ⊢ (𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ 𝐺 ∈ Grp
Theorem	grpsgrp 17493	A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
⊢ (𝐺 ∈ Grp → 𝐺 ∈ SGrp)
Theorem	dfgrp2 17494*	Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp 17472, based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ SGrp ∧ ∃𝑛 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑥) = 𝑛)))
Theorem	dfgrp2e 17495*	Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in [Lang] p. 7. (Contributed by NM, 10-Oct-2006.) (Revised by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) ∧ ∃𝑛 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑥) = 𝑛)))
Theorem	isgrpix 17496*	Properties that determine a group. Read 𝑁 as 𝑁(𝑥). Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ + ∈ V    &   ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩}    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ 0 ∈ 𝐵    &   ⊢ (𝑥 ∈ 𝐵 → ( 0 + 𝑥) = 𝑥)    &   ⊢ (𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ 𝐺 ∈ Grp
Theorem	grpidcl 17497	The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)
Theorem	grpbn0 17498	The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
Theorem	grplid 17499	The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
Theorem	grprid 17500	The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)