Theorem issubgrpd

Description: Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014)

	Ref	Expression
Hypotheses	issubgrpd.s	|- ( ph -> S = ( I |`s D ) )
	issubgrpd.z	|- ( ph -> .0. = ( 0g ` I ) )
	issubgrpd.p	|- ( ph -> .+ = ( +g ` I ) )
	issubgrpd.ss	|- ( ph -> D C_ ( Base ` I ) )
	issubgrpd.zcl	|- ( ph -> .0. e. D )
	issubgrpd.acl	|- ( ( ph /\ x e. D /\ y e. D ) -> ( x .+ y ) e. D )
	issubgrpd.ncl	|- ( ( ph /\ x e. D ) -> ( ( invg ` I ) ` x ) e. D )
	issubgrpd.g	|- ( ph -> I e. Grp )
Assertion	issubgrpd	|- ( ph -> S e. Grp )

Proof

Step	Hyp	Ref	Expression
1		issubgrpd.s	|- ( ph -> S = ( I |`s D ) )
2		issubgrpd.z	|- ( ph -> .0. = ( 0g ` I ) )
3		issubgrpd.p	|- ( ph -> .+ = ( +g ` I ) )
4		issubgrpd.ss	|- ( ph -> D C_ ( Base ` I ) )
5		issubgrpd.zcl	|- ( ph -> .0. e. D )
6		issubgrpd.acl	|- ( ( ph /\ x e. D /\ y e. D ) -> ( x .+ y ) e. D )
7		issubgrpd.ncl	|- ( ( ph /\ x e. D ) -> ( ( invg ` I ) ` x ) e. D )
8		issubgrpd.g	|- ( ph -> I e. Grp )
9	1 2 3 4 5 6 7 8	issubgrpd2	|- ( ph -> D e. ( SubGrp ` I ) )
10		eqid	|- ( I |`s D ) = ( I |`s D )
11	10	subggrp	|- ( D e. ( SubGrp ` I ) -> ( I |`s D ) e. Grp )
12	9 11	syl	|- ( ph -> ( I |`s D ) e. Grp )
13	1 12	eqeltrd	|- ( ph -> S e. Grp )