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

Metamath Proof Explorer

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 )