Theorem sgrp2sgrp

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

	Ref	Expression
Assertion	sgrp2sgrp	⊢ ( 𝑀 ∈ SGrpALT ↔ 𝑀 ∈ Smgrp )

Proof

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