This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 → ( 𝐵 ⊕ 𝐵 ) = 𝐵 )