Metamath Proof Explorer

Theorem sgrp2sgrp

Description: Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020)

Ref Expression
Assertion sgrp2sgrp ⊢ M ∈ SGrpALT ↔ M ∈ Smgrp

Proof

Step Hyp Ref Expression
1 mgm2mgm ⊢ M ∈ MgmALT ↔ M ∈ Mgm
2 1 anbi1i ⊢ M ∈ MgmALT ∧ + M assLaw Base M ↔ M ∈ Mgm ∧ + M assLaw Base M
3 fvex ⊢ + M ∈ V
4 fvex ⊢ Base M ∈ V
5 3 4 pm3.2i ⊢ + M ∈ V ∧ Base M ∈ V
6 isasslaw ⊢ + M ∈ V ∧ Base M ∈ V → + M assLaw Base M ↔ ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
7 5 6 mp1i ⊢ M ∈ Mgm → + M assLaw Base M ↔ ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
8 7 pm5.32i ⊢ M ∈ Mgm ∧ + M assLaw Base M ↔ M ∈ Mgm ∧ ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
9 2 8 bitri ⊢ M ∈ MgmALT ∧ + M assLaw Base M ↔ M ∈ Mgm ∧ ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
10 eqid ⊢ Base M = Base M
11 eqid ⊢ + M = + M
12 10 11 issgrpALT ⊢ M ∈ SGrpALT ↔ M ∈ MgmALT ∧ + M assLaw Base M
13 10 11 issgrp ⊢ M ∈ Smgrp ↔ M ∈ Mgm ∧ ∀ x ∈ Base M ∀ y ∈ Base M ∀ z ∈ Base M x + M y + M z = x + M y + M z
14 9 12 13 3bitr4i ⊢ M ∈ SGrpALT ↔ M ∈ Smgrp