This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issubm2

Description: Submonoids are subsets that are also monoids with the same zero. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypotheses issubm2.b 
|- B = ( Base ` M )
issubm2.z 
|- .0. = ( 0g ` M )
issubm2.h 
|- H = ( M |`s S )
Assertion issubm2 
|- ( M e. Mnd -> ( S e. ( SubMnd ` M ) <-> ( S C_ B /\ .0. e. S /\ H e. Mnd ) ) )

Proof

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 ) ) )