Step |
Hyp |
Ref |
Expression |
1 |
|
issubmndb.b |
|- B = ( Base ` G ) |
2 |
|
issubmndb.z |
|- .0. = ( 0g ` G ) |
3 |
|
eqid |
|- ( G |`s S ) = ( G |`s S ) |
4 |
1 2 3
|
issubm2 |
|- ( G e. Mnd -> ( S e. ( SubMnd ` G ) <-> ( S C_ B /\ .0. e. S /\ ( G |`s S ) e. Mnd ) ) ) |
5 |
|
3anrot |
|- ( ( ( G |`s S ) e. Mnd /\ S C_ B /\ .0. e. S ) <-> ( S C_ B /\ .0. e. S /\ ( G |`s S ) e. Mnd ) ) |
6 |
|
3anass |
|- ( ( ( G |`s S ) e. Mnd /\ S C_ B /\ .0. e. S ) <-> ( ( G |`s S ) e. Mnd /\ ( S C_ B /\ .0. e. S ) ) ) |
7 |
5 6
|
bitr3i |
|- ( ( S C_ B /\ .0. e. S /\ ( G |`s S ) e. Mnd ) <-> ( ( G |`s S ) e. Mnd /\ ( S C_ B /\ .0. e. S ) ) ) |
8 |
4 7
|
bitrdi |
|- ( G e. Mnd -> ( S e. ( SubMnd ` G ) <-> ( ( G |`s S ) e. Mnd /\ ( S C_ B /\ .0. e. S ) ) ) ) |
9 |
8
|
pm5.32i |
|- ( ( G e. Mnd /\ S e. ( SubMnd ` G ) ) <-> ( G e. Mnd /\ ( ( G |`s S ) e. Mnd /\ ( S C_ B /\ .0. e. S ) ) ) ) |
10 |
|
submrcl |
|- ( S e. ( SubMnd ` G ) -> G e. Mnd ) |
11 |
10
|
pm4.71ri |
|- ( S e. ( SubMnd ` G ) <-> ( G e. Mnd /\ S e. ( SubMnd ` G ) ) ) |
12 |
|
anass |
|- ( ( ( G e. Mnd /\ ( G |`s S ) e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) <-> ( G e. Mnd /\ ( ( G |`s S ) e. Mnd /\ ( S C_ B /\ .0. e. S ) ) ) ) |
13 |
9 11 12
|
3bitr4i |
|- ( S e. ( SubMnd ` G ) <-> ( ( G e. Mnd /\ ( G |`s S ) e. Mnd ) /\ ( S C_ B /\ .0. e. S ) ) ) |