Step |
Hyp |
Ref |
Expression |
1 |
|
submgmcl.p |
⊢ + = ( +g ‘ 𝑀 ) |
2 |
|
submgmrcl |
⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → 𝑀 ∈ Mgm ) |
3 |
|
eqid |
⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) |
4 |
3 1
|
issubmgm |
⊢ ( 𝑀 ∈ Mgm → ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ) ) |
5 |
2 4
|
syl |
⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ) ) |
6 |
5
|
ibi |
⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) ) |
7 |
6
|
simprd |
⊢ ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) |
8 |
|
ovrspc2v |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 + 𝑦 ) ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 ) |
9 |
7 8
|
sylan2 |
⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 ) |
10 |
9
|
ancoms |
⊢ ( ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 ) |
11 |
10
|
3impb |
⊢ ( ( 𝑆 ∈ ( SubMgm ‘ 𝑀 ) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 + 𝑌 ) ∈ 𝑆 ) |