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