Theorem mndlsmidm

Description: Subgroup sum is idempotent for monoids. This corresponds to the observation in Lang p. 6. (Contributed by AV, 27-Dec-2023)

	Ref	Expression
Hypotheses	mndlsmidm.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
	mndlsmidm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	mndlsmidm	⊢ ( 𝐺 ∈ Mnd → ( 𝐵 ⊕ 𝐵 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mndlsmidm.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2		mndlsmidm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3	2	submid	⊢ ( 𝐺 ∈ Mnd → 𝐵 ∈ ( SubMnd ‘ 𝐺 ) )
4	1	smndlsmidm	⊢ ( 𝐵 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝐵 ⊕ 𝐵 ) = 𝐵 )
5	3 4	syl	⊢ ( 𝐺 ∈ Mnd → ( 𝐵 ⊕ 𝐵 ) = 𝐵 )