Theorem lsmidm

Description: Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014) (Proof shortened by AV, 27-Dec-2023)

	Ref	Expression
Hypothesis	lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
Assertion	lsmidm	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lsmub1.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2		subgsubm	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ∈ ( SubMnd ‘ 𝐺 ) )
3	1	smndlsmidm	⊢ ( 𝑈 ∈ ( SubMnd ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = 𝑈 )
4	2 3	syl	⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = 𝑈 )