This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 ‘ 𝐺 ) → ( 𝑈 ⊕ 𝑈 ) = 𝑈 ) |