Metamath Proof Explorer


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 )