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 𝐵 = ( Base ‘ 𝑀 )
issubm2.z 0 = ( 0g𝑀 )
issubm2.h 𝐻 = ( 𝑀s 𝑆 )
Assertion issubm2 ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆𝐵0𝑆𝐻 ∈ Mnd ) ) )

Proof

Step Hyp Ref Expression
1 issubm2.b 𝐵 = ( Base ‘ 𝑀 )
2 issubm2.z 0 = ( 0g𝑀 )
3 issubm2.h 𝐻 = ( 𝑀s 𝑆 )
4 eqid ( +g𝑀 ) = ( +g𝑀 )
5 1 2 4 issubm ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆𝐵0𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝑆 ) ) )
6 1 4 2 3 issubmnd ( ( 𝑀 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) → ( 𝐻 ∈ Mnd ↔ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝑆 ) )
7 6 bicomd ( ( 𝑀 ∈ Mnd ∧ 𝑆𝐵0𝑆 ) → ( ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝑆𝐻 ∈ Mnd ) )
8 7 3expb ( ( 𝑀 ∈ Mnd ∧ ( 𝑆𝐵0𝑆 ) ) → ( ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝑆𝐻 ∈ Mnd ) )
9 8 pm5.32da ( 𝑀 ∈ Mnd → ( ( ( 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝑆 ) ↔ ( ( 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) ) )
10 df-3an ( ( 𝑆𝐵0𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝑆 ) ↔ ( ( 𝑆𝐵0𝑆 ) ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝑆 ) )
11 df-3an ( ( 𝑆𝐵0𝑆𝐻 ∈ Mnd ) ↔ ( ( 𝑆𝐵0𝑆 ) ∧ 𝐻 ∈ Mnd ) )
12 9 10 11 3bitr4g ( 𝑀 ∈ Mnd → ( ( 𝑆𝐵0𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝑀 ) 𝑦 ) ∈ 𝑆 ) ↔ ( 𝑆𝐵0𝑆𝐻 ∈ Mnd ) ) )
13 5 12 bitrd ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆𝐵0𝑆𝐻 ∈ Mnd ) ) )