Metamath Proof Explorer

Theorem issubmndb

Description: The submonoid predicate. Analogous to issubg . (Contributed by AV, 1-Feb-2024)

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

Proof

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