Metamath Proof Explorer


Theorem issubmndb

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

Ref Expression
Hypotheses issubmndb.b 𝐵 = ( Base ‘ 𝐺 )
issubmndb.z 0 = ( 0g𝐺 )
Assertion issubmndb ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 issubmndb.b 𝐵 = ( Base ‘ 𝐺 )
2 issubmndb.z 0 = ( 0g𝐺 )
3 eqid ( 𝐺s 𝑆 ) = ( 𝐺s 𝑆 )
4 1 2 3 issubm2 ( 𝐺 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑆𝐵0𝑆 ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) ) )
5 3anrot ( ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ↔ ( 𝑆𝐵0𝑆 ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) )
6 3anass ( ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ 𝑆𝐵0𝑆 ) ↔ ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) )
7 5 6 bitr3i ( ( 𝑆𝐵0𝑆 ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) ↔ ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) )
8 4 7 bitrdi ( 𝐺 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) ) )
9 8 pm5.32i ( ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) ↔ ( 𝐺 ∈ Mnd ∧ ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) ) )
10 submrcl ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → 𝐺 ∈ Mnd )
11 10 pm4.71ri ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝐺 ∈ Mnd ∧ 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ) )
12 anass ( ( ( 𝐺 ∈ Mnd ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ) ) ↔ ( 𝐺 ∈ Mnd ∧ ( ( 𝐺s 𝑆 ) ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) ) )
13 9 11 12 3bitr4i ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺s 𝑆 ) ∈ Mnd ) ∧ ( 𝑆𝐵0𝑆 ) ) )