Step |
Hyp |
Ref |
Expression |
1 |
|
grpissubg.b |
|- B = ( Base ` G ) |
2 |
|
grpissubg.s |
|- S = ( Base ` H ) |
3 |
1 2
|
grpissubg |
|- ( ( G e. Grp /\ H e. Grp ) -> ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S e. ( SubGrp ` G ) ) ) |
4 |
3
|
imp |
|- ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> S e. ( SubGrp ` G ) ) |
5 |
|
ibar |
|- ( ( G e. Grp /\ S C_ B ) -> ( ( G |`s S ) e. Grp <-> ( ( G e. Grp /\ S C_ B ) /\ ( G |`s S ) e. Grp ) ) ) |
6 |
5
|
ad2ant2r |
|- ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( ( G |`s S ) e. Grp <-> ( ( G e. Grp /\ S C_ B ) /\ ( G |`s S ) e. Grp ) ) ) |
7 |
|
df-3an |
|- ( ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) <-> ( ( G e. Grp /\ S C_ B ) /\ ( G |`s S ) e. Grp ) ) |
8 |
6 7
|
bitr4di |
|- ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( ( G |`s S ) e. Grp <-> ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) ) ) |
9 |
1
|
issubg |
|- ( S e. ( SubGrp ` G ) <-> ( G e. Grp /\ S C_ B /\ ( G |`s S ) e. Grp ) ) |
10 |
8 9
|
bitr4di |
|- ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( ( G |`s S ) e. Grp <-> S e. ( SubGrp ` G ) ) ) |
11 |
4 10
|
mpbird |
|- ( ( ( G e. Grp /\ H e. Grp ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( G |`s S ) e. Grp ) |
12 |
11
|
ex |
|- ( ( G e. Grp /\ H e. Grp ) -> ( ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> ( G |`s S ) e. Grp ) ) |