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 ⊢ M ∈ V ∧ Base M = ∅ → M ∈ Smgrp

Proof

Step Hyp Ref Expression
1 mgm0 ⊢ M ∈ V ∧ Base M = ∅ → M ∈ Mgm
2 rzal ⊢ Base M = ∅ → ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
3 2 adantl ⊢ M ∈ V ∧ Base M = ∅ → ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
4 eqid ⊢ Base M = Base M
5 eqid ⊢ + M = + M
6 4 5 issgrp ⊢ M ∈ Smgrp ↔ M ∈ Mgm ∧ ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
7 1 3 6 sylanbrc ⊢ M ∈ V ∧ Base M = ∅ → M ∈ Smgrp