Theorem sgrp0

Description: Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021)

	Ref	Expression
Assertion	sgrp0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → 𝑀 ∈ Smgrp )

Proof

Step	Hyp	Ref	Expression
1		mgm0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → 𝑀 ∈ Mgm )
2		rzal	⊢ ( ( Base ‘ 𝑀 ) = ∅ → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ∀ 𝑧 ∈ ( Base ‘ 𝑀 ) ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) )
3	2	adantl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ∀ 𝑧 ∈ ( Base ‘ 𝑀 ) ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) )
4		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
5		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
6	4 5	issgrp	⊢ ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ∀ 𝑧 ∈ ( Base ‘ 𝑀 ) ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) )
7	1 3 6	sylanbrc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → 𝑀 ∈ Smgrp )