Step |
Hyp |
Ref |
Expression |
1 |
|
mndissubm.b |
|- B = ( Base ` G ) |
2 |
|
mndissubm.s |
|- S = ( Base ` H ) |
3 |
|
mndissubm.z |
|- .0. = ( 0g ` G ) |
4 |
1 2 3
|
mndissubm |
|- ( ( G e. Mnd /\ H e. Mnd ) -> ( ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S e. ( SubMnd ` G ) ) ) |
5 |
4
|
imp |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> S e. ( SubMnd ` G ) ) |
6 |
|
simpl |
|- ( ( G e. Mnd /\ H e. Mnd ) -> G e. Mnd ) |
7 |
|
3simpa |
|- ( ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> ( S C_ B /\ .0. e. S ) ) |
8 |
6 7
|
anim12i |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( G e. Mnd /\ ( S C_ B /\ .0. e. S ) ) ) |
9 |
8
|
biantrud |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( ( G |`s S ) e. Mnd <-> ( ( G |`s S ) e. Mnd /\ ( G e. Mnd /\ ( S C_ B /\ .0. e. S ) ) ) ) ) |
10 |
|
an21 |
|- ( ( ( G e. Mnd /\ ( G |`s S ) e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) <-> ( ( G |`s S ) e. Mnd /\ ( G e. Mnd /\ ( S C_ B /\ .0. e. S ) ) ) ) |
11 |
9 10
|
bitr4di |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( ( G |`s S ) e. Mnd <-> ( ( G e. Mnd /\ ( G |`s S ) e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) ) ) |
12 |
1 3
|
issubmndb |
|- ( S e. ( SubMnd ` G ) <-> ( ( G e. Mnd /\ ( G |`s S ) e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) ) |
13 |
11 12
|
bitr4di |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( ( G |`s S ) e. Mnd <-> S e. ( SubMnd ` G ) ) ) |
14 |
5 13
|
mpbird |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( G |`s S ) e. Mnd ) |
15 |
14
|
ex |
|- ( ( G e. Mnd /\ H e. Mnd ) -> ( ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> ( G |`s S ) e. Mnd ) ) |