This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem submcl

Description: Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypothesis submcl.p ⊢ + = ( +g ‘ 𝑀 )
Assertion submcl ( ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 submcl.p ⊢ + = ( +g ‘ 𝑀 )
2 submrcl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑀 ∈ Mnd )
3 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
4 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
5 3 4 1 issubm ⊢ ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ) )
6 2 5 syl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ) )
7 6 ibi ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ( 0g ‘ 𝑀 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) )
8 7 simp3d ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 )
9 ovrspc2v ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )
10 8 9 sylan2 ⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )
11 10 ancoms ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )
12 11 3impb ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 )