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 )