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 ` G ) |
|
| Assertion | lsmidm | |- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | lsmub1.p | |- .(+) = ( LSSum ` G ) |
|
| 2 | subgsubm | |- ( U e. ( SubGrp ` G ) -> U e. ( SubMnd ` G ) ) |
|
| 3 | 1 | smndlsmidm | |- ( U e. ( SubMnd ` G ) -> ( U .(+) U ) = U ) |
| 4 | 2 3 | syl | |- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U ) |