P. 139 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13801-13900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfgrp3m 13801*	Alternate definition of a group as semigroup (with at least one element) which is also a quasigroup, i.e. a magma in which solutions 𝑥 and 𝑦 of the equations (𝑎 + 𝑥) = 𝑏 and (𝑥 + 𝑎) = 𝑏 exist. Theorem 3.2 of [Bruck] p. 28. (Contributed by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ ∃𝑤 𝑤 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)))
Theorem	dfgrp3me 13802*	Alternate definition of a group as a set with a closed, associative operation, for which solutions 𝑥 and 𝑦 of the equations (𝑎 + 𝑥) = 𝑏 and (𝑥 + 𝑎) = 𝑏 exist. Exercise 1 of [Herstein] p. 57. (Contributed by NM, 5-Dec-2006.) (Revised by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (∃𝑤 𝑤 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))
Theorem	grplactfval 13803*	The left group action of element 𝐴 of group 𝐺. (Contributed by Paul Chapman, 18-Mar-2008.)
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝐹‘𝐴) = (𝑎 ∈ 𝑋 ↦ (𝐴 + 𝑎)))
Theorem	grplactcnv 13804*	The left group action of element 𝐴 of group 𝐺 maps the underlying set 𝑋 of 𝐺 one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡(𝐹‘𝐴) = (𝐹‘(𝐼‘𝐴))))
Theorem	grplactf1o 13805*	The left group action of element 𝐴 of group 𝐺 maps the underlying set 𝑋 of 𝐺 one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴):𝑋–1-1-onto→𝑋)
Theorem	grpsubpropdg 13806	Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.)
⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))    &   ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    ⇒   ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻))
Theorem	grpsubpropd2 13807*	Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦))    ⇒   ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻))
Theorem	grp1 13808	The (smallest) structure representing a trivial group. According to Wikipedia ("Trivial group", 28-Apr-2019, https://en.wikipedia.org/wiki/Trivial_group) "In mathematics, a trivial group is a group consisting of a single element. All such groups are isomorphic, so one often speaks of the trivial group. The single element of the trivial group is the identity element". (Contributed by AV, 28-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Grp)
Theorem	grp1inv 13809	The inverse function of the trivial group. (Contributed by FL, 21-Jun-2010.) (Revised by AV, 26-Aug-2021.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (invg‘𝑀) = ( I ↾ {𝐼}))
Theorem	prdsinvlem 13810*	Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Grp)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 0 = (0g ∘ 𝑅)    &   ⊢ 𝑁 = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ (𝑁 + 𝐹) = 0 ))
Theorem	prdsgrpd 13811	The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Grp)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Grp)
Theorem	prdsinvgd 13812*	Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Grp)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑁 = (invg‘𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = (𝑥 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑥))‘(𝑋‘𝑥))))
Theorem	pwsgrp 13813	A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Grp)
Theorem	pwsinvg 13814	Negation in a group power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑀 = (invg‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑌)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = (𝑀 ∘ 𝑋))
Theorem	pwssub 13815	Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑀 = (-g‘𝑅)    &   ⊢ − = (-g‘𝑌)    ⇒   ⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹 − 𝐺) = (𝐹 ∘𝑓 𝑀𝐺))
Theorem	imasgrp2 13816*	The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))    &   ⊢ (𝜑 → 0 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 ))    ⇒   ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0g‘𝑈)))
Theorem	imasgrp 13817*	The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0g‘𝑈)))
Theorem	imasgrpf1 13818	The image of a group under an injection is a group. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑈 = (𝐹 “s 𝑅)    &   ⊢ 𝑉 = (Base‘𝑅)    ⇒   ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Grp) → 𝑈 ∈ Grp)
Theorem	qusgrp2 13819*	Prove that a quotient structure is a group. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) ∼ (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) ∼ 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) ∼ 0 )    ⇒   ⊢ (𝜑 → (𝑈 ∈ Grp ∧ [ 0 ] ∼ = (0g‘𝑈)))
Theorem	mhmlem 13820*	Lemma for mhmmnd 13822 and ghmgrp 13824. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵)))
Theorem	mhmid 13821*	A surjective monoid morphism preserves identity element. (Contributed by Thierry Arnoux, 25-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑌 = (Base‘𝐻)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → (𝐹‘ 0 ) = (0g‘𝐻))
Theorem	mhmmnd 13822*	The image of a monoid 𝐺 under a monoid homomorphism 𝐹 is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑌 = (Base‘𝐻)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐻 ∈ Mnd)
Theorem	mhmfmhm 13823*	The function fulfilling the conditions of mhmmnd 13822 is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑌 = (Base‘𝐻)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐺 MndHom 𝐻))
Theorem	ghmgrp 13824*	The image of a group 𝐺 under a group homomorphism 𝐹 is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator 𝑂 in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑌 = (Base‘𝐻)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐻 ∈ Grp)
7.2.2  Group multiple operation The "group multiple" operation (if the group is multiplicative, also called "group power" or "group exponentiation" operation), can be defined for arbitrary magmas, if the multiplier/exponent is a nonnegative integer. See also the definition in [Lang] p. 6, where an element 𝑥(of a monoid) to the power of a nonnegative integer 𝑛 is defined and denoted by 𝑥↑𝑛. Definition df-mulg 13826, however, defines the group multiple for arbitrary (i.e. also negative) integers. This is meaningful for groups only, and requires Definition df-minusg 13706 of the inverse operation invg.
Syntax	cmg 13825	Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group.
class .g
Definition	df-mulg 13826*	Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘-𝑛))))))
Theorem	mulgfvalg 13827*	Group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → · = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))))
Theorem	mulgval 13828	Value of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑆 = seq1( + , (ℕ × {𝑋}))    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = if(𝑁 = 0, 0 , if(0 < 𝑁, (𝑆‘𝑁), (𝐼‘(𝑆‘-𝑁)))))
Theorem	mulgex 13829	Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.)
⊢ (𝐺 ∈ 𝑉 → (.g‘𝐺) ∈ V)
Theorem	mulgfng 13830	Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → · Fn (ℤ × 𝐵))
Theorem	mulg0 13831	Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 )
Theorem	mulgnn 13832	Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑆 = seq1( + , (ℕ × {𝑋}))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝑆‘𝑁))
Theorem	mulgnngsum 13833*	Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑁) ↦ 𝑋)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝐺 Σg 𝐹))
Theorem	mulgnn0gsum 13834*	Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in [Lang] p. 6, second formula. (Contributed by AV, 28-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑁) ↦ 𝑋)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝐺 Σg 𝐹))
Theorem	mulg1 13835	Group multiple (exponentiation) operation at one. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (1 · 𝑋) = 𝑋)
Theorem	mulgnnp1 13836	Group multiple (exponentiation) operation at a successor. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
Theorem	mulg2 13837	Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (2 · 𝑋) = (𝑋 + 𝑋))
Theorem	mulgnegnn 13838	Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝐼‘(𝑁 · 𝑋)))
Theorem	mulgnn0p1 13839	Group multiple (exponentiation) operation at a successor, extended to ℕ0. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
Theorem	mulgnnsubcl 13840*	Closure of the group multiple (exponentiation) operation in a subsemigroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	mulgnn0subcl 13841*	Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 0 ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	mulgsubcl 13842*	Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 0 ∈ 𝑆)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	mulgnncl 13843	Closure of the group multiple (exponentiation) operation for a positive multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgnn0cl 13844	Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgcl 13845	Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgneg 13846	Group multiple (exponentiation) operation at a negative integer. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝐼‘(𝑁 · 𝑋)))
Theorem	mulgnegneg 13847	The inverse of a negative group multiple is the positive group multiple. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐼‘(-𝑁 · 𝑋)) = (𝑁 · 𝑋))
Theorem	mulgm1 13848	Group multiple (exponentiation) operation at negative one. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 20-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (-1 · 𝑋) = (𝐼‘𝑋))
Theorem	mulgnn0cld 13849	Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13844. (Contributed by SN, 1-Feb-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgcld 13850	Deduction associated with mulgcl 13845. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgaddcomlem 13851	Lemma for mulgaddcom 13852. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ ((𝑦 · 𝑋) + 𝑋) = (𝑋 + (𝑦 · 𝑋))) → ((-𝑦 · 𝑋) + 𝑋) = (𝑋 + (-𝑦 · 𝑋)))
Theorem	mulgaddcom 13852	The group multiple operator commutes with the group operation. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑁 · 𝑋) + 𝑋) = (𝑋 + (𝑁 · 𝑋)))
Theorem	mulginvcom 13853	The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · (𝐼‘𝑋)) = (𝐼‘(𝑁 · 𝑋)))
Theorem	mulginvinv 13854	The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐼‘(𝑁 · (𝐼‘𝑋))) = (𝑁 · 𝑋))
Theorem	mulgnn0z 13855	A group multiple of the identity, for nonnegative multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0) → (𝑁 · 0 ) = 0 )
Theorem	mulgz 13856	A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝑁 · 0 ) = 0 )
Theorem	mulgnndir 13857	Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
Theorem	mulgnn0dir 13858	Sum of group multiples, generalized to ℕ0. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
Theorem	mulgdirlem 13859	Lemma for mulgdir 13860. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
Theorem	mulgdir 13860	Sum of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
Theorem	mulgp1 13861	Group multiple (exponentiation) operation at a successor, extended to ℤ. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
Theorem	mulgneg2 13862	Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝑁 · (𝐼‘𝑋)))
Theorem	mulgnnass 13863	Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014.) (Revised by AV, 29-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
Theorem	mulgnn0ass 13864	Product of group multiples, generalized to ℕ0. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
Theorem	mulgass 13865	Product of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
Theorem	mulgassr 13866	Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑁 · 𝑀) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
Theorem	mulgmodid 13867	Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 mod 𝑀) · 𝑋) = (𝑁 · 𝑋))
Theorem	mulgsubdir 13868	Distribution of group multiples over subtraction for group elements, subdir 8655 analog. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 − 𝑁) · 𝑋) = ((𝑀 · 𝑋) − (𝑁 · 𝑋)))
Theorem	mhmmulg 13869	A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ × = (.g‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))
Theorem	mulgpropdg 13870*	Two structures with the same group-nature have the same group multiple function. 𝐾 is expected to either be V (when strong equality is available) or 𝐵 (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 → · = (.g‘𝐺))    &   ⊢ (𝜑 → × = (.g‘𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐻))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐾)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦))    ⇒   ⊢ (𝜑 → · = × )
Theorem	submmulgcl 13871	Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ ∙ = (.g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) ∈ 𝑆)
Theorem	submmulg 13872	A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ ∙ = (.g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ · = (.g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) = (𝑁 · 𝑋))
7.2.3  Subgroups and Quotient groups
Syntax	csubg 13873	Extend class notation with all subgroups of a group.
class SubGrp
Syntax	cnsg 13874	Extend class notation with all normal subgroups of a group.
class NrmSGrp
Syntax	cqg 13875	Quotient group equivalence class.
class ~QG
Definition	df-subg 13876*	Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2m 13895), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 13890), contains the neutral element of the group (see subg0 13886) and contains the inverses for all of its elements (see subginvcl 13889). (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp})
Definition	df-nsg 13877*	Define the equivalence relation in a quotient ring or quotient group (where 𝑖 is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ NrmSGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})
Definition	df-eqg 13878*	Define the equivalence relation in a group generated by a subgroup. More precisely, if 𝐺 is a group and 𝐻 is a subgroup, then 𝐺 ~QG 𝐻 is the equivalence relation on 𝐺 associated with the left cosets of 𝐻. A typical application of this definition is the construction of the quotient group (resp. ring) of a group (resp. ring) by a normal subgroup (resp. two-sided ideal). (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ ~QG = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)})
Theorem	issubg 13879	The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
Theorem	subgss 13880	A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)
Theorem	subgid 13881	A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (SubGrp‘𝐺))
Theorem	subgex 13882	The class of subgroups of a group is a set. (Contributed by Jim Kingdon, 8-Mar-2025.)
⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ V)
Theorem	subggrp 13883	A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
Theorem	subgbas 13884	The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻))
Theorem	subgrcl 13885	Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
Theorem	subg0 13886	A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘𝐻))
Theorem	subginv 13887	The inverse of an element in a subgroup is the same as the inverse in the larger group. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝐽 = (invg‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆) → (𝐼‘𝑋) = (𝐽‘𝑋))
Theorem	subg0cl 13888	The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)
Theorem	subginvcl 13889	The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆) → (𝐼‘𝑋) ∈ 𝑆)
Theorem	subgcl 13890	A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	subgsubcl 13891	A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 − 𝑌) ∈ 𝑆)
Theorem	subgsub 13892	The subtraction of elements in a subgroup is the same as subtraction in the group. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ − = (-g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ 𝑁 = (-g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 − 𝑌) = (𝑋𝑁𝑌))
Theorem	subgmulgcl 13893	Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	subgmulg 13894	A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ · = (.g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ ∙ = (.g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) = (𝑁 ∙ 𝑋))
Theorem	issubg2m 13895*	Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑢 𝑢 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))))
Theorem	issubgrpd2 13896*	Prove a subgroup by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷))    &   ⊢ (𝜑 → 0 = (0g‘𝐼))    &   ⊢ (𝜑 → + = (+g‘𝐼))    &   ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼))    &   ⊢ (𝜑 → 0 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (SubGrp‘𝐼))
Theorem	issubgrpd 13897*	Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷))    &   ⊢ (𝜑 → 0 = (0g‘𝐼))    &   ⊢ (𝜑 → + = (+g‘𝐼))    &   ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼))    &   ⊢ (𝜑 → 0 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Grp)
Theorem	issubg3 13898*	A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)))
Theorem	issubg4m 13899*	A subgroup is an inhabited subset of the group closed under subtraction. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ ∃𝑤 𝑤 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 − 𝑦) ∈ 𝑆)))
Theorem	grpissubg 13900	If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the (base set of the) group is subgroup of the other group. (Contributed by AV, 14-Mar-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺)))