Step |
Hyp |
Ref |
Expression |
1 |
|
mndissubm.b |
|- B = ( Base ` G ) |
2 |
|
mndissubm.s |
|- S = ( Base ` H ) |
3 |
|
mndissubm.z |
|- .0. = ( 0g ` G ) |
4 |
|
simpr1 |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> S C_ B ) |
5 |
|
simpr2 |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> .0. e. S ) |
6 |
|
mndmgm |
|- ( G e. Mnd -> G e. Mgm ) |
7 |
|
mndmgm |
|- ( H e. Mnd -> H e. Mgm ) |
8 |
6 7
|
anim12i |
|- ( ( G e. Mnd /\ H e. Mnd ) -> ( G e. Mgm /\ H e. Mgm ) ) |
9 |
8
|
ad2antrr |
|- ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ ( a e. S /\ b e. S ) ) -> ( G e. Mgm /\ H e. Mgm ) ) |
10 |
|
3simpb |
|- ( ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) |
11 |
10
|
ad2antlr |
|- ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ ( a e. S /\ b e. S ) ) -> ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) |
12 |
|
simpr |
|- ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ ( a e. S /\ b e. S ) ) -> ( a e. S /\ b e. S ) ) |
13 |
1 2
|
mgmsscl |
|- ( ( ( G e. Mgm /\ H e. Mgm ) /\ ( S C_ B /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) /\ ( a e. S /\ b e. S ) ) -> ( a ( +g ` G ) b ) e. S ) |
14 |
9 11 12 13
|
syl3anc |
|- ( ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) /\ ( a e. S /\ b e. S ) ) -> ( a ( +g ` G ) b ) e. S ) |
15 |
14
|
ralrimivva |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> A. a e. S A. b e. S ( a ( +g ` G ) b ) e. S ) |
16 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
17 |
1 3 16
|
issubm |
|- ( G e. Mnd -> ( S e. ( SubMnd ` G ) <-> ( S C_ B /\ .0. e. S /\ A. a e. S A. b e. S ( a ( +g ` G ) b ) e. S ) ) ) |
18 |
17
|
ad2antrr |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> ( S e. ( SubMnd ` G ) <-> ( S C_ B /\ .0. e. S /\ A. a e. S A. b e. S ( a ( +g ` G ) b ) e. S ) ) ) |
19 |
4 5 15 18
|
mpbir3and |
|- ( ( ( G e. Mnd /\ H e. Mnd ) /\ ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) ) -> S e. ( SubMnd ` G ) ) |
20 |
19
|
ex |
|- ( ( G e. Mnd /\ H e. Mnd ) -> ( ( S C_ B /\ .0. e. S /\ ( +g ` H ) = ( ( +g ` G ) |` ( S X. S ) ) ) -> S e. ( SubMnd ` G ) ) ) |