Description: Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sgrpass.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
sgrpass.o | ⊢ ⚬ = ( +g ‘ 𝐺 ) | ||
Assertion | sgrpcl | ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sgrpass.b | ⊢ 𝐵 = ( Base ‘ 𝐺 ) | |
2 | sgrpass.o | ⊢ ⚬ = ( +g ‘ 𝐺 ) | |
3 | sgrpmgm | ⊢ ( 𝐺 ∈ Smgrp → 𝐺 ∈ Mgm ) | |
4 | 1 2 | mgmcl | ⊢ ( ( 𝐺 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 ) |
5 | 3 4 | syl3an1 | ⊢ ( ( 𝐺 ∈ Smgrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⚬ 𝑌 ) ∈ 𝐵 ) |