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