Metamath Proof Explorer

Theorem issubgrpd2

Description: Prove a subgroup by closure (definition version). (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 issubgrpd2 
|- ( ph -> D e. ( SubGrp ` I ) )

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 5 ne0d 
 |-  ( ph -> D =/= (/) )
10 3 oveqd 
 |-  ( ph -> ( x .+ y ) = ( x ( +g ` I ) y ) )
11 10 ad2antrr 
 |-  ( ( ( ph /\ x e. D ) /\ y e. D ) -> ( x .+ y ) = ( x ( +g ` I ) y ) )
12 6 3expa 
 |-  ( ( ( ph /\ x e. D ) /\ y e. D ) -> ( x .+ y ) e. D )
13 11 12 eqeltrrd 
 |-  ( ( ( ph /\ x e. D ) /\ y e. D ) -> ( x ( +g ` I ) y ) e. D )
14 13 ralrimiva 
 |-  ( ( ph /\ x e. D ) -> A. y e. D ( x ( +g ` I ) y ) e. D )
15 14 7 jca 
 |-  ( ( ph /\ x e. D ) -> ( A. y e. D ( x ( +g ` I ) y ) e. D /\ ( ( invg ` I ) ` x ) e. D ) )
16 15 ralrimiva 
 |-  ( ph -> A. x e. D ( A. y e. D ( x ( +g ` I ) y ) e. D /\ ( ( invg ` I ) ` x ) e. D ) )
17 eqid 
 |-  ( Base ` I ) = ( Base ` I )
18 eqid 
 |-  ( +g ` I ) = ( +g ` I )
19 eqid 
 |-  ( invg ` I ) = ( invg ` I )
20 17 18 19 issubg2 
 |-  ( I e. Grp -> ( D e. ( SubGrp ` I ) <-> ( D C_ ( Base ` I ) /\ D =/= (/) /\ A. x e. D ( A. y e. D ( x ( +g ` I ) y ) e. D /\ ( ( invg ` I ) ` x ) e. D ) ) ) )
21 8 20 syl 
 |-  ( ph -> ( D e. ( SubGrp ` I ) <-> ( D C_ ( Base ` I ) /\ D =/= (/) /\ A. x e. D ( A. y e. D ( x ( +g ` I ) y ) e. D /\ ( ( invg ` I ) ` x ) e. D ) ) ) )
22 4 9 16 21 mpbir3and 
 |-  ( ph -> D e. ( SubGrp ` I ) )