Metamath Proof Explorer


Theorem issgrpn0

Description: The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020)

Ref Expression
Hypotheses issgrpn0.b 𝐵 = ( Base ‘ 𝑀 )
issgrpn0.o = ( +g𝑀 )
Assertion issgrpn0 ( 𝐴𝐵 → ( 𝑀 ∈ Smgrp ↔ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 𝑦 ) 𝑧 ) = ( 𝑥 ( 𝑦 𝑧 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 issgrpn0.b 𝐵 = ( Base ‘ 𝑀 )
2 issgrpn0.o = ( +g𝑀 )
3 1 2 ismgmn0 ( 𝐴𝐵 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦 ) ∈ 𝐵 ) )
4 3 anbi1d ( 𝐴𝐵 → ( ( 𝑀 ∈ Mgm ∧ ∀ 𝑥𝐵𝑦𝐵𝑧𝐵 ( ( 𝑥 𝑦 ) 𝑧 ) = ( 𝑥 ( 𝑦 𝑧 ) ) ) ↔ ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑥𝐵𝑦𝐵𝑧𝐵 ( ( 𝑥 𝑦 ) 𝑧 ) = ( 𝑥 ( 𝑦 𝑧 ) ) ) ) )
5 1 2 issgrp ( 𝑀 ∈ Smgrp ↔ ( 𝑀 ∈ Mgm ∧ ∀ 𝑥𝐵𝑦𝐵𝑧𝐵 ( ( 𝑥 𝑦 ) 𝑧 ) = ( 𝑥 ( 𝑦 𝑧 ) ) ) )
6 r19.26-2 ( ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 𝑦 ) 𝑧 ) = ( 𝑥 ( 𝑦 𝑧 ) ) ) ↔ ( ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑥𝐵𝑦𝐵𝑧𝐵 ( ( 𝑥 𝑦 ) 𝑧 ) = ( 𝑥 ( 𝑦 𝑧 ) ) ) )
7 4 5 6 3bitr4g ( 𝐴𝐵 → ( 𝑀 ∈ Smgrp ↔ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧𝐵 ( ( 𝑥 𝑦 ) 𝑧 ) = ( 𝑥 ( 𝑦 𝑧 ) ) ) ) )