Metamath Proof Explorer


Theorem lsmidmOLD

Description: Obsolete proof of lsmidm as of 13-Jan-2024. Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014) (Revised by Mario Carneiro, 21-Jun-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis lsmub1.p
|- .(+) = ( LSSum ` G )
Assertion lsmidmOLD
|- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U )

Proof

Step Hyp Ref Expression
1 lsmub1.p
 |-  .(+) = ( LSSum ` G )
2 eqid
 |-  ( Base ` G ) = ( Base ` G )
3 eqid
 |-  ( +g ` G ) = ( +g ` G )
4 2 3 1 lsmval
 |-  ( ( U e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( U .(+) U ) = ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) )
5 4 anidms
 |-  ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) )
6 3 subgcl
 |-  ( ( U e. ( SubGrp ` G ) /\ x e. U /\ y e. U ) -> ( x ( +g ` G ) y ) e. U )
7 6 3expb
 |-  ( ( U e. ( SubGrp ` G ) /\ ( x e. U /\ y e. U ) ) -> ( x ( +g ` G ) y ) e. U )
8 7 ralrimivva
 |-  ( U e. ( SubGrp ` G ) -> A. x e. U A. y e. U ( x ( +g ` G ) y ) e. U )
9 eqid
 |-  ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) = ( x e. U , y e. U |-> ( x ( +g ` G ) y ) )
10 9 fmpo
 |-  ( A. x e. U A. y e. U ( x ( +g ` G ) y ) e. U <-> ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) : ( U X. U ) --> U )
11 8 10 sylib
 |-  ( U e. ( SubGrp ` G ) -> ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) : ( U X. U ) --> U )
12 11 frnd
 |-  ( U e. ( SubGrp ` G ) -> ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) C_ U )
13 5 12 eqsstrd
 |-  ( U e. ( SubGrp ` G ) -> ( U .(+) U ) C_ U )
14 1 lsmub1
 |-  ( ( U e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U C_ ( U .(+) U ) )
15 14 anidms
 |-  ( U e. ( SubGrp ` G ) -> U C_ ( U .(+) U ) )
16 13 15 eqssd
 |-  ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U )