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 ⊢ 𝐵 = ( 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 ) ) )