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 ) |
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 ) |