Step |
Hyp |
Ref |
Expression |
1 |
|
issubm2.b |
|- B = ( Base ` M ) |
2 |
|
issubm2.z |
|- .0. = ( 0g ` M ) |
3 |
|
issubm2.h |
|- H = ( M |`s S ) |
4 |
|
eqid |
|- ( +g ` M ) = ( +g ` M ) |
5 |
1 2 4
|
issubm |
|- ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) ) |
6 |
1 4 2 3
|
issubmnd |
|- ( ( M e. Mnd /\ S C_ B /\ .0. e. S ) -> ( H e. Mnd <-> A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) |
7 |
6
|
bicomd |
|- ( ( M e. Mnd /\ S C_ B /\ .0. e. S ) -> ( A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S <-> H e. Mnd ) ) |
8 |
7
|
3expb |
|- ( ( M e. Mnd /\ ( S C_ B /\ .0. e. S ) ) -> ( A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S <-> H e. Mnd ) ) |
9 |
8
|
pm5.32da |
|- ( M e. Mnd -> ( ( ( S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) <-> ( ( S C_ B /\ .0. e. S ) /\ H e. Mnd ) ) ) |
10 |
|
df-3an |
|- ( ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) <-> ( ( S C_ B /\ .0. e. S ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) |
11 |
|
df-3an |
|- ( ( S C_ B /\ .0. e. S /\ H e. Mnd ) <-> ( ( S C_ B /\ .0. e. S ) /\ H e. Mnd ) ) |
12 |
9 10 11
|
3bitr4g |
|- ( M e. Mnd -> ( ( S C_ B /\ .0. e. S /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) <-> ( S C_ B /\ .0. e. S /\ H e. Mnd ) ) ) |
13 |
5 12
|
bitrd |
|- ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ B /\ .0. e. S /\ H e. Mnd ) ) ) |